module E_acsl_visitor:sig..end
val case_globals : default:(unit -> 'a) ->
?builtin:(Cil_types.varinfo -> 'a) ->
?fc_compiler_builtin:(Cil_types.varinfo -> 'a) ->
?rtl_symbol:(Cil_types.global -> 'a) ->
?fc_stdlib_generated:(Cil_types.varinfo -> 'a) ->
?var_fun_decl:(Cil_types.varinfo -> 'a) ->
?var_init:(Cil_types.varinfo -> 'a) ->
?var_def:(Cil_types.varinfo -> Cil_types.init -> 'a) ->
?glob_annot:(Cil_types.global_annotation -> 'a) ->
fun_def:(Cil_types.fundec -> 'a) -> Cil_types.global -> 'aFunction 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 builtinsfc_builtin_compiler is the case for frama-c or compiler builtinsrtl_symbol is the case for any global coming from the runtime libraryfc_stdlib_generated is the case for frama-c or standard library
generated functionsvar_fun_decl is the case for variables or functions declarationsvar_init is the case for variable definition wihtout an initialization
valuevar_def is the case for variable definitions with an initialization
valueglob_annot is the case for global annotationsfun_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 : (Property.t -> bool) Stdlib.ref
val must_translate_ppt_opt_ref : (Property.t option -> bool) Stdlib.ref