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).
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:
- closed maps
Just s
, where all missing assertions are considered as true:
s
contains the only alarms that can occur.
- open maps
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 s |
| |
AllBut of s |
type
alarm = Alarms.t
type
status =
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 add : alarm -> t -> t
! Different semantics according to the kind of the alarm map.
add alarm [Just s] = set alarm Unknown (Just s)
add alarm [AllBut s] = set alarm True (AllBut s)
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 : alarm -> t
singleton alarm
creates the map add alarm none
:
alarm
has a Unknown status, and all others have a True status.
val union : t -> t -> t
Pointwise union of property status: the least precise status is kept.
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.
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 : Format.formatter -> t -> unit
val pretty_status : Format.formatter -> status -> unit