module Property:sig
..end
ACSL comparable property.
type
behavior_or_loop =
| |
Id_contract of |
(* | in case of statement contract, we can have different contracts based on different sets of active behaviors. | *) |
| |
Id_loop of |
assigns can belong either to a contract or a loop annotation
typeidentified_code_annotation =
Cil_types.kernel_function * Cil_types.stmt * Cil_types.code_annotation
Only AAssert, AInvariant, or APragma. Other code annotations are dispatched as identified_property of their own.
typeidentified_assigns =
Cil_types.kernel_function * Cil_types.kinstr * behavior_or_loop *
Cil_types.from list
typeidentified_allocation =
Cil_types.kernel_function * Cil_types.kinstr * behavior_or_loop *
(Cil_types.identified_term list * Cil_types.identified_term list)
typeidentified_from =
Cil_types.kernel_function * Cil_types.kinstr * behavior_or_loop *
Cil_types.from
typeidentified_decrease =
Cil_types.kernel_function * Cil_types.kinstr *
Cil_types.code_annotation option * Cil_types.variant
code_annotation is None for decreases and Some { AVariant }
for
loop variant.
typeidentified_behavior =
Cil_types.kernel_function * Cil_types.kinstr * Datatype.String.Set.t *
Cil_types.funbehavior
for statement contract, the set of parent behavior for which the contract is active is part of its identification. If the set is empty, the contract is active for all parent behaviors.
typeidentified_complete =
Cil_types.kernel_function * Cil_types.kinstr * Datatype.String.Set.t *
string list
Same as for Property.identified_behavior
.
typeidentified_disjoint =
identified_complete
type
predicate_kind = private
| |
PKRequires of |
| |
PKAssumes of |
| |
PKEnsures of |
| |
PKTerminates |
typeidentified_predicate =
predicate_kind * Cil_types.kernel_function * Cil_types.kinstr *
Cil_types.identified_predicate
type
program_point =
| |
Before |
| |
After |
typeidentified_reachable =
Cil_types.kernel_function option * Cil_types.kinstr * program_point
None, Kglobal
--> global property
None, Some ki
--> impossible
Some kf, Kglobal
--> property of a function without code
Some kf, Kstmt stmt
--> reachability of the given stmt (and the attached
properties)
type
other_loc =
| |
OLContract of |
| |
OLStmt of |
| |
OLGlob of |
type
extended_loc =
| |
ELContract of |
| |
ELStmt of |
| |
ELGlob |
typeidentified_extended =
extended_loc * Cil_types.acsl_extension
typeidentified_axiomatic =
string * identified_property list
typeidentified_lemma =
string * Cil_types.logic_label list * string list * Cil_types.predicate *
Cil_types.location
typeidentified_axiom =
identified_lemma
typeidentified_instance =
Cil_types.kernel_function * Cil_types.stmt *
Cil_types.identified_predicate option * identified_property
Specialization of a property at a given point, identified by a statement and a function, along with the predicate transposed at this point (if it can be) and the original property.
typeidentified_type_invariant =
string * Cil_types.typ * Cil_types.predicate * Cil_types.location
typeidentified_global_invariant =
string * Cil_types.predicate * Cil_types.location
type
identified_property = private
| |
IPPredicate of |
| |
IPExtended of |
| |
IPAxiom of |
| |
IPAxiomatic of |
| |
IPLemma of |
| |
IPBehavior of |
| |
IPComplete of |
| |
IPDisjoint of |
| |
IPCodeAnnot of |
| |
IPAllocation of |
| |
IPAssigns of |
| |
IPFrom of |
| |
IPDecrease of |
| |
IPReachable of |
| |
IPPropertyInstance of |
| |
IPTypeInvariant of |
| |
IPGlobalInvariant of |
| |
IPOther of |
include Datatype.S_with_collections
val short_pretty : Stdlib.Format.formatter -> t -> unit
output a meaningful name for the property (e.g. the name of the corresponding identified predicate when available) reverting back to the full ACSL formula if it can't find one. The name is not meant to uniquely identify the property.
val pretty_predicate_kind : Stdlib.Format.formatter -> predicate_kind -> unit
val pretty_debug : Stdlib.Format.formatter -> identified_property -> unit
Internal use only.
val e_loc_of_stmt : Cil_types.kernel_function -> Cil_types.kinstr -> extended_loc
create a Loc_contract or Loc_stmt depending on the kinstr.
val o_loc_of_stmt : Cil_types.kernel_function -> Cil_types.kinstr -> other_loc
create a Loc_contract or Loc_stmt depending on the kinstr.
val ip_other : string -> other_loc -> identified_property
Create a non-standard property.
val ip_reachable_stmt : Cil_types.kernel_function -> Cil_types.stmt -> identified_property
val ip_reachable_ppt : identified_property -> identified_property
val ip_of_requires : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior ->
Cil_types.identified_predicate -> identified_property
IPPredicate of a single requires.
val ip_requires_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior -> identified_property list
Builds the IPPredicate corresponding to requires of a behavior.
val ip_of_assumes : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior ->
Cil_types.identified_predicate -> identified_property
IPPredicate of a single assumes.
val ip_assumes_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior -> identified_property list
Builds the IPPredicate corresponding to assumes of a behavior.
val ip_of_ensures : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior ->
Cil_types.termination_kind * Cil_types.identified_predicate ->
identified_property
IPPredicate of single ensures.
val ip_of_extended : extended_loc ->
Cil_types.acsl_extension -> identified_property
Extended property.
val ip_ensures_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior -> identified_property list
Builds the IPPredicate PKEnsures corresponding to a behavior.
val ip_of_allocation : Cil_types.kernel_function ->
Cil_types.kinstr ->
behavior_or_loop ->
Cil_types.allocation -> identified_property option
Builds the corresponding IPAllocation.
val ip_allocation_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list ->
Cil_types.funbehavior -> identified_property option
ip_allocation_of_behavior kf ki active bhv
builds IPAllocation for
behavior bhv
, in the spec in function kf
, at statement ki
, under
active behaviors active
val ip_of_assigns : Cil_types.kernel_function ->
Cil_types.kinstr ->
behavior_or_loop ->
Cil_types.assigns -> identified_property option
Builds the corresponding IPAssigns.
val ip_assigns_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list ->
Cil_types.funbehavior -> identified_property option
ip_assigns_of_behavior kf ki active bhv
builds IPAssigns for a contract (if not WritesAny).
See Property.ip_allocation_of_behavior
for signification of active
.
val ip_of_from : Cil_types.kernel_function ->
Cil_types.kinstr ->
behavior_or_loop ->
Cil_types.from -> identified_property option
Builds the corresponding IPFrom (if not FromAny)
val ip_from_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list ->
Cil_types.funbehavior -> identified_property list
ip_from_of_behavior kf ki active bhv
builds IPFrom for a behavior (if not ReadsAny).
See Property.ip_from_of_behavior
for signification of active
val ip_assigns_of_code_annot : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.code_annotation -> identified_property option
Builds IPAssigns for a loop annotation (if not WritesAny)
val ip_from_of_code_annot : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.code_annotation -> identified_property list
Builds IPFrom for a loop annotation(if not ReadsAny)
val ip_post_cond_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list ->
Cil_types.funbehavior -> identified_property list
ip_post_cond_of_behavior kf ki active bhv
builds all IP related to the post-conditions (including allocates, frees,
assigns and from). See Property.ip_allocation_of_behavior
for the signification
of the active
argument.
val ip_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list -> Cil_types.funbehavior -> identified_property
ip_of_behavior kf ki activd bhv
builds the IP corresponding
to the behavior itself.
See Property.ip_allocation_of_behavior
for signification of active
val ip_all_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list ->
Cil_types.funbehavior -> identified_property list
ip_all_of_behavior kf ki active bhv
builds all IP related to a behavior.
See Property.ip_allocation_of_behavior
for signification of active
val ip_of_complete : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list -> string list -> identified_property
ip_of_complete kf ki active complete
builds IPComplete.
See Property.ip_allocation_of_behavior
for signification of active
val ip_complete_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list -> Cil_types.funspec -> identified_property list
ip_complete_of_spec kf ki active spec
builds IPComplete of a given spec.
See Property.ip_allocation_of_behavior
for signification of active
val ip_of_disjoint : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list -> string list -> identified_property
ip_of_disjoint kf ki active disjoint
builds IPDisjoint.
See Property.ip_allocation_of_behavior
for signification of active
val ip_disjoint_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list -> Cil_types.funspec -> identified_property list
ip_disjoint_of_spec kf ki active spec
builds IPDisjoint of a given spec.
See Property.ip_allocation_of_behavior
for signification of active
val ip_of_terminates : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.identified_predicate -> identified_property
val ip_terminates_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.funspec -> identified_property option
Builds IPTerminates of a given spec.
val ip_of_decreases : Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.variant -> identified_property
Builds IPDecrease
val ip_decreases_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.funspec -> identified_property option
Builds IPDecrease of a given spec.
val ip_post_cond_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list -> Cil_types.funspec -> identified_property list
ip_post_cond_of_spec kf ki active spec
builds all IP of post-conditions related to a spec.
See Property.ip_post_cond_of_behavior
for more information.
val ip_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr ->
active:string list -> Cil_types.funspec -> identified_property list
ip_of_spec kf ki active spec
builds all IP related to a spec.
See Property.ip_allocation_of_behavior
for signification of active
val ip_property_instance : Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.identified_predicate option ->
identified_property -> identified_property
Build a specialization of the given property at the given function and stmt. The predicate is the property predicate transposed at the given statement, or None if it can't be.
val ip_axiom : identified_axiom -> identified_property
Builds an IPAxiom.
val ip_lemma : identified_lemma -> identified_property
Build an IPLemma.
val ip_type_invariant : identified_type_invariant -> identified_property
Build an IPTypeInvariant.
val ip_global_invariant : identified_global_invariant -> identified_property
Build an IPGlobalInvariant.
val ip_of_code_annot : Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation -> identified_property list
Builds all IP related to a given code annotation.
val ip_of_code_annot_single : Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.code_annotation -> identified_property
Builds the IP related to the code annotation. should be used only on code annotations returning a single ip, i.e. assert, invariant, variant, pragma.
Invalid_argument
if the resulting code annotation has an empty set
of identified propertyval ip_of_global_annotation : Cil_types.global_annotation -> identified_property list
val ip_of_global_annotation_single : Cil_types.global_annotation -> identified_property option
val has_status : identified_property -> bool
Does the property has a logical status (which may be Never_tried)? False for pragma, assumes clauses and some ACSL extensions.
val get_kinstr : identified_property -> Cil_types.kinstr
val get_kf : identified_property -> Cil_types.kernel_function option
val get_behavior : identified_property -> Cil_types.funbehavior option
val location : identified_property -> Cil_types.location
returns the location of the property.
val source : identified_property -> Filepath.position option
returns the location of the property, if not unknown.
module LegacyNames:sig
..end
module Names:sig
..end