Module `Biabduction__Prover`

val atom_negate : IR.Tenv.t -> Biabduction.Predicates.atom -> Biabduction.Predicates.atom: Negate an atom

val check_zero : IR.Tenv.t -> IR.Exp.t -> bool: Check |- e=0. Result false means "don't know".

val check_equal : IR.Tenv.t -> Biabduction.Prop.normal Biabduction.Prop.t -> IR.Exp.t -> IR.Exp.t -> bool: Check prop |- exp1=exp2. Result false means "don't know".

val check_disequal : IR.Tenv.t -> Biabduction.Prop.normal Biabduction.Prop.t -> IR.Exp.t -> IR.Exp.t -> bool: Check whether prop |- exp1!=exp2. Result false means "don't know".

val check_atom : IR.Tenv.t -> Biabduction.Prop.normal Biabduction.Prop.t -> Biabduction.Predicates.atom -> bool: Check whether prop |- a. Result false means "don't know".

val check_inconsistency_base : IR.Tenv.t -> Biabduction.Prop.normal Biabduction.Prop.t -> bool: Inconsistency checking ignoring footprint.

val check_inconsistency : IR.Tenv.t -> Biabduction.Prop.normal Biabduction.Prop.t -> bool: Inconsistency checking.

val check_allocatedness : IR.Tenv.t -> Biabduction.Prop.normal Biabduction.Prop.t -> IR.Exp.t -> bool: Check whether prop |- allocated(exp).

val is_root : IR.Tenv.t -> Biabduction.Prop.normal Biabduction.Prop.t -> IR.Exp.t -> IR.Exp.t -> Biabduction.Predicates.offset list option: is_root prop base_exp exp checks whether base_exp = exp.offlist for some list of offsets offlist. If so, it returns Some(offlist). Otherwise, it returns None. Assumes that base_exp points to the beginning of a structure, not the middle.

val expand_hpred_pointer : IR.Tenv.t -> bool -> Biabduction.Predicates.hpred -> bool * bool * Biabduction.Predicates.hpred: expand_hpred_pointer calc_index_frame hpred expands hpred if it is a |-> whose lhs is a Lfield or Lindex or ptr+off. Return (changed, calc_index_frame', hpred') where changed indicates whether the predicate has changed.

val get_bounds : IR.Tenv.t -> Biabduction.Prop.normal Biabduction.Prop.t -> IR.Exp.t -> IR.IntLit.t option * IR.IntLit.t option: Get upper and lower bounds of an expression, if any

val check_implication : Biabduction.BiabductionSummary.t Absint.InterproceduralAnalysis.t -> Biabduction.Prop.normal Biabduction.Prop.t -> Biabduction.Prop.exposed Biabduction.Prop.t -> bool: check_implication p1 p2 returns true if p1|-p2

type check = | Bounds_check | Class_cast_check of IR.Exp.t * IR.Exp.t * IR.Exp.t

type implication_result = | ImplOK of check list * Biabduction.Predicates.subst * Biabduction.Predicates.subst * Biabduction.Predicates.hpred list * Biabduction.Predicates.atom list * Biabduction.Predicates.hpred list * Biabduction.Predicates.hpred list * Biabduction.Predicates.hpred list * (IR.Exp.t * IR.Exp.t) list * (IR.Exp.t * IR.Exp.t) list | ImplFail of check list

val check_implication_for_footprint : Biabduction.BiabductionSummary.t Absint.InterproceduralAnalysis.t -> Biabduction.Prop.normal Biabduction.Prop.t -> Biabduction.Prop.exposed Biabduction.Prop.t -> implication_result: check_implication_for_footprint p1 p2 returns Some(sub, frame, missing) if sub(p1 * missing) |- sub(p2 * frame) where sub is a substitution which instantiates the primed vars of p1 and p2, which are assumed to be disjoint.

val find_minimum_pure_cover : IR.Tenv.t -> (Biabduction.Predicates.atom list * 'a) list -> (Biabduction.Predicates.atom list * 'a) list option: Find minimum set of pi's in cases whose disjunction covers true