Prover (infer.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