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-30.0-Zinc.tar.gz

sha256=3ac0f995261ec829a7bd042bf70fc29ac6379029eb9df30bcc044748eb4d2a56

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

Module `Wp.Warning`Source

Contextual Errors

Sourceexception Error of string * string

Source, Reason

Source

val error : 
  ?source:string ->
  ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
  'a

Warning Manager

Sourcetype t = {

loc : Frama_c_kernel.Filepath.position;
severe : bool;
source : string;
reason : string;
fallback : string;

}

Sourceval compare : t -> t -> int

Sourceval pretty : Stdlib.Format.formatter -> t -> unit

module Set : Stdlib.Set.S with type elt = t

module Map : Stdlib.Map.S with type key = t

Sourceval severe : Set.t -> bool

Sourcetype context

Sourceval context : ?source:string -> unit -> context

Sourceval flush : context -> Set.t

Sourceval add : t -> unit

Source

val create : 
  ?log:bool ->
  ?severe:bool ->
  ?source:string ->
  fallback:string ->
  ('a, Stdlib.Format.formatter, unit, t) Stdlib.format4 ->
  'a

Source

val emit : 
  ?severe:bool ->
  ?source:string ->
  fallback:string ->
  ('a, Stdlib.Format.formatter, unit) Stdlib.format ->
  'a

Emit a warning in current context. Defaults: severe=true, source="wp".

Source

val handle : 
  ?severe:bool ->
  fallback:string ->
  handler:('a -> 'b) ->
  ('a -> 'b) ->
  'a ->
  'b

Handle the error and emit a warning with specified severity and fallback if a context has been set. Otherwise, a WP-fatal error is raised instead. Default for severe is false.

before 30.0-Zinc
fallback was effect

Sourcetype 'a outcome =

| Result of Set.t * 'a
| Failed of Set.t

Source

val catch : 
  ?source:string ->
  ?severe:bool ->
  fallback:string ->
  ('a -> 'b) ->
  'a ->
  'b outcome

Set up a context for the job. If non-handled errors are raised, then a warning is emitted with specified severity and fallback. Default for severe is true.

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Wp.WarningSource

Module `Wp.Warning`Source