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.kernel/Frama_c_kernel/Log/index.html

Module `Frama_c_kernel.Log`

Logging Services for Frama-C Kernel and Plugins.

since Beryllium-20090601-beta1

type kind =

| Result
| Feedback
| Debug
| Warning
| Error
| Failure
(*
- since Beryllium-20090601-beta1
*)

type event = {

evt_kind : kind;
evt_plugin : string;
evt_category : string option;
(*
message or warning category
*)
evt_source : Filepath.position option;
evt_message : string;

}

since Beryllium-20090601-beta1

type 'a pretty_printer =
  ?current:bool ->
  ?source:Filepath.position ->
  ?emitwith:(event -> unit) ->
  ?echo:bool ->
  ?once:bool ->
  ?append:(Format.formatter -> unit) ->
  ('a, Format.formatter, unit) format ->
  'a

Generic type for the various logging channels which are not aborting Frama-C.

When current is false (default for most of the channels), no location is output. When it is true, the last registered location is used as current (see Current_loc).
source is the location to be output. If nil, current is used to determine if a location should be output
emitwith function which is called each time an event is processed
echo is true if the event should be output somewhere in addition to stdout
append adds some actions performed on the formatter after the event has been processed.

since Beryllium-20090601-beta1

type ('a, 'b) pretty_aborter =
  ?current:bool ->
  ?source:Filepath.position ->
  ?echo:bool ->
  ?append:(Format.formatter -> unit) ->
  ('a, Format.formatter, unit, 'b) format4 ->
  'a

Same as Log.pretty_printer except that channels having this type denote a fatal error aborting Frama-C.

since Beryllium-20090601-beta1

Exception Registry

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

since Beryllium-20090601-beta1

exception AbortError of string

User error that prevents a plugin to terminate. Argument is the name of the plugin.

since Beryllium-20090601-beta1

exception AbortFatal of string

Internal error that prevents a plugin to terminate. Argument is the name of the plugin.

since Beryllium-20090601-beta1

exception FeatureRequest of Filepath.position option * string * string

Raised by not_yet_implemented. You may catch FeatureRequest(s,p,r) to support degenerated behavior. The (optional) source location is s, the responsible plugin is 'p' and the feature request is 'r'.

before 23.0-Vanadium
there was no source location

Option_signature.Interface

since Beryllium-20090601-beta1

type ontty = [

| `Message
(*
Normal message (default)
*)
| `Feedback
(*
Temporary visible on console, normal message otherwise
*)
| `Transient
(*
Temporary visible, only on console
*)
| `Silent
(*
Not visible on console
*)

]

type warn_status =

| Winactive
(*
nothing is emitted.
*)
| Wfeedback_once
(*
combines feedback and once.
*)
| Wfeedback
(*
emit a feedback message.
*)
| Wonce
(*
emit a warning message, but only the first time the category is encountered.
*)
| Wactive
(*
emit a warning message.
*)
| Werror_once
(*
combines once and error.
*)
| Werror
(*
emit a message. Execution continues, but exit status will not be 0
*)
| Wabort
(*
emit a message and abort execution
*)

status of a warning category

since Chlorine-20180501

module type Messages = sig ... end

val evt_category : event -> string list

Split an event category into its constituants.

since 18.0-Argon

val split_category : string -> string list

Split a category specification into its constituants. "*" is considered as empty, and "" categories are skipped.

since 18.0-Argon

val is_subcategory : string list -> string list -> bool

Sub-category checks. is_subcategory a b checks whether a is a sub-category of b. Indeed, it checks whether b is a prefix of a, that is, that a equals b or refines b with (a list of) sub-category(ies).

since 18.0-Argon

module Register (_ : sig ... end) : Messages

Each plugin has its own channel to output messages. This functor should not be directly applied by plug-in developer. They should apply Plugin.Register instead.

Echo and Notification

val set_echo : ?plugin:string -> ?kind:kind list -> bool -> unit

Turns echo on or off. Applies to all channel unless specified, and all kind of messages unless specified.

since Beryllium-20090601-beta1

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

val add_listener : ?plugin:string -> ?kind:kind list -> (event -> unit) -> unit

Register a hook that is called each time an event is emitted. Applies to all channel unless specified, and all kind of messages unless specified.

Warning: when executing the listener, all listeners will be temporarily deactivated in order to avoid infinite recursion.

since Beryllium-20090601-beta1

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

val echo : event -> unit

Display an event of the terminal, unless echo has been turned off.

since Beryllium-20090601-beta1

val notify : event -> unit

Send an event over the associated listeners.

since Beryllium-20090601-beta1

Channel interface

This is the low-level interface to logging services. Not to be used by casual users.

type channel

since Beryllium-20090601-beta1

val new_channel : string -> channel

since Beryllium-20090901

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

val log_channel : channel -> ?kind:kind -> 'a pretty_printer

logging function to user-created channel.

since Beryllium-20090901

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

val kernel_channel_name : string

the reserved channel name used by the Frama-C kernel.

since Beryllium-20090601-beta1

val kernel_label_name : string

the reserved label name used by the Frama-C kernel.

since Beryllium-20090601-beta1

val source : file:Filepath.Normalized.t -> line:int -> Filepath.position

since Chlorine-20180501

val get_current_source : unit -> Filepath.position

Terminal interface

This is the low-level interface to logging services. Not to be used by casual users.

val clean : unit -> unit

Flushes the last transient message if necessary.

val set_output : 
  ?isatty:bool ->
  (string -> int -> int -> unit) ->
  (unit -> unit) ->
  unit

This function has the same parameters as Format.make_formatter.

since Beryllium-20090901

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

val print_on_output : (Format.formatter -> unit) -> unit

Direct printing on output. Message echo is delayed until the output is finished. Then, the output is flushed and all pending message are echoed. Notification of listeners is not delayed, however.

Can not be recursively invoked.

since Beryllium-20090901

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

val print_delayed : (Format.formatter -> unit) -> unit

Direct printing on output. Same as print_on_output, except that message echo is not delayed until text material is actually written. This gives an chance for formatters to emit messages before actual pretty printing.