package frama-c

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

Generate C implementations of user-defined logic functions. A logic function can have multiple C implementations depending on the types computed for its arguments. Eg: Consider the following definition: integer g(integer x) = x with the following calls: g(5) and g(10*INT_MAX) They will respectively generate the C prototypes int g_1(int) and long g_2(long)

val reset : unit -> unit

Translate a Tapp term or a Papp predicate to an expression. If the optional argument eargs is provided, then these expressions are used as arguments of the fonction. The optional argument tapp is the term corresponding to the call, in case we are translating a term

val add_generated_functions_to_file : Frama_c_kernel.Cil_types.file -> unit

Insert into the globals of the given file the generated kernel functions (their declaration and their definition). Also registers these functions using Globals.Functions.register.

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