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 (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-e-acsl.core/E_ACSL/Options/index.html

Module `E_ACSL.Options`Source

implementation of Log.S for E-ACSL

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val warning : ?wkey:warn_category -> 'a Frama_c_kernel.Log.pretty_printer

Hypothesis and restrictions.

since Beryllium-20090601-beta1

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val error : 'a Frama_c_kernel.Log.pretty_printer

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

since Beryllium-20090601-beta1

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val abort : ('a, 'b) Frama_c_kernel.Log.pretty_aborter

user error stopping the plugin.

raises AbortError
with the channel name.

since Beryllium-20090601-beta1

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val failure : 'a Frama_c_kernel.Log.pretty_printer

internal error of the plug-in.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val fatal : ('a, 'b) Frama_c_kernel.Log.pretty_aborter

internal error of the plug-in.

raises AbortFatal
with the channel name.

since Beryllium-20090601-beta1

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val get_warn_status : warn_category -> Frama_c_kernel.Log.warn_status

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

module Verbose : Frama_c_kernel.Parameter_sig.Int

module Debug : Frama_c_kernel.Parameter_sig.Int

module Share : Frama_c_kernel.Parameter_sig.Specific_dir

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

module Session : Frama_c_kernel.Parameter_sig.Specific_dir

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

module Config : Frama_c_kernel.Parameter_sig.Specific_dir

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

val help : Frama_c_kernel.Cmdline.Group.t

The group containing option -*-help.

since Boron-20100401

val messages : Frama_c_kernel.Cmdline.Group.t

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.

module Run : Frama_c_kernel.Parameter_sig.Bool

module Valid : Frama_c_kernel.Parameter_sig.Bool

module Gmp_only : Frama_c_kernel.Parameter_sig.Bool

module Full_mtracking : Frama_c_kernel.Parameter_sig.Bool

module Project_name : Frama_c_kernel.Parameter_sig.String

module Builtins : Frama_c_kernel.Parameter_sig.String_set

module Temporal_validity : Frama_c_kernel.Parameter_sig.Bool

module Validate_format_strings : Frama_c_kernel.Parameter_sig.Bool

module Replace_libc_functions : Frama_c_kernel.Parameter_sig.Bool

module Assert_print_data : Frama_c_kernel.Parameter_sig.Bool

module Concurrency : Frama_c_kernel.Parameter_sig.Bool

module Functions : Frama_c_kernel.Parameter_sig.Kernel_function_set

module Instrument : Frama_c_kernel.Parameter_sig.Kernel_function_set

module Widening_arguments_base : Frama_c_kernel.Parameter_sig.Int

module Widening_arguments : 
  Frama_c_kernel.Parameter_sig.Map with type key = string and type value = int

module Widening_output_base : Frama_c_kernel.Parameter_sig.Int

module Widening_output : 
  Frama_c_kernel.Parameter_sig.Map with type key = string and type value = int

Sourceval parameter_states : Frama_c_kernel.State.t list

Sourceval emitter : Frama_c_kernel.Emitter.t

Sourceval must_visit : unit -> bool

Sourcemodule Dkey : sig ... end

Sourceval setup : ?rtl:bool -> unit -> unit

Verify and initialize the options of the current project according to the options set by the user. If rtl is true, then the project being modified is the RTL project.