package frama-c

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

    the preprocessed of a quantified predicate the (term * logic_var * term) list is the list of all the quantified variables along with their syntactic guards, and the predicate is the goal: the original predicate with all the quantifiers removed

Adds an optional additional guard condition that comes from the typing

  • returns

    the optional additional guard for a quantified logic variables. It may happen that the syntactic guard of the variable can be refined with the type of the variable, this additional predicate translates this refinement

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 : Frama_c_kernel.Cil_types.file -> unit

Preprocess all the quantified predicates in the ast and store the result in an hashtable

val preprocess_annot : Frama_c_kernel.Cil_types.code_annotation -> unit

Preprocess the quantified predicate in a given code annotation

val preprocess_predicate : Frama_c_kernel.Cil_types.predicate -> unit

Preprocess the quantified predicate in a given predicate

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