module Property_status:sig
..end
A local status (shortly, a status) of a property is a status directly set
by an emitter. Thus a property may have several distinct status according to
who attempts the verification.
type
emitted_status =
| |
True |
(* |
for each execution path
ep from the program entry point to s ,
the formula (/\_ h) ==> P(ep) is true | *) |
| |
False_if_reachable |
(* |
for each execution path
ep from the program entry
point to s , the formula (/\_ h) ==> P(ep)
is false | *) |
| |
False_and_reachable |
(* |
it exists an execution path
ep from the program
entry point to s such that the formula (/\_ h) ==> P(ep) is false | *) |
| |
Dont_know |
(* |
any other case
| *) |
s
and implicitly depends on an execution path from the program
entry point to s
. It also depends on an explicit set of hypotheses H
indicating when emitting the property (see function Property_status.emit
).module Emitted_status:Datatype.S
with type t = emitted_status
exception Inconsistent_emitted_status of emitted_status * emitted_status
val emit : Emitter.t ->
hyps:Property.t list ->
Property.t -> ?distinct:bool -> emitted_status -> unit
emit e ~hyps p s
indicates that the status of p
is s
, is emitted by
e
, and is based on the list of hypothesis hyps
. If e
previously
emitted another status s'
, it must be emitted with the same hypotheses and
a consistency check is performed between s
and s'
and the best (by
default the strongest) status is kept. If distinct
is true
(default is
false
), then we consider than the given status actually merges several
statuses coming from distinct execution paths. The strategy for computing
the best status is changed accordingly. One example when ~distinct:true
may be required is when emitting a status for a pre-condition of a function
f
since the status associated to a pre-condition p
merges all statuses
of p
at each callsite of the function f
.Inconsistent_emitted_status
when emitting False after emitting True
or converselyval emit_and_get : Emitter.t ->
hyps:Property.t list ->
Property.t ->
?distinct:bool ->
emitted_status -> emitted_status
Property_status.emit
but also returns the computed status.val logical_consequence : Emitter.t -> Property.t -> Property.t list -> unit
logical_consequence e ppt list
indicates that the emitter e
considers
that ppt
is a logical consequence of the conjunction of properties
list
. Thus it lets the kernel automatically computes it: e
must not call
functions emit*
itself on this property, but the kernel ensures that the
status will be up-to-date when getting it.val legal_dependency_cycle : Emitter.t -> Property.Set.t -> unit
val self : State.t
type
emitter_with_properties = private {
|
emitter : |
|||
|
mutable properties : |
|||
|
logical_consequence : |
(* |
Is the emitted status automatically
inferred?
| *) |
type
inconsistent = private {
|
valid : |
|
invalid : |
type
status = private
| |
Never_tried |
(* |
Nobody tries to verify the property
| *) |
| |
Best of |
(* |
who attempt the verification
under which hypotheses
| *) |
| |
Inconsistent of |
(* |
someone locally says the property is valid
and someone else says it is invalid: only
the consolidated status may conclude.
| *) |
include Datatype.S
val get : Property.t -> status
Property_status.Consolidation.get
if you want to know the
consolidated status of the property.val iter_on_statuses : (emitter_with_properties ->
emitted_status -> unit) ->
Property.t -> unit
val fold_on_statuses : (emitter_with_properties ->
emitted_status -> 'a -> 'a) ->
Property.t -> 'a -> 'a
module Consolidation:sig
..end
module Feedback:sig
..end
module Consolidation_graph:sig
..end
val iter : (Property.t -> unit) -> unit
val fold : (Property.t -> 'a -> 'a) -> 'a -> 'a
val register : Property.t -> unit
val register_property_add_hook : (Property.t -> unit) -> unit
val remove : Property.t -> unit
val register_property_remove_hook : (Property.t -> unit) -> unit
val merge : old:Property.t list -> Property.t list -> unit
merge old new
registers properties in new
which are not in old
and
removes properties in old
which are not in new
.val automatically_proven : Property.t -> bool