Module Ast.InstrSource

Sourcetype t = ..
Sourcetype t +=
  1. | Nop
  2. | Label of string
    (*

    label:

    *)
  3. | Assign of Loc.t loc * Expr.t loc
    (*

    lval := rval

    *)
  4. | Undef of Loc.t loc
    (*

    lval := undef

    *)
  5. | Nondet of Loc.t loc
    (*

    lval := nondet

    *)
  6. | Assume of Expr.t loc
    (*

    assume rval

    *)
  7. | Assert of Expr.t loc
    (*

    assert rval

    *)
  8. | If of Expr.t loc * string
    (*

    if rval then goto label

    *)
  9. | Goto of string
    (*

    goto label

    *)
  10. | Jump of Expr.t loc
    (*

    jump at rval

    *)
  11. | Halt
Sourceval nop : t
Sourceval label : string -> t
Sourceval assign : Loc.t loc -> Expr.t loc -> t
Sourceval undef : Loc.t loc -> t
Sourceval nondet : Loc.t loc -> t
Sourceval assume : Expr.t loc -> t
Sourceval dynamic_assert : Expr.t loc -> t
Sourceval conditional_jump : Expr.t loc -> string -> t
Sourceval dynamic_jump : Expr.t loc -> t
Sourceval goto : string -> t
Sourceval halt : t
Sourceval pp : Stdlib.Format.formatter -> t -> unit
Sourceval register_pp : (Stdlib.Format.formatter -> t -> bool) -> unit