Module Property

module Property: sig .. end
ACSL comparable property.
Since Carbon-20101201
Consult the Plugin Development Guide for additional details.


Type declarations


type behavior_or_loop = 
| Id_behavior of Cil_types.funbehavior
| Id_code_annot of Cil_types.code_annotation
assigns can belong either to a contract or a loop annotation
type identified_complete = Cil_types.kernel_function * Cil_types.kinstr * string list 
type identified_disjoint = identified_complete 
type identified_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.
type identified_assigns = Cil_types.kernel_function * Cil_types.kinstr * behavior_or_loop *
Cil_types.identified_term Cil_types.from list
type identified_allocation = Cil_types.kernel_function * Cil_types.kinstr * behavior_or_loop *
(Cil_types.identified_term list * Cil_types.identified_term list)
type identified_from = Cil_types.kernel_function * Cil_types.kinstr * behavior_or_loop *
Cil_types.identified_term Cil_types.from
type identified_decrease = Cil_types.kernel_function * Cil_types.kinstr *
Cil_types.code_annotation option * Cil_types.term Cil_types.variant
code_annotation is None for decreases and Some { AVariant } for loop variant.
type identified_behavior = Cil_types.kernel_function * Cil_types.kinstr * Cil_types.funbehavior 
type predicate_kind = private 
| PKRequires of Cil_types.funbehavior
| PKAssumes of Cil_types.funbehavior
| PKEnsures of Cil_types.funbehavior * Cil_types.termination_kind
| PKTerminates
type identified_predicate = predicate_kind * Cil_types.kernel_function * Cil_types.kinstr *
Cil_types.identified_predicate
type program_point = 
| Before
| After
type identified_reachable = Cil_types.kernel_function option * Cil_types.kinstr * program_point 
None, Kglobal --> global property None, Some kf --> impossible Some kf, Kglobal --> property of a function without code Some kf, Kstmt stmt --> reachability of the given stmt (and the attached properties)
type identified_axiomatic = string * identified_property list 
type identified_lemma = string * Cil_types.logic_label list * string list *
Cil_types.predicate Cil_types.named * Cil_types.location
type identified_axiom = identified_lemma 
type identified_instance = Cil_types.kernel_function option * Cil_types.kinstr * identified_property 
Specialization of a property at a given point.
type identified_type_invariant = string * Cil_types.typ * Cil_types.predicate Cil_types.named *
Cil_types.location
type identified_global_invariant = string * Cil_types.predicate Cil_types.named * Cil_types.location 
type identified_property = private 
| IPPredicate of identified_predicate
| IPAxiom of identified_axiom
| IPAxiomatic of identified_axiomatic
| IPLemma of identified_lemma
| IPBehavior of identified_behavior
| IPComplete of identified_complete
| IPDisjoint of identified_disjoint
| IPCodeAnnot of identified_code_annotation
| IPAllocation of identified_allocation
| IPAssigns of identified_assigns
| IPFrom of identified_from
| IPDecrease of identified_decrease
| IPReachable of identified_reachable
| IPPropertyInstance of identified_instance
| IPTypeInvariant of identified_type_invariant
| IPGlobalInvariant of identified_global_invariant
| IPOther of string * Cil_types.kernel_function option * Cil_types.kinstr
include Datatype.S_with_collections
val short_pretty : 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.
Since Neon-20140301
val pretty_predicate_kind : Format.formatter -> predicate_kind -> unit
Since Oxygen-20120901

Smart constructors


