sig
type extension_preprocessor =
Logic_ptree.lexpr list -> Logic_ptree.lexpr list
type extension_typer =
Logic_typing.typing_context ->
Logic_ptree.location ->
Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind
type extension_visitor =
Cil.cilVisitor ->
Cil_types.acsl_extension_kind ->
Cil_types.acsl_extension_kind Cil.visitAction
type extension_printer =
Printer_api.extensible_printer_type ->
Format.formatter -> Cil_types.acsl_extension_kind -> unit
val register_behavior :
string ->
?preprocessor:Acsl_extension.extension_preprocessor ->
Acsl_extension.extension_typer ->
?visitor:Acsl_extension.extension_visitor ->
?printer:Acsl_extension.extension_printer ->
?short_printer:Acsl_extension.extension_printer -> bool -> unit
val register_global :
string ->
?preprocessor:Acsl_extension.extension_preprocessor ->
Acsl_extension.extension_typer ->
?visitor:Acsl_extension.extension_visitor ->
?printer:Acsl_extension.extension_printer ->
?short_printer:Acsl_extension.extension_printer -> bool -> unit
val register_code_annot :
string ->
?preprocessor:Acsl_extension.extension_preprocessor ->
Acsl_extension.extension_typer ->
?visitor:Acsl_extension.extension_visitor ->
?printer:Acsl_extension.extension_printer ->
?short_printer:Acsl_extension.extension_printer -> bool -> unit
val register_code_annot_next_stmt :
string ->
?preprocessor:Acsl_extension.extension_preprocessor ->
Acsl_extension.extension_typer ->
?visitor:Acsl_extension.extension_visitor ->
?printer:Acsl_extension.extension_printer ->
?short_printer:Acsl_extension.extension_printer -> bool -> unit
val register_code_annot_next_loop :
string ->
?preprocessor:Acsl_extension.extension_preprocessor ->
Acsl_extension.extension_typer ->
?visitor:Acsl_extension.extension_visitor ->
?printer:Acsl_extension.extension_printer ->
?short_printer:Acsl_extension.extension_printer -> bool -> unit
val register_code_annot_next_both :
string ->
?preprocessor:Acsl_extension.extension_preprocessor ->
Acsl_extension.extension_typer ->
?visitor:Acsl_extension.extension_visitor ->
?printer:Acsl_extension.extension_printer ->
?short_printer:Acsl_extension.extension_printer -> bool -> unit
end