Module Biabduction.Prover

val atom_negate : IR.Tenv.t -> Predicates.atom -> Predicates.atom

Negate an atom

Ordinary Theorem Proving

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 -> Prop.normal 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 -> Prop.normal 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 -> Prop.normal Prop.t -> Predicates.atom -> bool

Check whether prop |- a. Result false means "don't know".

val check_inconsistency_base : IR.Tenv.t -> Prop.normal Prop.t -> bool

Inconsistency checking ignoring footprint.

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

Inconsistency checking.

val check_allocatedness : IR.Tenv.t -> Prop.normal Prop.t -> IR.Exp.t -> bool

Check whether prop |- allocated(exp).

val is_root : IR.Tenv.t -> Prop.normal Prop.t -> IR.Exp.t -> IR.Exp.t -> 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 -> Predicates.hpred -> bool * bool * 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 -> Prop.normal Prop.t -> IR.Exp.t -> IR.IntLit.t option * IR.IntLit.t option

Get upper and lower bounds of an expression, if any

Abduction prover

val check_implication : BiabductionSummary.t Absint.InterproceduralAnalysis.t -> Prop.normal Prop.t -> Prop.exposed 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
val d_typings : (IR.Exp.t * IR.Exp.t) list -> unit
type implication_result =
| ImplOK of check list * Predicates.subst * Predicates.subst * Predicates.hpred list * Predicates.atom list * Predicates.hpred list * Predicates.hpred list * 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 : BiabductionSummary.t Absint.InterproceduralAnalysis.t -> Prop.normal Prop.t -> Prop.exposed 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.

Cover: minimum set of pi's whose disjunction is equivalent to true

val find_minimum_pure_cover : IR.Tenv.t -> (Predicates.atom list * 'a) list -> (Predicates.atom list * 'a) list option

Find minimum set of pi's in cases whose disjunction covers true