module Logic_normalizer:sig
..end
This module is dedicated to some preprocessing on the predicates:
Pvalid
and Pvalid_read
clauses with
an adequate Pinitialized
clause;Papp
by a corresponding
term obtained as an application Tapp
The predicates that have undergone these changed are
called the preprocessed predicates.val preprocess : Cil_types.file -> unit
Preprocess all the predicates of the ast and store the results
val preprocess_annot : Cil_types.code_annotation -> unit
Preprocess of the predicate of a single code annotation and store the results
val preprocess_predicate : Cil_types.predicate -> unit
Preprocess a predicate and its children and store the results
val get_pred : Cil_types.predicate -> Cil_types.predicate
Retrieve the preprocessed form of a predicate
val get_term : Cil_types.term -> Cil_types.term
Retrieve the preprocessed form of a term
val clear : unit -> unit
clear the table of normalized predicates