Module UnitTests__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