Frama-C:
Plug-ins:
Libraries:

Frama-C API - Contract_types

type contract = {
  1. location : Frama_c_kernel.Cil_types.location;
    (*

    Location of the function or statement attached to the contract.

    *)
  2. named_behaviors_count : int;
    (*

    Number of named behaviors in the contract (excluding the default behavior)

    *)
  3. name_to_idx_tbl : (string, int) Frama_c_kernel.Hashtbl.t;
    (*

    Hashtable associating the name of a behavior with its index in the C API structure used to store behaviors information at runtime.

    *)
  4. mutable var : (Frama_c_kernel.Cil_types.varinfo * Frama_c_kernel.Cil_types.exp) option;
    (*

    Elements to access the C API structure used to store contracts information at runtime.

    *)
  5. mutable all_assumes_translated : bool;
    (*

    True if all the assumes clauses of the contract could be translated, false otherwise.

    If even one assume clause can't be translated, then the complete and disjoint clauses can't be computed.

    *)
  6. spec : Frama_c_kernel.Cil_types.spec;
    (*

    Specification for the contract

    *)
}

Represent a function or statement contract.