Module Alarms

module Alarms: sig .. end
Alarms Database.
Change in Fluorine-20130401: fully re-implemented.

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 Cil_types.exp
| Memory_access of Cil_types.lval * access_kind
| Logic_memory_access of Cil_types.term * access_kind
| Index_out_of_bound of Cil_types.exp * Cil_types.exp option (*
None = lower bound is zero; Some up = upper bound
*)
| Invalid_shift of Cil_types.exp * int option (*
strict upper bound, if any
*)
| Pointer_comparison of Cil_types.exp option * Cil_types.exp
| Differing_blocks of Cil_types.exp * Cil_types.exp (*
The two expressions (which evaluate to pointers) must point to the same allocated block
*)
| Overflow of overflow_kind * Cil_types.exp * Integer.t * bound_kind
| Float_to_int of Cil_types.exp * Integer.t * bound_kind
| Not_separated of Cil_types.lval * Cil_types.lval (*
the two lvalues must be separated
*)
| Overlap of Cil_types.lval * Cil_types.lval (*
overlapping read/write: the two lvalues must be separated or equal
*)
| Uninitialized of Cil_types.lval
| Dangling of Cil_types.lval
| Is_nan_or_infinite of Cil_types.exp * Cil_types.fkind
| Valid_string of Cil_types.exp
| Function_pointer of Cil_types.exp (*
the type of the pointer is compatible with the type of the pointed function.
*)
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 ->
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.
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
Change in Aluminium-20160501: removed argument save. Use Alarms.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.
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
Generate the predicate corresponding to a given alarm.
Since Fluorine-20130401
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.