module Alarms:sig
..end
Alarms Database.
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 =
| |
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
Register the given alarm on the given statement. By default, no status is
emitted. 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
Conversion of an alarm to a 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
Iterator over all alarms and the associated annotations at some program point.
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.
val find : Cil_types.code_annotation -> alarm option
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
.
val create_predicate : ?loc:Cil_types.location -> t -> Cil_types.predicate
Generate the predicate corresponding to a given alarm.
val get_name : t -> string
Short name of the alarm, used to prefix the assertion in the AST.
val get_short_name : t -> string
Even shorter name. Similar alarms (e.g. signed overflow vs. unsigned overflow) are aggregated.
val get_description : t -> string
Long description of the alarm, explaining the UB it guards against.