Module Alarmset

module Alarmset: sig .. end
Map from alarms to status. Returned by the abstract domains and the evaluation functions of an abstract interpretation analysis.


There are two kinds of alarms map:
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 Dont_know status. = AllBut empty
val equal : t -> t -> bool
val is_empty : t -> bool
Is there an assertion with a non True status ?
val singleton : alarm -> t
val add' : alarm -> status -> t -> t
val add : alarm -> t -> t
! Different semantics according to the kind of alarms map. add alarm [Just s] = add' alarm Dont_know (Just s) add alarm [AllBut s] = add' alarm True (AllBut s)
val find : alarm -> t -> status
Returns the status of a given alarm.
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 : CilE.warn_mode -> t -> unit
Emits the alarms according to the given warn mode.
val start_stmt : Cil_types.kinstr -> unit
val end_stmt : unit -> unit
val current_stmt : unit -> Cil_types.kinstr
val pretty : Format.formatter -> t -> unit