Module Bound_variables

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


val 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

val 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 conditions 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