package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install 

dune-project
 Dependency

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

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. A
    Anne Pacalet
  36. V
    Valentin Perrelle
  37. G
    Guillaume Petiot
  38. D
    Dario Pinto
  39. V
    Virgile Prevosto
  40. A
    Armand Puccetti
  41. F
    Félix Ridoux
  42. V
    Virgile Robles
  43. M
    Muriel Roger
  44. J
    Julien Signoles
  45. N
    Nicolas Stouls
  46. K
    Kostyantyn Vorobyov
  47. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-27.0-beta-Cobalt.tar.gz
sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

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

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

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.