module Bound_variables:sig
..end
Module for preprocessing the quantified predicates. Predicates with
quantifiers are hard to translate, so we delegate some of the work to
a preprocessing phase. At the end of this phase, all the quantified
predicates should have an associated preprocessed form vars * goal
where
vars
is a list of guarded variables in the right ordergoal
is the predicate under the quantifications
The guarded variables in the list vars
are of
type term * logic_var * term * predicate option
, where a tuple
(t1,v,t2,p)
indicates that v is a logic variable with the two
guards t1 <= x < t2 and p is an additional optional guard to
intersect the first guard with the provided type for the variable vval get_preprocessed_quantifier : Cil_types.predicate ->
((Cil_types.term * Cil_types.logic_var * Cil_types.term) list *
Cil_types.predicate)
Error.or_error
Getters and setters
(term * logic_var * term) list
is the list of all the quantified variables
along with their syntactic guards, and the predicate
is the goal: the
original predicate with all the quantifiers removedval add_guard_for_small_type : Cil_types.logic_var -> Cil_types.predicate -> unit
Adds an optional additional guard condition that comes from the typing
val get_guard_for_small_type : Cil_types.logic_var -> Cil_types.predicate option
val replace : Cil_types.predicate ->
(Cil_types.term * Cil_types.logic_var * Cil_types.term) list ->
Cil_types.predicate -> unit
Replace the computed guards. This is because the typing sometimes simplifies the computed bounds, so we allow for storing new bounds
val clear_guards : unit -> unit
Clear the table of guard condi tions for quantified variables
val preprocess : Cil_types.file -> unit
Preprocess all the quantified predicates in the ast and store the result in an hashtable
val preprocess_annot : Cil_types.code_annotation -> unit
Preprocess the quantified predicate in a given code annotation
val preprocess_predicate : Cil_types.predicate -> unit
Preprocess the quantified predicate in a given predicate