Module Alarms

module Alarms: sig .. end

Alarms Database.

Change in Fluorine-20130401

type overflow_kind =

`\|`	`Signed`
`\|`	`Unsigned`
`\|`	`Signed_downcast`
`\|`	`Unsigned_downcast`
`\|`	`Pointer_downcast`

Only signed overflows and pointer downcasts 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`
`\|`	`Index_out_of_bound of Cil_types.exp * Cil_types.exp option`	`(*`	`Index_out_of_bound(index, opt)` `opt = None` -> lower bound is zero; Some up = upper bound	`*)`
`\|`	`Invalid_pointer of Cil_types.exp`
`\|`	`Invalid_shift of Cil_types.exp * int option`	`(*`	strict upper bound, if any	`*)`
`\|`	`Pointer_comparison of Cil_types.exp option * Cil_types.exp`	`(*`	First parameter is `None` when implicit comparison to NULL pointer	`*)`
`\|`	`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`	`(*`	Integer parameters is the bound	`*)`
`\|`	`Float_to_int of Cil_types.exp * Integer.t * bound_kind`	`(*`	Integer parameter is the bound for the integer type. The actual alarm is `exp < bound+1` or `bound-1 < exp`.	`*)`
`\|`	`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`
`\|`	`Is_nan of Cil_types.exp * Cil_types.fkind`
`\|`	`Function_pointer of Cil_types.exp * Cil_types.exp list option`	`(*`	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 Cil_types.lval list`
`\|`	`Invalid_bool of Cil_types.lval`	`(*`	Trap representation of a _Bool variable.	`*)`

Change in Fluorine-20130401

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

Change in Fluorine-20130401

kf

loc

save

Change in Aluminium-20160501

Alarms.to_annot

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.