module Alarms:sig
..end
type
overflow_kind =
| |
Signed |
| |
Unsigned |
| |
Signed_downcast |
| |
Unsigned_downcast |
type
access_kind =
| |
For_reading |
| |
For_writing |
type
bound_kind =
| |
Lower_bound |
| |
Upper_bound |
type
alarm =
| |
Division_by_zero of |
|||
| |
Memory_access of |
|||
| |
Index_out_of_bound of |
(* |
None = lower bound is zero; Some up = upper bound
| *) |
| |
Invalid_shift of |
(* |
strict upper bound, if any
| *) |
| |
Pointer_comparison of |
|||
| |
Differing_blocks of |
(* |
The two expressions (which evaluate to
pointers) must point to the same allocated block
| *) |
| |
Overflow of |
|||
| |
Float_to_int of |
|||
| |
Not_separated of |
(* |
the two lvalues must be separated
| *) |
| |
Overlap of |
(* |
overlapping read/write: the two lvalues must be
separated or equal
| *) |
| |
Uninitialized of |
|||
| |
Dangling of |
|||
| |
Is_nan_or_infinite of |
|||
| |
Is_nan of |
|||
| |
Function_pointer of |
(* |
the type of the pointer is compatible with the type of the pointed
function (first argument). The second argument is the list of the
arguments of the call.
| *) |
| |
Uninitialized_union of |
|||
| |
Invalid_bool of |
(* |
Trap representation of a _Bool variable.
| *) |
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 ->
alarm -> Cil_types.code_annotation * bool
kf
must be given only if the kinstr
is a statement, and
must be the function enclosing this statement.kf
, loc
and
save
; also returns the corresponding code_annotationAlarms.to_annot
instead.val to_annot : Cil_types.kinstr ->
?loc:Cil_types.location -> alarm -> Cil_types.code_annotation * bool
code_annotation
, without any registration.
The returned boolean indicates that the alarm has not been registered
in the kernel yet.val iter : (Emitter.t ->
Cil_types.kernel_function ->
Cil_types.stmt ->
rank:int -> alarm -> Cil_types.code_annotation -> unit) ->
unit
val fold : (Emitter.t ->
Cil_types.kernel_function ->
Cil_types.stmt ->
rank:int -> alarm -> Cil_types.code_annotation -> 'a -> 'a) ->
'a -> 'a
val find : Cil_types.code_annotation -> alarm option
val remove : ?filter:(alarm -> bool) ->
?kinstr:Cil_types.kinstr -> Emitter.t -> unit
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
.val create_predicate : ?loc:Cil_types.location -> t -> Cil_types.predicate
val get_name : t -> string
val get_short_name : t -> string
val get_description : t -> string