E_ACSL.Logic_normalizer
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 : Frama_c_kernel.Cil_types.file -> unit
Preprocess all the predicates of the ast and store the results
val preprocess_annot : Frama_c_kernel.Cil_types.code_annotation -> unit
Preprocess of the predicate of a single code annotation and store the results
val preprocess_predicate : Frama_c_kernel.Cil_types.predicate -> unit
Preprocess a predicate and its children and store the results
module Logic_infos : sig ... end
The analyses in Logic_normalizer
may:
val get_pred :
Frama_c_kernel.Cil_types.predicate ->
Frama_c_kernel.Cil_types.predicate
Retrieve the preprocessed form of a predicate
val get_orig_pred :
Frama_c_kernel.Cil_types.predicate ->
Frama_c_kernel.Cil_types.predicate
Retrieve the original form of the given predicate
val get_term : Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.term
Retrieve the preprocessed form of a term
val get_orig_term :
Frama_c_kernel.Cil_types.term ->
Frama_c_kernel.Cil_types.term
Retrieve the original form of the given term