Frama-C:
Plug-ins:
Libraries:

Frama-C API - Property

ACSL comparable property.

  • since Carbon-20101201

Type declarations

type behavior_or_loop =
  1. | 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.

    *)
  2. | Id_loop of Cil_types.code_annotation

assigns can belong either to a contract or a loop annotation

type identified_code_annotation = {
  1. ica_kf : Cil_types.kernel_function;
  2. ica_stmt : Cil_types.stmt;
  3. 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 = {
  1. ias_kf : Cil_types.kernel_function;
  2. ias_kinstr : Cil_types.kinstr;
  3. ias_bhv : behavior_or_loop;
  4. ias_froms : Cil_types.from list;
}
type identified_allocation = {
  1. ial_kf : Cil_types.kernel_function;
  2. ial_kinstr : Cil_types.kinstr;
  3. ial_bhv : behavior_or_loop;
  4. ial_allocs : Cil_types.identified_term list * Cil_types.identified_term list;
}
type identified_from = {
  1. if_kf : Cil_types.kernel_function;
  2. if_kinstr : Cil_types.kinstr;
  3. if_bhv : behavior_or_loop;
  4. if_from : Cil_types.from;
}
type identified_decrease = {
  1. id_kf : Cil_types.kernel_function;
  2. id_kinstr : Cil_types.kinstr;
  3. id_ca : Cil_types.code_annotation option;
  4. id_variant : Cil_types.variant;
}

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

type identified_behavior = {
  1. ib_kf : Cil_types.kernel_function;
  2. ib_kinstr : Cil_types.kinstr;
  3. ib_active : Datatype.String.Set.t;
  4. 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 = {
  1. ic_kf : Cil_types.kernel_function;
  2. ic_kinstr : Cil_types.kinstr;
  3. ic_active : Datatype.String.Set.t;
  4. ic_bhvs : Datatype.String.Set.t;
}

Same as for identified_behavior.

type identified_disjoint = identified_complete
type predicate_kind = private
  1. | PKRequires of Cil_types.funbehavior
  2. | PKAssumes of Cil_types.funbehavior
  3. | PKEnsures of Cil_types.funbehavior * Cil_types.termination_kind
  4. | PKTerminates
type identified_predicate = {
  1. ip_kind : predicate_kind;
  2. ip_kf : Cil_types.kernel_function;
  3. ip_kinstr : Cil_types.kinstr;
  4. ip_pred : Cil_types.identified_predicate;
}
type program_point =
  1. | Before
  2. | After
type identified_reachable = {
  1. ir_kf : Cil_types.kernel_function option;
  2. ir_kinstr : Cil_types.kinstr;
  3. ir_program_point : program_point;
}

None, Kglobal --> global property None, Kstmt stmt --> impossible Some kf, Kglobal --> property of a function without code / Not directly attached to a statement Some kf, Kstmt stmt --> reachability of the given stmt (and the attached properties)

type other_loc =
  1. | OLContract of Cil_types.kernel_function
  2. | OLStmt of Cil_types.kernel_function * Cil_types.stmt
  3. | OLGlob of Cil_types.location
type extended_loc =
  1. | ELContract of Cil_types.kernel_function
  2. | ELStmt of Cil_types.kernel_function * Cil_types.stmt
  3. | ELGlob
type identified_extended = {
  1. ie_loc : extended_loc;
  2. ie_ext : Cil_types.acsl_extension;
}
and identified_axiomatic = {
  1. iax_name : string;
  2. iax_props : identified_property list;
  3. iax_attrs : Cil_types.attributes;
}
and identified_lemma = {
  1. il_name : string;
  2. il_labels : Cil_types.logic_label list;
  3. il_args : string list;
  4. il_pred : Cil_types.toplevel_predicate;
  5. il_attrs : Cil_types.attributes;
  6. il_loc : Cil_types.location;
}
and identified_instance = {
  1. ii_kf : Cil_types.kernel_function;
  2. ii_stmt : Cil_types.stmt;
  3. ii_pred : Cil_types.identified_predicate option;
  4. 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.

and identified_type_invariant = {
  1. iti_name : string;
  2. iti_type : Cil_types.typ;
  3. iti_pred : Cil_types.predicate;
  4. iti_loc : Cil_types.location;
}
and identified_global_invariant = {
  1. igi_name : string;
  2. igi_pred : Cil_types.predicate;
  3. igi_loc : Cil_types.location;
}
and identified_other = {
  1. io_name : string;
  2. io_loc : other_loc;
}
and identified_property = private
  1. | IPPredicate of identified_predicate
  2. | IPExtended of identified_extended
  3. | IPAxiomatic of identified_axiomatic
  4. | IPLemma of identified_lemma
  5. | IPBehavior of identified_behavior
  6. | IPComplete of identified_complete
  7. | IPDisjoint of identified_disjoint
  8. | IPCodeAnnot of identified_code_annotation
  9. | IPAllocation of identified_allocation
  10. | IPAssigns of identified_assigns
  11. | IPFrom of identified_from
  12. | IPDecrease of identified_decrease
  13. | IPReachable of identified_reachable
  14. | IPPropertyInstance of identified_instance
  15. | IPTypeInvariant of identified_type_invariant
  16. | IPGlobalInvariant of identified_global_invariant
  17. | IPOther of identified_other
include Datatype.S_with_collections with type t = identified_property
include Datatype.S with type t = identified_property
include Datatype.S_no_copy with type t = identified_property
include Datatype.Ty with type t = identified_property
val ty : t Type.t
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.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

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

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

module Set : Datatype.Set with type elt = t
module Map : Datatype.Map with type key = t
module Hashtbl : Datatype.Hashtbl with type key = t

Datatype with alternative ordering, where properties are ordered according the following criteria: 1. Kf name (global properties ranked first) 2. Kinstr 3. kind of property 4. id of the property

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.

  • since Neon-20140301
val pretty_predicate_kind : Stdlib.Format.formatter -> predicate_kind -> unit
  • since Oxygen-20120901
val pretty_debug : Stdlib.Format.formatter -> identified_property -> unit

Internal use only.

  • since 18.0-Argon

create a Loc_contract or Loc_stmt depending on the kinstr.

  • since 18.0-Argon

create a Loc_contract or Loc_stmt depending on the kinstr.

  • since 18.0-Argon

Smart constructors

val ip_other : string -> other_loc -> identified_property

Create a non-standard property.

  • since Nitrogen-20111001
  • since Oxygen-20120901
val ip_reachable_ppt : identified_property -> identified_property
  • since Oxygen-20120901

IPPredicate of a single requires.

  • since Carbon-20110201

Builds the IPPredicate corresponding to requires of a behavior.

  • since Carbon-20110201

IPPredicate of a single assumes.

  • since Carbon-20110201

Builds the IPPredicate corresponding to assumes of a behavior.

  • since Carbon-20110201

IPPredicate of single ensures.

  • since Carbon-20110201

Extended property.

  • since Chlorine-20180501

Builds the IPPredicate PKEnsures corresponding to a behavior.

  • since Carbon-20110201

Builds the corresponding IPAllocation.

  • since Oxygen-20120901
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

  • since Oxygen-20120901

Builds the corresponding IPAssigns.

  • since Carbon-20110201
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 ip_allocation_of_behavior for signification of active.

  • since Carbon-20110201

Builds the corresponding IPFrom (if not FromAny)

  • since Carbon-20110201
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 ip_from_of_behavior for signification of active

  • since Carbon-20110201

Builds IPAssigns for a loop annotation (if not WritesAny)

  • since Carbon-20110201

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 -> 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 ip_allocation_of_behavior for the signification of the active argument.

  • since Carbon-20110201
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 ip_allocation_of_behavior for signification of active

  • since Carbon-20110201
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 ip_allocation_of_behavior for signification of active

  • since Carbon-20110201
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 ip_allocation_of_behavior for signification of active

  • since Carbon-20110201
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 ip_allocation_of_behavior for signification of active

  • since Carbon-20110201
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 ip_allocation_of_behavior for signification of active

  • since Carbon-20110201
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 ip_allocation_of_behavior for signification of active

  • since Carbon-20110201

Builds IPTerminates of a given spec.

  • since Carbon-20110201

Builds IPDecrease

  • since Carbon-20110201

Builds IPDecrease of a given spec.

  • since Carbon-20110201
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 ip_post_cond_of_behavior for more information.

  • since Carbon-20110201
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 ip_allocation_of_behavior for signification of active

  • since Carbon-20110201

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.

Build an IPLemma.

  • since Nitrogen-20111001

Build an IPTypeInvariant.

Build an IPGlobalInvariant.

Builds all IP related to a given code annotation.

  • since Carbon-20110201

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.

  • raises Invalid_argument

    if the resulting code annotation has an empty set of identified property

  • since Carbon-20110201
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 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.

  • since 19.0-Potassium

For a given property, returns its corresponding kernel_function, kinstr and program point.

  • since 29.0-Copper

Uses get_ir. If ir_kf is Some kf and ir_kinstr is Kglobal, we try to attach a statement depending on ir_program_point : the first statement of kf for Before, the return statement of kf for After.

  • since 29.0-Copper
val get_behavior : identified_property -> Cil_types.funbehavior option
val get_names : identified_property -> string list
val get_for_behaviors : identified_property -> string list

returns the location of the property.

  • since Oxygen-20120901
val source : identified_property -> Filepath.position option

returns the location of the property, if not unknown.

  • since Chlorine-20180501

names

module Names : sig ... end