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:
Just s
, where all missing properties are considered as true:
s
contains the only alarms that can occur.
AllBut s
, where all missing properties 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 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