Module Alarmset

module Alarmset: sig .. end
Map from alarms to status. Returned by the abstract semantics to report the possible undefined behaviors.

Emitting alarms



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 = 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 : Format.formatter -> t -> unit
val pretty_status : Format.formatter -> status -> unit