module Lang:sig
..end
Logic Language based on Qed
typelibrary =
string
type 'a
infoprover = {
|
altergo : |
|
why3 : |
|
coq : |
Name for external prover.
In case a Qed.Engine.link is used, F_subst
patterns
are not supported for Why-3.
generic way to have different informations for the provers
val infoprover : 'a -> 'a infoprover
same information for all the provers
Unique identifiers.
val comp_id : Cil_types.compinfo -> string
val comp_init_id : Cil_types.compinfo -> string
val field_id : Cil_types.fieldinfo -> string
val field_init_id : Cil_types.fieldinfo -> string
val type_id : Cil_types.logic_type_info -> string
val logic_id : Cil_types.logic_info -> string
val ctor_id : Cil_types.logic_ctor_info -> string
val lemma_id : string -> string
type
datakind =
| |
KValue |
| |
KInit |
type
adt = private
| |
Mtype of |
(* | External type | *) |
| |
Mrecord of |
(* | External record-type | *) |
| |
Atype of |
(* | Logic Type | *) |
| |
Comp of |
(* | C-code struct or union | *) |
typemdt =
string extern
name to print to the provers
type 'a
extern = {
|
ext_id : |
|||
|
ext_link : |
|||
|
ext_library : |
(* | a library which it depends on | *) |
|
ext_debug : |
(* | just for printing during debugging | *) |
type
fields = {
|
mutable fields : |
type
field =
| |
Mfield of |
| |
Cfield of |
typetau =
(field, adt) Qed.Logic.datatype
type
t_builtin =
| |
E_mdt of |
| |
E_poly of |
type
lfun =
| |
ACSL of |
(* | Registered in Definition.t, only | *) |
| |
CTOR of |
(* | Not registered in Definition.t directly converted/printed | *) |
| |
Model of |
type
model = {
|
m_category : |
|
m_params : |
|
m_result : |
|
m_typeof : |
|
m_source : |
type
source =
| |
Generated of |
| |
Extern of |
val mem_builtin_type : name:string -> bool
val is_builtin : Cil_types.logic_type_info -> 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 infoprover ->
library:string -> (string * tau) list -> adt
val comp : Cil_types.compinfo -> adt
val comp_init : Cil_types.compinfo -> 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
val atype : Cil_types.logic_type_info -> tau list -> tau
val adt : Cil_types.logic_type_info -> adt
Must not be a builtin
type
balance =
| |
Nary |
| |
Left |
| |
Right |
val extern_s : library:library ->
?link:Qed.Engine.link infoprover ->
?category:lfun Qed.Logic.category ->
?params:Qed.Logic.sort list ->
?sort:Qed.Logic.sort ->
?result:tau ->
?typecheck:(tau option list -> tau) -> string -> lfun
val extern_f : library:library ->
?link:Qed.Engine.link infoprover ->
?balance:balance ->
?category:lfun Qed.Logic.category ->
?params:Qed.Logic.sort list ->
?sort:Qed.Logic.sort ->
?result:tau ->
?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 infoprover ->
?params:Qed.Logic.sort list -> unit -> lfun
val extern_fp : library:library ->
?params:Qed.Logic.sort list ->
?link:string infoprover -> string -> lfun
val generated_f : ?context:bool ->
?category:lfun Qed.Logic.category ->
?params:Qed.Logic.sort list ->
?sort:Qed.Logic.sort ->
?result:tau ->
('a, Stdlib.Format.formatter, unit, lfun) Stdlib.format4 -> 'a
val generated_p : ?context:bool -> string -> lfun
val extern_t : string ->
link:string infoprover -> library:library -> mdt
val tau_of_object : Wp.Ctypes.c_object -> tau
val tau_of_ctype : Cil_types.typ -> tau
val tau_of_ltype : Cil_types.logic_type -> tau
val tau_of_return : Cil_types.logic_info -> 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 : Wp.Ctypes.c_object -> tau
val init_of_ctype : 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 : Cil_types.compinfo -> tau
val t_init : Cil_types.compinfo -> tau
val t_float : Wp.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 Wp.Context.value
type of pointers
val floats : (Wp.Ctypes.c_float -> tau) Wp.Context.value
type of floats
val poly : string list Wp.Context.value
polymorphism
val builtin_types : (string -> t_builtin) Wp.Context.value
val parameters : (lfun -> Qed.Logic.sort list) -> unit
definitions
val name_of_lfun : lfun -> string
val name_of_field : field -> string
module ADT:Logic.Data
with type t = adt
module Field:Logic.Field
with type t = field
module Fun:Logic.Function
with type t = lfun
class virtual idprinting :object
..end
module F:sig
..end
module N:sig
..end
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
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
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