Module E_acsl_visitor

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 -> '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

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