module Alarmset:sig
..end
Map from alarms to status. Returned by the abstract semantics to report the possible undefined behaviors.
An alarm is a guard against an undesirable behavior. If the status of an assertion is true, then its corresponding undesirable behavior never occurs. Otherwise, the undesirable behavior may occur (unknown status) or definitely happens if the program point is reachable (false status).
The maps are partial. Missing assertions are implicitly bound to a default status. There are two kinds of alarm maps:
Just s
, where all missing assertions are considered as true:
s
contains the only alarms that can occur.AllBut s
, where all missing assertions are considered as
unknown: s
contains the only alarms whose status is known.type
s
type
t = private
| |
Just of |
| |
AllBut of |
typealarm =
Alarms.t
typestatus =
Abstract_interp.Comp.result
=
| |
True |
| |
False |
| |
Unknown |
type'a
if_consistent =[ `Inconsistent | `Value of 'a ]
module Status:sig
..end
val none : t
no alarms: all potential assertions have a True status. = Just empty
val all : t
all alarms: all potential assertions have a Unknown status. = AllBut empty
val set : alarm -> status -> t -> t
set alarm status t
binds the alarm
to the status
in the map t
.
val find : alarm -> t -> status
Returns the status of a given alarm.
val equal : t -> t -> bool
Are two maps equal?
val is_empty : t -> bool
Is there an assertion with a non True status ?
val singleton : ?status:status -> alarm -> t
singleton ?status alarm
creates the map set alarm status none
:
alarm
has a by default an unkown status (which can be overridden through
status
), and all others have a True status.
val combine : t -> t -> t
Combines two alarm maps carrying different sets of alarms. If t1
and t2
are sound alarm maps for the evaluation in the same state of the expressions
e1
and e2
respectively, then combine t1 t2
is a sound alarm map for
both evaluations of e1
and e2
.
val union : t -> t -> t
Pointwise union of property status: the least precise status is kept.
If t1
and t2
are sound alarm maps for a same expression e
in states
s1
and s2
respectively, then union t1 t2
is a sound alarm map for e
in states s1
and s2
.
val inter : t -> t -> t if_consistent
Pointwise intersection of property status: the most precise status is kept.
May return Inconsistent in case of incompatible status bound to an alarm.
If t1
and t2
are both sound alarm maps for a same expression e
in the
same state, then inter t1 t2
is also a sound alarm map for e
.
val exists : (alarm -> status -> bool) ->
default:(status -> bool) -> t -> bool
val for_all : (alarm -> status -> bool) ->
default:(status -> bool) -> t -> bool
val iter : (alarm -> status -> unit) -> t -> unit
val emit : Cil_types.kinstr -> t -> unit
Emits the alarms according to the given warn mode, at the given instruction.
val notify : CilE.warn_mode -> t -> unit
Calls the functions registered in the warn_mode
according to the
set of alarms.
val pretty : Stdlib.Format.formatter -> t -> unit
val pretty_status : Stdlib.Format.formatter -> status -> unit