Module `Biabduction__SymExec`

val declare_locals_and_ret : IR.Tenv.t -> IR.Procdesc.t -> Biabduction.Prop.normal Biabduction.Prop.t -> Biabduction.Prop.normal Biabduction.Prop.t: Symbolic execution of the declaration of locals and return value.

val node : (exn -> unit) -> Biabduction.BiabductionSummary.t Absint.InterproceduralAnalysis.t -> Absint.ProcCfg.Exceptional.t -> Absint.ProcCfg.Exceptional.Node.t -> Biabduction.Paths.PathSet.t -> Biabduction.Paths.PathSet.t: Symbolic execution of the instructions of a node, lifted to sets of propositions.

val instrs : ?⁠mask_errors:bool -> Biabduction.BiabductionSummary.t Absint.InterproceduralAnalysis.t -> IR.Instrs.not_reversed_t -> (Biabduction.Prop.normal Biabduction.Prop.t * Biabduction.Paths.Path.t) list -> (Biabduction.Prop.normal Biabduction.Prop.t * Biabduction.Paths.Path.t) list: Symbolic execution of a sequence of instructions. If errors occur and mask_errors is true, just treat as skip.

val diverge : Biabduction.Prop.normal Biabduction.Prop.t -> Biabduction.Paths.Path.t -> (Biabduction.Prop.normal Biabduction.Prop.t * Biabduction.Paths.Path.t) list: Symbolic execution of the divergent pure computation.

val proc_call : (IR.Procdesc.t * Biabduction.BiabductionSummary.t) -> Biabduction.Builtin.t
val unknown_or_scan_call : is_scan:bool -> reason:string -> IR.Typ.t -> IR.Annot.Item.t -> Biabduction.Builtin.t
val check_variadic_sentinel : ?⁠fails_on_nil:bool -> int -> (int * int) -> Biabduction.Builtin.t
val check_arith_norm_exp : Biabduction.BiabductionSummary.t Absint.InterproceduralAnalysis.t -> IR.Exp.t -> Biabduction.Prop.normal Biabduction.Prop.t -> IR.Exp.t * Biabduction.Prop.normal Biabduction.Prop.t: Check for arithmetic problems and normalize an expression.

val prune : IR.Tenv.t -> positive:bool -> IR.Exp.t -> Biabduction.Prop.normal Biabduction.Prop.t -> Biabduction.Propset.t