package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.kernel/Frama_c_kernel/Acsl_extension/index.html

Module `Frama_c_kernel.Acsl_extension`

ACSL extensions registration module

since 21.0-Scandium

type extension_preprocessor = Logic_ptree.lexpr list -> Logic_ptree.lexpr list

Untyped ACSL extensions transformers

type extension_typer =
  Logic_typing.typing_context ->
  Logic_ptree.location ->
  Logic_ptree.lexpr list ->
  Cil_types.acsl_extension_kind

Transformers from untyped to typed ACSL extension

type extension_visitor =
  Cil.cilVisitor ->
  Cil_types.acsl_extension_kind ->
  Cil_types.acsl_extension_kind Cil.visitAction

Visitor functions for ACSL extensions

type extension_preprocessor_block =
  (string * Logic_ptree.extended_decl list) ->
  string * Logic_ptree.extended_decl list

type extension_typer_block =
  Logic_typing.typing_context ->
  Logic_ptree.location ->
  (string * Logic_ptree.extended_decl list) ->
  Cil_types.acsl_extension_kind

type extension_printer =
  Printer_api.extensible_printer_type ->
  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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide