Module Biabduction.Builtin

Module for builtin functions with their symbolic execution handler

type args = {
  1. instr : IR.Sil.instr;
  2. prop_ : Prop.normal Prop.t;
  3. path : Paths.Path.t;
  4. ret_id_typ : IR.Ident.t * IR.Typ.t;
  5. args : (IR.Exp.t * IR.Typ.t) list;
  6. proc_name : IR.Procname.t;
  7. loc : IBase.Location.t;
  8. 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

val print_and_exit : unit -> 'a

Print the builtin functions and exit