module Consolidation:sig
..end
typepending =
Property.Set.t Emitter.Usable_emitter.Map.t Emitter.Usable_emitter.Map.t
type
consolidated_status = private
| |
Never_tried |
(* |
Nobody tries to verify the property.
The argument is for internal use only
| *) |
| |
Considered_valid |
(* |
Nobody succeeds to verify the property, but it is expected to be
verified by another way (manual review, ...)
| *) |
| |
Valid of |
(* |
The verification of this property is fully done. No work to
do anymore for this property. The argument is the emitters who did the
job.
| *) |
| |
Valid_under_hyp of |
(* |
The verification of this property is locally done, but it remains
properties to verify in order to close the
work.
| *) |
| |
Unknown of |
(* |
The verification of this property is not finished: the property itself
remains to verify and it may also remain other pending properties.
NB: the pendings contains the property itself.
| *) |
| |
Invalid of |
(* |
The verification of this property is fully done. All its hypotheses have
been verified, but it is false: that is a true bug.
| *) |
| |
Invalid_under_hyp of |
(* |
This property is locally false, but it remains properties to verify in
order to be sure that is a bug.
| *) |
| |
Invalid_but_dead of |
(* |
This property is locally false, but there is other bugs in hypotheses
| *) |
| |
Valid_but_dead of |
(* |
This property is locally true, but there is bugs in hypotheses
| *) |
| |
Unknown_but_dead of |
(* |
This property is locally unknown, but there is other bugs in
hypotheses
| *) |
| |
Inconsistent of |
(* |
Inconsistency detected when computing the consolidated status.
The string explains what is the issue for the end-user.
| *) |
include Datatype.S
val get : Property.t -> t
val get_conjunction : Property.t list -> t