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 |
|||
| |
Logic_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 |
|||
| |
Valid_string of |
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
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.kf
, loc
and
save
; also returns the corresponding code_annotationval 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 Cil_types.named
val get_name : t -> string