package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
val case_globals : default:(unit -> 'a) -> ?builtin:(Frama_c_kernel.Cil_types.varinfo -> 'a) -> ?fc_compiler_builtin:(Frama_c_kernel.Cil_types.varinfo -> 'a) -> ?rtl_symbol:(Frama_c_kernel.Cil_types.global -> 'a) -> ?fc_stdlib_generated:(Frama_c_kernel.Cil_types.varinfo -> 'a) -> ?var_fun_decl:(Frama_c_kernel.Cil_types.varinfo -> 'a) -> ?var_init:(Frama_c_kernel.Cil_types.varinfo -> 'a) -> ?var_def: (Frama_c_kernel.Cil_types.varinfo -> Frama_c_kernel.Cil_types.init -> 'a) -> ?glob_annot:(Frama_c_kernel.Cil_types.global_annotation -> 'a) -> fun_def:(Frama_c_kernel.Cil_types.fundec -> 'a) -> Frama_c_kernel.Cil_types.global -> 'a

Function to descend into the root of the ast according to the various cases relevant for E-ACSL. Each of the named argument corresponds to the function to be applied in the corresponding case. The default case is used if any optional argument is not given

  • builtin is the case for C builtins
  • fc_builtin_compiler is the case for frama-c or compiler builtins
  • rtl_symbol is the case for any global coming from the runtime library
  • fc_stdlib_generated is the case for frama-c or standard library generated functions
  • var_fun_decl is the case for variables or functions declarations
  • var_init is the case for variable definition wihtout an initialization value
  • var_def is the case for variable definitions with an initialization value
  • glob_annot is the case for global annotations
  • fun_def is the case for function definition.
class visitor : Options.category -> object ... end

Visitor to visit the AST in the same manner than the injector.

val must_translate_ppt_ref : (Frama_c_kernel.Property.t -> bool) ref
val must_translate_ppt_opt_ref : (Frama_c_kernel.Property.t option -> bool) ref
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