package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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:

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct