package frama-c

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

Install

Dune Dependency

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

Authors

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

Maintainers

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

Sources

frama-c-29.0-Copper.tar.gz
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/Wp_parameters/index.html

Module Wp.Wp_parametersSource

WP Plugin Interface

include Frama_c_kernel.Plugin.S
include Frama_c_kernel.Log.Messages
type category

category for debugging/verbose messages. Must be registered before any use. Each column in the string defines a sub-category, e.g. a:b:c defines a subcategory c of b, which is itself a subcategory of a. Enabling a category (via -plugin-msg-category) will enable all its subcategories.

  • since Fluorine-20130401
type warn_category

Same as above, but for warnings

  • since Chlorine-20180501
val verbose_atleast : int -> bool
  • since Beryllium-20090601-beta1
val debug_atleast : int -> bool
  • since Beryllium-20090601-beta1
val printf : ?level:int -> ?dkey:category -> ?current:bool -> ?source:Frama_c_kernel.Filepath.position -> ?append:(Format.formatter -> unit) -> ?header:(Format.formatter -> unit) -> ('a, Format.formatter, unit) format -> 'a

Outputs the formatted message on stdout. Levels and key-categories are taken into account like event messages. The header formatted message is emitted as a regular result message.

val result : ?level:int -> ?dkey:category -> 'a Frama_c_kernel.Log.pretty_printer

Results of analysis. Default level is 1.

  • since Beryllium-20090601-beta1
val has_tty : unit -> bool

Returns true is this Log's channel is in console mode

val feedback : ?ontty:Frama_c_kernel.Log.ontty -> ?level:int -> ?dkey:category -> 'a Frama_c_kernel.Log.pretty_printer

Progress and feedback. Level is tested against the verbosity level.

  • since Beryllium-20090601-beta1
val debug : ?level:int -> ?dkey:category -> 'a Frama_c_kernel.Log.pretty_printer

Debugging information dedicated to Plugin developers. Default level is 1. The debugging key is used in message headers. See also set_debug_keys and set_debug_keyset.

  • since Beryllium-20090601-beta1

Hypothesis and restrictions.

  • since Beryllium-20090601-beta1

user error: syntax/typing error, bad expected input, etc.

  • since Beryllium-20090601-beta1

user error stopping the plugin.

  • raises AbortError

    with the channel name.

  • since Beryllium-20090601-beta1

internal error of the plug-in.

internal error of the plug-in.

  • raises AbortFatal

    with the channel name.

  • since Beryllium-20090601-beta1
val verify : bool -> ('a, bool) Frama_c_kernel.Log.pretty_aborter

If the first argument is true, return true and do nothing else, otherwise, send the message on the fatal channel and return false.

The intended usage is: assert (verify e "Bla...") ;.

  • since Beryllium-20090601-beta1
val not_yet_implemented : ?current:bool -> ?source:Frama_c_kernel.Filepath.position -> ('a, Format.formatter, unit, 'b) format4 -> 'a

raises FeatureRequest but does not send any message. If the exception is not caught, Frama-C displays a feature-request message to the user.

  • since Beryllium-20090901
  • before 23.0-Vanadium

    there was no current and source arguments.

val deprecated : string -> now:string -> ('a -> 'b) -> 'a -> 'b

deprecated s ~now f indicates that the use of f of name s is now deprecated. It should be replaced by now.

  • returns

    the given function itself

  • since Lithium-20081201 in Extlib
  • since Beryllium-20090902
val with_result : (Frama_c_kernel.Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel.Log.pretty_aborter

with_result f fmt calls f in the same condition as logwith.

  • since Beryllium-20090601-beta1
val with_warning : (Frama_c_kernel.Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel.Log.pretty_aborter

with_warning f fmt calls f in the same condition as logwith.

  • since Beryllium-20090601-beta1
val with_error : (Frama_c_kernel.Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel.Log.pretty_aborter

with_error f fmt calls f in the same condition as logwith.

  • since Beryllium-20090601-beta1
val with_failure : (Frama_c_kernel.Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel.Log.pretty_aborter

with_failure f fmt calls f in the same condition as logwith.

  • since Beryllium-20090601-beta1
val log : ?kind:Frama_c_kernel.Log.kind -> ?verbose:int -> ?debug:int -> 'a Frama_c_kernel.Log.pretty_printer

Generic log routine. The default kind is Result. Use cases (with n,m > 0):

  • log ~verbose:n: emit the message only when verbosity level is at least n.
  • log ~debug:n: emit the message only when debugging level is at least n.
  • log ~verbose:n ~debug:m: any debugging or verbosity level is sufficient.
  • since Beryllium-20090901
val logwith : (Frama_c_kernel.Log.event option -> 'b) -> ?wkey:warn_category -> ?emitwith:(Frama_c_kernel.Log.event -> unit) -> ?once:bool -> ('a, 'b) Frama_c_kernel.Log.pretty_aborter

Recommanded generic log routine using warn_category instead of kind. logwith continuation ?wkey fmt similar to warning ?wkey fmt and then calling the continuation. The optional continuation argument refers to the corresponding event. None is used iff no message is logged. In case the wkey is considered as a Failure, the continution is not called. This kind of message denotes a fatal error aborting Frama-C. Notice that the ~emitwith action is called iff a message is logged.

  • since 18.0-Argon
val register : Frama_c_kernel.Log.kind -> (Frama_c_kernel.Log.event -> unit) -> unit

Local registry for listeners.

val register_tag_handlers : ((string -> string) * (string -> string)) -> unit

Category management

val register_category : string -> category

register a new debugging/verbose category. Note: categories must be added (e.g. via add_debug_keys) after registration.

  • since Fluorine-20130401
val pp_category : Format.formatter -> category -> unit

pretty-prints a category.

  • since Chlorine-20180501
val dkey_name : category -> string

returns the category name as a string.

  • since 18.0-Argon
val is_registered_category : string -> bool

true iff the string corresponds to a registered category

  • since Chlorine-20180501
val get_category : string -> category option

returns the corresponding registered category or None if no such category exists.

  • since Fluorine-20130401
val get_all_categories : unit -> category list

returns all registered categories.

val add_debug_keys : category -> unit

adds categories corresponding to string (including potential subcategories) to the set of categories for which messages are to be displayed. The string must have been registered beforehand.

  • since Fluorine-20130401 use categories instead of plain string
val del_debug_keys : category -> unit

removes the given categories from the set for which messages are printed. The string must have been registered beforehand.

  • since Fluorine-20130401
val get_debug_keys : unit -> category list

Returns currently active keys

  • since Fluorine-20130401
val is_debug_key_enabled : category -> bool

Returns true if the given category is currently active

  • since Fluorine-20130401
val register_warn_category : string -> warn_category
val is_warn_category : string -> bool
val pp_warn_category : Format.formatter -> warn_category -> unit
val pp_all_warn_categories_status : unit -> unit
val wkey_name : warn_category -> string

returns the warning category name as a string.

  • since 18.0-Argon
val get_warn_category : string -> warn_category option
val get_all_warn_categories : unit -> warn_category list
val get_all_warn_categories_status : unit -> (warn_category * Frama_c_kernel.Log.warn_status) list
val set_warn_status : warn_category -> Frama_c_kernel.Log.warn_status -> unit
include Frama_c_kernel.Plugin.S_no_log
val add_group : ?memo:bool -> string -> Frama_c_kernel.Cmdline.Group.t

Create a new group inside the plug-in. The given string must be different of all the other group names of this plug-in if memo is false. If memo is true the function will either create a fresh group or return an existing group of the same name in the same plugin. memo defaults to false

  • since Beryllium-20090901

Handle the specific `share' directory of the plug-in.

Handle the specific `session' directory of the plug-in.

Handle the specific `config' directory of the plug-in.

The group containing option -*-help.

  • since Boron-20100401

The group containing options -*-debug and -*-verbose.

  • since Boron-20100401
val add_plugin_output_aliases : ?visible:bool -> ?deprecated:bool -> string list -> unit

Adds aliases to the options -plugin-help, -plugin-verbose, -plugin-log, -plugin-msg-key, and -plugin-warn-key. add_plugin_output_aliases [alias] adds the aliases -alias-help, -alias-verbose, etc.

  • since 18.0-Argon
  • before 22.0-Titanium

    no visible and deprecated arguments.

Sourceval reset : unit -> unit
Sourceval is_interactive : unit -> bool

Function Selection

Sourcetype functions =
  1. | Fct_none
  2. | Fct_all
  3. | Fct_skip of Frama_c_kernel.Cil_datatype.Kf.Set.t
  4. | Fct_list of Frama_c_kernel.Cil_datatype.Kf.Set.t
Sourceval get_fct : unit -> functions
Sourceval iter_fct : (Frama_c_kernel.Kernel_function.t -> unit) -> functions -> unit
Sourceval iter_kf : (Frama_c_kernel.Kernel_function.t -> unit) -> unit

Goal Selection

Model Selection

Sourceval has_dkey : category -> bool

Computation Strategies

Prover Interface

Proof Obligations

Getters

Sourceval has_out : unit -> bool
Sourceval has_session : unit -> bool
Sourceval get_session : force:bool -> unit -> Frama_c_kernel.Datatype.Filepath.t
Sourceval get_session_dir : force:bool -> string -> Frama_c_kernel.Datatype.Filepath.t
Sourceval get_output_dir : string -> Frama_c_kernel.Datatype.Filepath.t
Sourceval make_output_dir : Frama_c_kernel.Datatype.Filepath.t -> unit

Debugging Categories

Sourceval has_print_generated : unit -> bool
Sourceval print_generated : ?header:string -> Frama_c_kernel.Filepath.Normalized.t -> unit

print the given file if the debugging category "print-generated" is set

Sourceval cat_print_generated : category
Sourceval protect : exn -> bool
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct