Module Wp.Lang

Low-Level Logic Terms and Predicates

Logic Language based on Qed

Library

type library = string

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 =
| KValue
| KInit
type adt = private
| Mtype of mdt(*

External type

*)
| Mrecord of mdt * fields(*

External record-type

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

Logic Type

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

C-code struct or union

*)

A type is never registered in a Definition.t

and mdt = string extern

name to print to the provers

and 'a extern = {
ext_id : int;
ext_library : library;(*

a library which it depends on

*)
ext_debug : string;(*

just for printing during debugging

*)
}
and fields = {
mutable fields : field list;
}
and field =
| Mfield of mdt * fields * string * tau
| Cfield of Frama_c_kernel.Cil_types.fieldinfo * datakind
type t_builtin =
| E_mdt of mdt
| E_poly of tau list -> tau
type lfun =
| 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

*)
| Model of model
and model = {
m_category : lfun Qed.Logic.category;
m_params : Qed.Logic.sort list;
m_result : Qed.Logic.sort;
m_typeof : tau option list -> tau;
m_source : source;
m_coloring : bool;
}
and source =
| Generated of WpContext.context option * string
| Extern of Qed.Engine.link extern
val mem_builtin_type : name:string -> bool
val is_builtin_type : name:string -> tau -> bool
val get_builtin_type : name:string -> adt
val datatype : library:string -> string -> adt
val record : link:string -> library:string -> (string * tau) list -> adt
val field : adt -> string -> field
val fields_of_adt : adt -> field list
val fields_of_tau : tau -> field list
val fields_of_field : field -> field list

Must not be a builtin

type balance =
| Nary
| Left
| Right
val extern_s : library:library -> ?link:Qed.Engine.link -> ?category:lfun Qed.Logic.category -> ?params:Qed.Logic.sort list -> ?sort:Qed.Logic.sort -> ?result:tau -> ?coloring:bool -> ?typecheck:( tau option list -> tau ) -> string -> lfun
val extern_f : library:library -> ?link:Qed.Engine.link -> ?balance:balance -> ?category:lfun Qed.Logic.category -> ?params:Qed.Logic.sort list -> ?sort:Qed.Logic.sort -> ?result:tau -> ?coloring:bool -> ?typecheck:( tau option list -> tau ) -> ( 'a, Stdlib.Format.formatter, unit, lfun ) Stdlib.format4 -> 'a

balance just give a default when link is not specified

val extern_p : library:library -> ?bool:string -> ?prop:string -> ?link:Qed.Engine.link -> ?params:Qed.Logic.sort list -> ?coloring:bool -> unit -> lfun
val extern_fp : library:library -> ?params:Qed.Logic.sort list -> ?link:string -> ?coloring:bool -> string -> lfun
val generated_f : ?context:bool -> ?category:lfun Qed.Logic.category -> ?params:Qed.Logic.sort list -> ?sort:Qed.Logic.sort -> ?result:tau -> ?coloring:bool -> ( 'a, Stdlib.Format.formatter, unit, lfun ) Stdlib.format4 -> 'a
val generated_p : ?context:bool -> ?coloring:bool -> string -> lfun
val extern_t : string -> link:string -> library:library -> mdt

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_lfun : lfun -> tau option list -> tau
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_datatype : 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 builtin_types : ( string -> t_builtin ) Context.value
val parameters : ( lfun -> Qed.Logic.sort list ) -> unit

definitions

val name_of_lfun : lfun -> string
val name_of_field : field -> string
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

Simplifiers

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

iter_consequence_literals assume_from_litteral hypothesis applies the function assume_from_litteral 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
module For_export : sig ... end

For why3_api but circular dependency