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 verifiy 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