Frama-C API - Property_status
Status of properties.
Local status
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.
Emitting a status
type emitted_status =
| True
(*for each execution path
*)ep
from the program entry point tos
, the formula(/\_{h in H} h) ==> P(ep)
is true| False_if_reachable
(*for each execution path
*)ep
from the program entry point tos
, the formula(/\_{h in H} h) ==> P(ep)
is false| False_and_reachable
(*it exists an execution path
*)ep
from the program entry point tos
such that the formula(/\_{h in H} h) ==> P(ep)
is false| Dont_know
(*any other case
*)
Type of status emitted by analyzers. Each Property is attached to a program point 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 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
.
val emit_and_get : Emitter.t -> hyps:Property.t list -> Property.t -> ?distinct:bool -> emitted_status -> emitted_status
Like 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
The given properties may define a legal dependency cycle for the given emitter.
val self : State.t
The state which stores the computed status.
Getting a (local) status
type emitter_with_properties = private {
emitter : Emitter.Usable_emitter.t;
mutable properties : Property.t list;
logical_consequence : bool;
(*Is the emitted status automatically inferred?
*)
}
type inconsistent = private {
valid : emitter_with_properties list;
invalid : emitter_with_properties list;
}
type status = private
| Never_tried
(*Nobody tries to verify the property
*)| Best of emitted_status * emitter_with_properties list
(*Best(s, l)
:s
: The know more precise statusl
: who attempt the verification under which hypotheses
| Inconsistent of inconsistent
(*someone locally says the property is valid and someone else says it is invalid: only the consolidated status may conclude.
*)
Type of the local status of a property.
include Datatype.S with type t = status
include Datatype.S_no_copy with type t = status
val packed_descr : Structural_descr.pack
Packed version of the descriptor.
val reprs : t list
List of representants of the descriptor.
val hash : t -> int
Hash function: same spec than Hashtbl.hash
.
val pretty : Stdlib.Format.formatter -> t -> unit
Pretty print each value in an user-friendly way.
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
mem_project f x
must return true
iff there is a value p
of type Project.t
in x
such that f p
returns true
.
val get : Property.t -> status
Iteration on all the individual statuses emitted for the given 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
val register_status_update_hook : (emitter_with_properties -> Property.t -> emitted_status -> unit) -> unit
Registers an hook to be called each time a property status is emitted.
Consolidated status
module Consolidation : sig ... end
Consolidation of a property status according to the (consolidated) status of the hypotheses of the property.
module Feedback : sig ... end
Lighter version than Consolidation
module Consolidation_graph : sig ... end
See the consolidated status of a property in a graph, which all its dependencies and their consolidated status.
Iteration over the registered properties
val iter : (Property.t -> unit) -> unit
val fold : (Property.t -> 'a -> 'a) -> 'a -> 'a
val iter_sorted : cmp:(Property.t -> Property.t -> int) -> (Property.t -> unit) -> unit
val fold_sorted : cmp:(Property.t -> Property.t -> int) -> (Property.t -> 'a -> 'a) -> 'a -> 'a
API not for casual users
val register : Property.t -> unit
Register the given property. It must not be already registered.
val register_property_add_hook : (Property.t -> unit) -> unit
Add an hook that will be called for any newly registered property
val remove : Property.t -> unit
Remove the property deeply. Must be called only when removing the corresponding annotation.
val register_property_remove_hook : (Property.t -> unit) -> unit
Add an hook that will be called each time a property is removed.
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_computed : Property.t -> bool
Is the status of the given property only automatically handled by the kernel?