module Alarms: sig
.. end
Alarms Database.
Change in Fluorine-20130401: fully re-implemented.
Consult the Plugin Development Guide for additional details.
type
overflow_kind =
| |
Signed |
| |
Unsigned |
| |
Signed_downcast |
| |
Unsigned_downcast |
Only signed overflows int are really RTEs. The other kinds may be
meaningful nevertheless.
type
access_kind =
| |
For_reading |
| |
For_writing |
type
bound_kind =
| |
Lower_bound |
| |
Upper_bound |
type
alarm =
Change in Fluorine-20130401: full re-implementation
include Datatype.S_with_collections
val self : State.t
val register : Emitter.t ->
?kf:Cil_types.kernel_function ->
Cil_types.kinstr ->
?loc:Cil_types.location ->
?status:Property_status.emitted_status ->
?save:bool -> alarm -> Cil_types.code_annotation * bool
Register the given alarm on the given statement. By default, no status is
generated. If save
is false
(default is true
), the annotation
corresponding to the alarm is built, but neither it nor the alarm is
registered. kf
must be given only if the kinstr
is a statement, and
must be the function enclosing this statement.
Returns true if the given alarm has never been emitted before on the
same kinstr (without taking into consideration the status or
the emitter).
Change in Oxygen-20120901: remove labeled argument ~deps
Change in Fluorine-20130401: add the optional arguments kf
, loc
and
save
; also returns the corresponding code_annotation
val iter : (Emitter.t ->
Cil_types.kernel_function ->
Cil_types.stmt ->
rank:int -> alarm -> Cil_types.code_annotation -> unit) ->
unit
Iterator over all alarms and the associated annotations at some program
point.
Since Fluorine-20130401
val fold : (Emitter.t ->
Cil_types.kernel_function ->
Cil_types.stmt ->
rank:int -> alarm -> Cil_types.code_annotation -> 'a -> 'a) ->
'a -> 'a
Folder over all alarms and the associated annotations at some program
point.
Since Fluorine-20130401
val find : Cil_types.code_annotation -> alarm option
Since Fluorine-20130401
Returns the alarm corresponding to the given assertion, if any.
val remove : ?filter:(alarm -> bool) ->
?kinstr:Cil_types.kinstr -> Emitter.t -> unit
Remove the alarms and the associated annotations emitted by the given
emitter. If kinstr
is specified, remove only the ones associated with this
kinstr. If filter
is specified, remove only the alarms a
such that
filter a
is true
.
Since Fluorine-20130401
val create_predicate : ?loc:Cil_types.location -> t -> Cil_types.predicate Cil_types.named
Generate the predicate corresponding to a given alarm.
Since Fluorine-20130401