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 Cil_types.named

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.