Previous  Up  Next

Module Property

module Property: sig .. end

ACSL comparable property.

Type declarations

type behavior_or_loop =
| Id_contract of Datatype.String.Set.t * Cil_types.funbehavior (*

in case of statement contract, we can have different contracts based on different sets of active behaviors.

*)
| Id_loop of Cil_types.code_annotation

assigns can belong either to a contract or a loop annotation

type identified_code_annotation = {
   ica_kf : Cil_types.kernel_function;
   ica_stmt : Cil_types.stmt;
   ica_ca : Cil_types.code_annotation;
}

Only AAssert, AInvariant, or APragma. Other code annotations are dispatched as identified_property of their own.

type identified_assigns = {
   ias_kf : Cil_types.kernel_function;
   ias_kinstr : Cil_types.kinstr;
   ias_bhv : behavior_or_loop;
   ias_froms : Cil_types.from list;
} 
type identified_allocation = {
   ial_kf : Cil_types.kernel_function;
   ial_kinstr : Cil_types.kinstr;
   ial_bhv : behavior_or_loop;
   ial_allocs : Cil_types.identified_term list * Cil_types.identified_term list;
} 
type identified_from = {
   if_kf : Cil_types.kernel_function;
   if_kinstr : Cil_types.kinstr;
   if_bhv : behavior_or_loop;
   if_from : Cil_types.from;
} 
type identified_decrease = {
   id_kf : Cil_types.kernel_function;
   id_kinstr : Cil_types.kinstr;
   id_ca : Cil_types.code_annotation option;
   id_variant : Cil_types.variant;
}

code_annotation is None for decreases and Some { AVariant } for loop variant.

type identified_behavior = {
   ib_kf : Cil_types.kernel_function;
   ib_kinstr : Cil_types.kinstr;
   ib_active : Datatype.String.Set.t;
   ib_bhv : 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.

type identified_complete = {
   ic_kf : Cil_types.kernel_function;
   ic_kinstr : Cil_types.kinstr;
   ic_active : Datatype.String.Set.t;
   ic_bhvs : Datatype.String.Set.t;
}

Same as for Property.identified_behavior.

type identified_disjoint = identified_complete 
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 = {
   ip_kind : predicate_kind;
   ip_kf : Cil_types.kernel_function;
   ip_kinstr : Cil_types.kinstr;
   ip_pred : Cil_types.identified_predicate;
} 
type program_point =
| Before
| After 
type identified_reachable = {
   ir_kf : Cil_types.kernel_function option;
   ir_kinstr : Cil_types.kinstr;
   ir_program_point : 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 Cil_types.kernel_function
| OLStmt of Cil_types.kernel_function * Cil_types.stmt
| OLGlob of Cil_types.location 
type extended_loc =
| ELContract of Cil_types.kernel_function
| ELStmt of Cil_types.kernel_function * Cil_types.stmt
| ELGlob 
type identified_extended = {
   ie_loc : extended_loc;
   ie_ext : Cil_types.acsl_extension;
} 
type identified_axiomatic = {
   iax_name : string;
   iax_props : identified_property list;
   iax_attrs : Cil_types.attributes;
} 
type identified_lemma = {
   il_name : string;
   il_labels : Cil_types.logic_label list;
   il_args : string list;
   il_pred : Cil_types.toplevel_predicate;
   il_attrs : Cil_types.attributes;
   il_loc : Cil_types.location;
} 
type identified_instance = {
   ii_kf : Cil_types.kernel_function;
   ii_stmt : Cil_types.stmt;
   ii_pred : Cil_types.identified_predicate option;
   ii_ip : 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.

type identified_type_invariant = {
   iti_name : string;
   iti_type : Cil_types.typ;
   iti_pred : Cil_types.predicate;
   iti_loc : Cil_types.location;
} 
type identified_global_invariant = {
   igi_name : string;
   igi_pred : Cil_types.predicate;
   igi_loc : Cil_types.location;
} 
type identified_other = {
   io_name : string;
   io_loc : other_loc;
} 
type identified_property = private
| IPPredicate of identified_predicate
| IPExtended of identified_extended
| 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 identified_other 
include Datatype.S_with_collections
module Ordered_by_function: Datatype.S_with_collections  with type t = identified_property

Datatype with alternative ordering, where properties are ordered according the following criteria: 1.

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.

Smart constructors

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_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.

val ip_of_global_annotation : Cil_types.global_annotation -> identified_property list
val ip_of_global_annotation_single : Cil_types.global_annotation -> identified_property option

getters

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 get_names : identified_property -> string list
val get_for_behaviors : identified_property -> string list
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.

names

module LegacyNames: sig .. end
module Names: sig .. end