Module Biabduction.Builtin
type args
=
{
instr : IR.Sil.instr;
prop_ : Prop.normal Prop.t;
path : Paths.Path.t;
ret_id_typ : IR.Ident.t * IR.Typ.t;
args : (IR.Exp.t * IR.Typ.t) list;
proc_name : IR.Procname.t;
loc : IBase.Location.t;
analysis_data : BiabductionSummary.t Absint.InterproceduralAnalysis.t;
}
type ret_typ
= (Prop.normal Prop.t * Paths.Path.t) list
type t
= args -> ret_typ
type registered
val register : IR.Procname.t -> t -> registered
Register a builtin
Procname.t
and symbolic execution handler
val get : IR.Procname.t -> t option
Get the symbolic execution handler associated to the builtin function name