Frama-C:
Plug-ins:
Libraries:

Frama-C API - Logic_normalizer

This module is dedicated to some preprocessing on the predicates:

  • It guards all the Pvalid and Pvalid_read clauses with an adequate Pinitialized clause;
  • It replaces all the applications 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 is_unsound_predicate : Frama_c_kernel.Cil_types.logic_info -> bool

Retrieve the preprocessed form of a predicate

Retrieve the original form of the given predicate

Retrieve the preprocessed form of a term

Retrieve the original form of the given term

val clear : unit -> unit

clear the table of normalized predicates