Wp.Warning
Contextual Errors
Warning Manager
type t = {
loc : Frama_c_kernel.Filepath.position;
severe : bool;
source : string;
reason : string;
effect : string;
}
val pretty : Stdlib.Format.formatter -> t -> unit
val context : ?source:string -> unit -> context
val flush : context -> Set.t
val add : t -> unit
val create :
?log:bool ->
?severe:bool ->
?source:string ->
effect:string ->
('a, Stdlib.Format.formatter, unit, t) Stdlib.format4 ->
'a
val emit :
?severe:bool ->
?source:string ->
effect:string ->
('a, Stdlib.Format.formatter, unit) Stdlib.format ->
'a
Emit a warning in current context. Defaults: severe=true
, source="wp"
.
Handle the error and emit a warning with specified severity and effect if a context has been set. Otherwise, a WP-fatal error is raised instead. Default for severe
is false.
val catch :
?source:string ->
?severe:bool ->
effect: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 effect. Default for severe
is true
.