E_acsl_visitor (frama-c-e-acsl.E_ACSL.E_acsl

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