Module AnalyzerTester.StructuredSil

structured language that makes it easy to write small test programs in OCaml

type assertion = string
type label = int
type structured_instr =
| Cmd of IR.Sil.instr
| If of IR.Exp.t * structured_instr list * structured_instr list
| While of IR.Exp.t * structured_instr list

try/catch/finally. note: there is no throw. the semantics are that every command in the try block is assumed to be possibly-excepting, and the catch block captures all exceptions

| Try of structured_instr list * structured_instr list * structured_instr list
| Invariant of assertion * label

gets autotranslated into assertions about abstract state

val pp_structured_instr : IR.Sil.F.formatter -> structured_instr -> unit
val pp_structured_instr_list : F.formatter -> structured_instr list -> unit
val pp_structured_program : F.formatter -> structured_instr list -> unit
val dummy_typ : IR.Typ.t
val dummy_loc : IBase.Location.t
val dummy_procname : IR.Procname.t
val label_counter : int IStdlib.IStd.ref
val fresh_label : unit -> int
val invariant : assertion -> structured_instr
val pvar_of_str : string -> IR.Pvar.t
val var_of_str : string -> IR.Exp.t
val ident_of_str : string -> IR.Ident.t
val unknown_exp : IR.Exp.t
val make_load : rhs_typ:IR.Typ.t -> IR.Ident.t -> IR.Exp.t -> structured_instr
val make_set : rhs_typ:IR.Typ.t -> lhs_exp:IR.Exp.t -> rhs_exp:IR.Exp.t -> structured_instr
val make_call : ?⁠procname:IR.Procname.t -> ?⁠return:(IR.Ident.t * IR.Typ.t) -> (IR.Exp.t * IR.Typ.t) list -> structured_instr
val make_store : rhs_typ:IR.Typ.t -> IR.Exp.t -> string -> rhs_exp:IR.Exp.t -> structured_instr
val make_load_fld : rhs_typ:IR.Typ.t -> string -> string -> IR.Exp.t -> structured_instr
val id_assign_exp : ?⁠rhs_typ:IR.Typ.t -> string -> IR.Exp.t -> structured_instr
val id_assign_id : ?⁠rhs_typ:IR.Typ.t -> string -> string -> structured_instr
val id_assign_var : ?⁠rhs_typ:IR.Typ.t -> string -> string -> structured_instr
val id_set_id : ?⁠rhs_typ:IR.Typ.t -> string -> string -> structured_instr
val var_assign_exp : rhs_typ:IR.Typ.t -> string -> IR.Exp.t -> structured_instr
val var_assign_int : string -> int -> structured_instr
val var_assign_id : ?⁠rhs_typ:IR.Typ.t -> string -> string -> structured_instr
val var_assign_addrof_var : ?⁠rhs_typ:IR.Typ.t -> string -> string -> structured_instr
val call_unknown : ?⁠return:(string * IR.Typ.t) -> string list -> structured_instr