Frama-C:
Plug-ins:
Libraries:

Frama-C API - Lang

Low-Level Logic Terms and Predicates

Logic Language based on Qed

Naming - Unique identifiers

val comp_id : Frama_c_kernel.Cil_types.compinfo -> string
val comp_init_id : Frama_c_kernel.Cil_types.compinfo -> string
val field_id : Frama_c_kernel.Cil_types.fieldinfo -> string
val field_init_id : Frama_c_kernel.Cil_types.fieldinfo -> string
val logic_id : Frama_c_kernel.Cil_types.logic_info -> string
val lemma_id : string -> string

Symbols

type datakind =
  1. | KValue
  2. | KInit
type adt = private
  1. | Qdata of Qed.Symbol.data
    (*

    Qed/Why3 Type

    *)
  2. | Atype of Frama_c_kernel.Cil_types.logic_type_info
    (*

    ACSL Logic Type

    *)
  3. | Comp of Frama_c_kernel.Cil_types.compinfo * datakind
    (*

    C-code Struct or Union

    *)

A type is never registered in a Definition.t

and fields = {
  1. mutable fields : field list;
}
and field = private
  1. | Cfield of Frama_c_kernel.Cil_types.fieldinfo * datakind
type lfun = private
  1. | ACSL of Frama_c_kernel.Cil_types.logic_info
    (*

    Registered in Definition.t only

    *)
  2. | CTOR of Frama_c_kernel.Cil_types.logic_ctor_info
    (*

    Not registered in Definition.t directly converted/printed

    *)
  3. | LFUN of lsymbol
    (*

    Generated logic symbol

    *)
  4. | QFUN of esymbol
    (*

    External logic symbol

    *)
and lsymbol = {
  1. m_name : string;
  2. m_context : WpContext.context option;
  3. m_category : lfun Qed.Logic.category;
  4. m_coloring : bool;
  5. m_result : tau;
  6. m_params : tau list;
}
and esymbol = {
  1. e_category : lfun Qed.Logic.category;
  2. e_coloring : bool;
  3. e_symbol : Qed.Symbol.lfun;
}
val fields_of_adt : adt -> field list
val fields_of_tau : tau -> field list
val fields_of_field : field -> field list
val on_lfun : (lfun -> unit) -> unit
val on_field : (field -> unit) -> unit

Builders

type 'a extern
val extern_t : string -> adt extern
val import_t : context:Why3.Theory.theory -> Why3.Ty.tysymbol -> adt
val import_f : context:Why3.Theory.theory -> Why3.Term.lsymbol -> lfun
val extern_f : ?category:lfun extern Qed.Logic.category -> ?coloring:bool -> string -> lfun extern
val generated_f : ?context:bool -> ?category:lfun Qed.Logic.category -> ?coloring:bool -> result:tau -> params:tau list -> ('a, Stdlib.Format.formatter, unit, lfun) Stdlib.format4 -> 'a
val generated_p : ?context:bool -> ?category:lfun Qed.Logic.category -> ?coloring:bool -> params:tau list -> ('a, Stdlib.Format.formatter, unit, lfun) Stdlib.format4 -> 'a

Sorting and Typing

val tau_of_object : Ctypes.c_object -> tau
val tau_of_ctype : Frama_c_kernel.Cil_types.typ -> tau
val tau_of_return : Frama_c_kernel.Cil_types.logic_type option -> tau
val tau_of_lfun : lfun -> tau option list -> tau
val adt_of_field : field -> adt
val tau_of_field : field -> tau
val tau_of_record : field -> tau
val init_of_object : Ctypes.c_object -> tau
val init_of_ctype : Frama_c_kernel.Cil_types.typ -> tau
val t_int : tau
val t_real : tau
val t_bool : tau
val t_prop : tau
val t_addr : unit -> tau
val t_float : Ctypes.c_float -> tau
val t_array : tau -> tau
val t_farray : tau -> tau -> tau
val t_data : adt -> tau list -> tau
val t_matrix : tau -> int -> tau
val pointer : tau Context.value

type of pointers

val floats : (Ctypes.c_float -> tau) Context.value

type of floats

val poly : string list Context.value

polymorphism

val parameters : (lfun -> Qed.Logic.sort list) -> unit

definitions

val context_of_lfun : lfun -> WpContext.context option

LFuns are unique by name and context

val is_coloring_lfun : lfun -> bool

Logic Formulae

module ADT : Qed.Logic.Data with type t = adt
module Field : Qed.Logic.Field with type t = field
module Fun : Qed.Logic.Function with type t = lfun
class virtual idprinting : object ... end
module F : sig ... end
module N : sig ... end

simpler notation for writing F.term and F.pred

Fresh Variables and Constraints

type gamma
val new_pool : ?copy:F.pool -> ?vars:F.Vars.t -> unit -> F.pool
val new_gamma : ?copy:gamma -> unit -> gamma
val local : ?pool:F.pool -> ?vars:F.Vars.t -> ?gamma:gamma -> ('a -> 'b) -> 'a -> 'b
val freshvar : ?basename:string -> F.tau -> F.var
val freshen : F.var -> F.var
val assume : F.pred -> unit
val without_assume : ('a -> 'b) -> 'a -> 'b
val hypotheses : gamma -> F.pred list
val get_pool : unit -> F.pool
val get_gamma : unit -> gamma
val has_gamma : unit -> bool
val get_hypotheses : unit -> F.pred list
val filter_hypotheses : F.var list -> F.pred list

Substitutions

val sigma : unit -> F.sigma

uses current pool

val alpha : unit -> F.sigma

freshen all variables

val subst : F.var list -> F.term list -> F.sigma

replace variables

val e_subst : (F.term -> F.term) -> F.term -> F.term

uses current pool

val p_subst : (F.term -> F.term) -> F.pred -> F.pred

uses current pool

module E : sig ... end
val extern : 'a extern -> 'a
val extern_mk : (Why3.Env.env -> 'a) -> 'a extern
val extern_tau : string -> F.tau extern
val extern_val : string -> F.term extern
val extern_map : ('a -> 'b) -> 'a extern -> 'b extern
val extern_const : 'a -> 'a extern
val extern_data : adt extern -> F.tau list -> F.tau
val extern_lfun : lfun extern -> F.term list -> F.term
val extern_pred : lfun extern -> F.term list -> F.pred

Simplifiers

exception Contradiction
val is_literal : F.term -> bool
val iter_consequence_literals : (F.term -> unit) -> F.term -> unit

iter_consequence_literals assume_from_literal hypothesis applies the function assume_from_literal on literals that are a consequence of the hypothesis (i.e. in the hypothesis not (A && (B || C) ==> D), only A and not D are considered as consequence literals).

class type simplifier = object ... end