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) ->
fun_def:(Cil_types.fundec -> 'a) -> 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 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
valuefun_def
is the case for function definition.class visitor :object
..end
Visitor for managing the root of the AST, on the globals level, with the cases that are relevant to E-ACSL.