package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Local status
1. Emitting a status
2. Getting a (local) status
Consolidated status
Iteration over the registered properties
API not for casual users

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.kernel/Frama_c_kernel/Property_status/index.html

Module `Frama_c_kernel.Property_status`

Status of properties.

since Nitrogen-20111001

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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 to s, the formula (/\_{h in H} h) ==> P(ep) is true
*)
| False_if_reachable
(*
for each execution path ep from the program entry point to s, the formula (/\_{h in H} 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 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.

returns
the kept status.

raises Inconsistent_emitted_status
when emitting False after emitting True or conversely

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.

since Oxygen-20120901

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 status
- l: 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

include Datatype.Ty with type t = status

type t = status

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val ty : t Type.t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val name : string

Unique name of the datatype.

val descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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 copy : t -> t

Deep copy: no possible sharing between x and copy x.

val get : Property.t -> status

returns
the most precise **local** status and all its emitters. Consider using Property_status.Consolidation.get if you want to know the consolidated status of the property.

Iteration on all the individual statuses emitted for the given property.

since Aluminium-20160501

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.

since 27.0-Cobalt

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

since 23.0-Vanadium

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

val register_property_add_hook : (Property.t -> unit) -> unit

Add an hook that will be called for any newly registered property

since Neon-20140301

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.

since Neon-20140301

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?