Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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_or_str -> '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 without 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) Stdlib.ref
val must_translate_ppt_opt_ref : (Frama_c_kernel.Property.t option -> bool) Stdlib.ref