SymExec (infer.Biabduction.SymExec)

val declare_locals_and_ret : 
  IR.Tenv.t ->
  IR.Procdesc.t ->
  Prop.normal Prop.t ->
  Prop.normal Prop.t

Symbolic execution of the declaration of locals and return value.

val node : 
  (exn -> unit) ->
  BiabductionSummary.t Absint.InterproceduralAnalysis.t ->
  Absint.ProcCfg.Exceptional.t ->
  Absint.ProcCfg.Exceptional.Node.t ->
  Paths.PathSet.t ->
  Paths.PathSet.t

Symbolic execution of the instructions of a node, lifted to sets of propositions.

val instrs : 
  ?mask_errors:bool ->
  BiabductionSummary.t Absint.InterproceduralAnalysis.t ->
  IR.Instrs.not_reversed_t ->
  (Prop.normal Prop.t * Paths.Path.t) list ->
  (Prop.normal Prop.t * 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 : 
  Prop.normal Prop.t ->
  Paths.Path.t ->
  (Prop.normal Prop.t * Paths.Path.t) list

Symbolic execution of the divergent pure computation.

val proc_call : IR.Procname.t -> BiabductionSummary.t -> Builtin.t

val unknown_or_scan_call : 
  is_scan:bool ->
  reason:string ->
  IR.Typ.t ->
  IR.Annot.Item.t ->
  Builtin.t

val check_variadic_sentinel : 
  ?fails_on_nil:bool ->
  int ->
  (int * int) ->
  Builtin.t

val check_arith_norm_exp : 
  BiabductionSummary.t Absint.InterproceduralAnalysis.t ->
  IR.Exp.t ->
  Prop.normal Prop.t ->
  IR.Exp.t * Prop.normal Prop.t

Check for arithmetic problems and normalize an expression.

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