package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.0-beta-Nickel.tar.gz

sha256=0c80dae8074fcb3f6a33d7a41faf9939a2a336478a8d2c79e20e2d7bab953735

doc/frama-c-e-acsl.core/E_ACSL/E_acsl_visitor/index.html

Module `E_ACSL.E_acsl_visitor`

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