Module InferModules__Prover

Functions for Theorem Proving

val atom_negate : InferIR.Tenv.t -> InferIR.Sil.atom -> InferIR.Sil.atom

Negate an atom

Ordinary Theorem Proving

val check_zero : InferIR.Tenv.t -> InferIR.Exp.t -> bool

Check |- e=0. Result false means "don't know".

val check_equal : InferIR.Tenv.t -> InferModules.Prop.normal InferModules.Prop.t -> InferIR.Exp.t -> InferIR.Exp.t -> bool

Check prop |- exp1=exp2. Result false means "don't know".

val check_disequal : InferIR.Tenv.t -> InferModules.Prop.normal InferModules.Prop.t -> InferIR.Exp.t -> InferIR.Exp.t -> bool

Check whether prop |- exp1!=exp2. Result false means "don't know".

val type_size_comparable : InferIR.Typ.t -> InferIR.Typ.t -> bool

Return true if the two types have sizes which can be compared

val check_type_size_leq : InferIR.Typ.t -> InferIR.Typ.t -> bool

Check <= on the size of comparable types

val check_atom : InferIR.Tenv.t -> InferModules.Prop.normal InferModules.Prop.t -> InferIR.Sil.atom -> bool

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

val check_inconsistency_base : InferIR.Tenv.t -> InferModules.Prop.normal InferModules.Prop.t -> bool

Inconsistency checking ignoring footprint.

val check_inconsistency : InferIR.Tenv.t -> InferModules.Prop.normal InferModules.Prop.t -> bool

Inconsistency checking.

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

Check whether prop |- allocated(exp).

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

Get upper and lower bounds of an expression, if any

Abduction prover

val check_implication : InferIR.Typ.Procname.t -> InferIR.Tenv.t -> InferModules.Prop.normal InferModules.Prop.t -> InferModules.Prop.exposed InferModules.Prop.t -> bool

check_implication p1 p2 returns true if p1|-p2

type check =
| Bounds_check
| Class_cast_check of InferIR.Exp.t * InferIR.Exp.t * InferIR.Exp.t
val d_typings : (InferIR.Exp.t * InferIR.Exp.t) list -> unit
type implication_result =
| ImplOK of check list * InferIR.Sil.subst * InferIR.Sil.subst * InferIR.Sil.hpred list * InferIR.Sil.atom list * InferIR.Sil.hpred list * InferIR.Sil.hpred list * InferIR.Sil.hpred list * (InferIR.Exp.t * InferIR.Exp.t) list * (InferIR.Exp.t * InferIR.Exp.t) list
| ImplFail of check list
val check_implication_for_footprint : InferIR.Typ.Procname.t -> InferIR.Tenv.t -> InferModules.Prop.normal InferModules.Prop.t -> InferModules.Prop.exposed InferModules.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 : InferIR.Tenv.t -> (InferIR.Sil.atom list * 'a) list -> (InferIR.Sil.atom list * 'a) list option

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

Subtype checking

module Subtyping_check : sig ... end