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