package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

ACSL extensions registration module

  • since 21.0-Scandium
type extension_preprocessor = Logic_ptree.lexpr list -> Logic_ptree.lexpr list

Untyped ACSL extensions transformers

Transformers from untyped to typed ACSL extension

Visitor functions for ACSL extensions

type extension_preprocessor_block = (string * Logic_ptree.extended_decl list) -> string * Logic_ptree.extended_decl list
type extension_printer = Printer_api.extensible_printer_type -> Stdlib.Format.formatter -> Cil_types.acsl_extension_kind -> unit

Pretty printers for ACSL extensions

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.