module Acsl_extension:sig
..end
ACSL extensions registration module
typeextension_preprocessor =
Logic_ptree.lexpr list -> Logic_ptree.lexpr list
Untyped ACSL extensions transformers
typeextension_typer =
Logic_typing.typing_context ->
Logic_ptree.location ->
Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind
Transformers from untyped to typed ACSL extension
Visitor functions for ACSL extensions
typeextension_visitor =
Cil.cilVisitor ->
Cil_types.acsl_extension_kind ->
Cil_types.acsl_extension_kind Cil.visitAction
typeextension_preprocessor_block =
string * Logic_ptree.extended_decl list ->
string * Logic_ptree.extended_decl list
typeextension_typer_block =
Logic_typing.typing_context ->
Logic_ptree.location ->
string * Logic_ptree.extended_decl list -> Cil_types.acsl_extension_kind
Pretty printers for ACSL extensions
typeextension_printer =
Printer_api.extensible_printer_type ->
Stdlib.Format.formatter -> Cil_types.acsl_extension_kind -> unit
val register_behavior : string ->
?preprocessor:extension_preprocessor ->
extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer ->
?short_printer:extension_printer -> bool -> unit
register_behavior name ~preprocessor typer ~visitor ~printer ~short_printer status
registers new ACSL extension to be used in function contracts with name
name
.
The optional preprocessor
is a function to be applied by the parser on the
untyped content of the extension before parsing the rest of the processed
file. By default, this function is the identity.
The typer
is applied when transforming the untyped AST to Cil. It recieves
the typing context of the annotation that can be used to type the received
logic expressions (see Logic_typing.typing_context
), and the location of
the annotation.
The optional visitor
allows changing the way the ACSL extension is visited.
By default, the behavior is Cil.DoChildren
, which ends up visiting
each identified predicate/term in the list and leave the id as is.
The optional printer
allows changing the way the ACSL extension is pretty
printed. By default, it prints the name of the extension followed by the
formatted predicates, terms or identifier according to the
Cil_types.acsl_extension_kind
.
The optional short_printer
allows changing the Printer.pp_short_extended
behavior for the ACSL extension. By default, it just prints the name
. It
is for example used for the filetree in the GUI.
The status
indicates whether the extension can be assigned a property
status or not.
Here is a basic example:
let count = ref 0
let foo_typer typing_context loc = function
| p :: [] ->
Ext_preds
[ (typing_context.type_predicate
typing_context
(typing_context.post_state [Normal])
p)])
| [] -> let id = !count in incr count; Ext_id id
| _ -> typing_context.error loc "expecting a predicate after keyword FOO"
let () = Acsl_extension.register_behavior "FOO" foo_typer false
val register_global : string ->
?preprocessor:extension_preprocessor ->
extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer ->
?short_printer:extension_printer -> bool -> unit
Registers extension for global annotation. See register_behavior
.
val register_global_block : string ->
?preprocessor:extension_preprocessor_block ->
extension_typer_block ->
?visitor:extension_visitor ->
?printer:extension_printer ->
?short_printer:extension_printer -> bool -> unit
Registers extension for global block annotation. See register_behavior
.
val register_code_annot : string ->
?preprocessor:extension_preprocessor ->
extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer ->
?short_printer:extension_printer -> bool -> unit
Registers extension for code annotation to be evaluated at _current_
program point. See register_behavior
.
val register_code_annot_next_stmt : string ->
?preprocessor:extension_preprocessor ->
extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer ->
?short_printer:extension_printer -> bool -> unit
Registers extension for code annotation to be evaluated for the _next_
statement. See register_behavior
.
val register_code_annot_next_loop : string ->
?preprocessor:extension_preprocessor ->
extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer ->
?short_printer:extension_printer -> bool -> unit
Registers extension for loop annotation. See register_behavior
.
val register_code_annot_next_both : string ->
?preprocessor:extension_preprocessor ->
extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer ->
?short_printer:extension_printer -> bool -> unit
Registers extension both for code and loop annotations.
See register_behavior
.