module Acsl_extension:sig
..end
typeextension_preprocessor =
Logic_ptree.lexpr list -> Logic_ptree.lexpr list
typeextension_typer =
Logic_typing.typing_context ->
Logic_ptree.location ->
Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind
Visitor functions for ACSL extensions
typeextension_visitor =
Cil.cilVisitor ->
Cil_types.acsl_extension_kind ->
Cil_types.acsl_extension_kind Cil.visitAction
typeextension_printer =
Printer_api.extensible_printer_type ->
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
Consult the Plugin Development Guide for additional details.
val register_global : string ->
?preprocessor:extension_preprocessor ->
extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer ->
?short_printer:extension_printer -> bool -> unit
register_behavior
.val register_code_annot : string ->
?preprocessor:extension_preprocessor ->
extension_typer ->
?visitor:extension_visitor ->
?printer:extension_printer ->
?short_printer:extension_printer -> bool -> unit
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
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
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
register_behavior
.