Module Alarmset

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:
type s 
type t = private 
| Just of s
| AllBut of s
type alarm = Alarms.t 
type status = 
| 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 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