Lang (frama-c-wp.Wp.Lang)

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 type_id : Frama_c_kernel.Cil_types.logic_type_info -> string

val logic_id : Frama_c_kernel.Cil_types.logic_info -> string

val ctor_id : Frama_c_kernel.Cil_types.logic_ctor_info -> string

val lemma_id : string -> string

Symbols

type adt = private

| Qdata of Qed.Symbol.data
(*
Qed/Why3 Type
*)
| Atype of Frama_c_kernel.Cil_types.logic_type_info
(*
ACSL Logic Type
*)

A type is never registered in a Definition.t

and field = Qed.Symbol.field

and tau = adt Qed.Logic.datatype

type lfun = private

| ACSL of Frama_c_kernel.Cil_types.logic_info
(*
Registered in Definition.t only
*)
| CTOR of Frama_c_kernel.Cil_types.logic_ctor_info
(*
Not registered in Definition.t directly converted/printed
*)
| LFUN of lsymbol
(*
Generated logic symbol
*)
| QFUN of esymbol
(*
External logic symbol
*)

and lsymbol = {

m_name : string;
m_context : WpContext.context option;
m_category : lfun Qed.Logic.category;
m_coloring : bool;
m_result : tau;
m_params : tau list;

}

and esymbol = {

e_category : lfun Qed.Logic.category;
e_coloring : bool;
e_symbol : Qed.Symbol.lfun;

}

val atype : Frama_c_kernel.Cil_types.logic_type_info -> tau list -> tau

val on_lfun : (lfun -> unit) -> unit

val on_field : (field -> unit) -> unit

val acsl : Frama_c_kernel.Cil_types.logic_info -> lfun

val ctor : Frama_c_kernel.Cil_types.logic_ctor_info -> lfun

val fields : adt -> field list

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_ltype : Frama_c_kernel.Cil_types.logic_type -> tau

val tau_of_return : Frama_c_kernel.Cil_types.logic_type option -> tau

val tau_of_lfun : lfun -> tau option list -> tau

val tau_of_field : 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_comp : Frama_c_kernel.Cil_types.compinfo -> tau

val t_init : Frama_c_kernel.Cil_types.compinfo -> 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_qdata : Qed.Symbol.data -> 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 datakind =

| KValue
| KInit

val comp : (datakind -> Frama_c_kernel.Cil_types.compinfo -> tau) Context.value

val field : 
  (datakind -> Frama_c_kernel.Cil_types.fieldinfo -> field) Context.value

val cfield : ?kind:datakind -> Frama_c_kernel.Cil_types.fieldinfo -> field

val fields_of_field : field -> field list

val fields_of_adt : adt -> field list

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