val ip_other : string ->
Cil_types.kernel_function option ->
Cil_types.kinstr -> identified_property
Create a non-standard property.
Since Nitrogen-20111001
val ip_reachable_stmt : Cil_types.kernel_function -> Cil_types.stmt -> identified_property
Since Oxygen-20120901
val ip_reachable_ppt : identified_property -> identified_property
Since Oxygen-20120901
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.
Since Carbon-20110201
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.
Since Carbon-20110201
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.
Since Carbon-20110201
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.
Since Carbon-20110201
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.
Since Carbon-20110201
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.
Since Carbon-20110201
val ip_of_allocation : Cil_types.kernel_function ->
Cil_types.kinstr ->
behavior_or_loop ->
Cil_types.identified_term Cil_types.allocation ->
identified_property option
Builds the corresponding IPAllocation.
Since Oxygen-20120901
val ip_allocation_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior -> identified_property option
Builds IPAllocation for a contract.
Since Oxygen-20120901
val ip_of_assigns : Cil_types.kernel_function ->
Cil_types.kinstr ->
behavior_or_loop ->
Cil_types.identified_term Cil_types.assigns ->
identified_property option
Builds the corresponding IPAssigns.
Since Carbon-20110201
val ip_assigns_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior -> identified_property option
Builds IPAssigns for a contract (if not WritesAny)
Since Carbon-20110201
val ip_of_from : Cil_types.kernel_function ->
Cil_types.kinstr ->
behavior_or_loop ->
Cil_types.identified_term Cil_types.from -> identified_property
Builds the corresponding IPFrom.
Since Carbon-20110201
val ip_from_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior -> identified_property list
Builds IPFrom for a contract (if not ReadsAny)
Since Carbon-20110201
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)
Since Carbon-20110201
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)
Since Carbon-20110201
val ip_post_cond_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior -> identified_property list
Builds all IP related to the post-conditions (including allocates, frees, assigns and from)
Since Carbon-20110201
val ip_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.funbehavior -> identified_property
Builds the IP corresponding to the behavior itself.
Since Carbon-20110201
val ip_all_of_behavior : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.funbehavior -> identified_property list
Builds all IP related to a behavior.
Since Carbon-20110201
val ip_of_complete : Cil_types.kernel_function ->
Cil_types.kinstr -> string list -> identified_property
Builds IPComplete.
Since Carbon-20110201
val ip_complete_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.funspec -> identified_property list
Builds IPComplete of a given spec.
Since Carbon-20110201
val ip_of_disjoint : Cil_types.kernel_function ->
Cil_types.kinstr -> string list -> identified_property
Builds IPDisjoint.
Since Carbon-20110201
val ip_disjoint_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.funspec -> identified_property list
Builds IPDisjoint of a given spec.
Since Carbon-20110201
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.
Since Carbon-20110201
val ip_of_decreases : Cil_types.kernel_function ->
Cil_types.kinstr ->
Cil_types.term Cil_types.variant -> identified_property
Builds IPDecrease
Since Carbon-20110201
val ip_decreases_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.funspec -> identified_property option
Builds IPDecrease of a given spec.
Since Carbon-20110201
val ip_post_cond_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.funspec -> identified_property list
Builds all IP of post-conditions related to a spec.
Since Carbon-20110201
val ip_of_spec : Cil_types.kernel_function ->
Cil_types.kinstr -> Cil_types.funspec -> identified_property list
Builds all IP related to a spec.
Since Carbon-20110201
val ip_property_instance : Cil_types.kernel_function option ->
Cil_types.kinstr ->
identified_property -> identified_property
Build a specialization of the given property at the given function and stmt
val ip_axiom : identified_axiom -> identified_property
Builds an IPAxiom.
Since Carbon-20110201
Change in Oxygen-20120901: takes an identified_axiom instead of a string
val ip_lemma : identified_lemma -> identified_property
Build an IPLemma.
Since Nitrogen-20111001
Change in Oxygen-20120901: takes an identified_lemma instead of a string
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.
Since Carbon-20110201
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.
Since Carbon-20110201
Raises Invalid_argument if the resulting code annotation has an empty set of identified property
val ip_of_global_annotation : Cil_types.global_annotation -> identified_property list
Since Nitrogen-20111001
val ip_of_global_annotation_single : Cil_types.global_annotation -> identified_property option
Since Nitrogen-20111001

getters


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.
Since Oxygen-20120901

names


module Names: sig .. end