module Lang:sig
..end
Logic Language based on Qed
val basename : string -> string -> string
val avoid_leading_backlash : string -> string
val comp_id : Cil_types.compinfo -> string
val field_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 'a
infoprover = {
|
altergo : |
|
why3 : |
|
coq : |
val infoprover : 'a -> 'a infoprover
val map_infoprover : ('a -> 'b) -> 'a infoprover -> 'b infoprover
typelibrary =
string
type
adt =
| |
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
a library which it depends on | *) |
|
ext_debug : |
(* |
just for printing during debugging
just for printing during debugging | *) |
type
fields = {
|
mutable fields : |
type
field =
| |
Mfield of |
| |
Cfield of |
typetau =
(field, adt) Qed.Logic.datatype
val pointer : (Cil_types.typ -> tau) Context.value
val new_extern_id : int Pervasives.ref
val new_extern : debug:string ->
library:library -> link:'a infoprover -> 'a extern
val ext_compare : 'a extern -> 'b extern -> int
val sort_of_object : Ctypes.c_object -> Qed.Logic.sort
val sort_of_ctype : Cil_types.typ -> Qed.Logic.sort
val sort_of_ltype : Cil_types.logic_type -> Qed.Logic.sort
val tau_of_comp : Cil_types.compinfo -> ('a, adt) Qed.Logic.datatype
val array : ('a, 'b) Qed.Logic.datatype -> ('a, 'b) Qed.Logic.datatype
val farray : ('a, 'b) Qed.Logic.datatype ->
('a, 'b) Qed.Logic.datatype -> ('a, 'b) Qed.Logic.datatype
val tau_of_object : Ctypes.c_object -> tau
val tau_of_ctype : Cil_types.typ -> tau
val poly : string list Context.value
val varpoly : int -> string -> string list -> int
val builtins : (string, mdt) Hashtbl.t
val tau_of_ltype : Cil_types.logic_type -> tau
val tau_of_return : Cil_types.logic_info -> tau
module ADT:sig
..end
val atype : Cil_types.logic_type_info -> adt
val builtin_type : name:string -> link:string infoprover -> library:library -> unit
val datatype : library:library -> string -> adt
val record : link:string infoprover ->
library:library -> (string * tau) list -> adt
val field : adt -> string -> field
val comp : Cil_types.compinfo -> adt
val fields_of_tau : ('a, adt) Qed.Logic.datatype -> field list
val fields_of_field : field -> field list
val tau_of_field : field -> tau
val tau_of_record : field -> ('a, adt) Qed.Logic.datatype
module Field:sig
..end
type
lfun =
| |
ACSL of |
(* |
Registered in Definition.t,
only
Registered in Definition.t,
only | *) |
| |
CTOR of |
(* |
Not registered in Definition.t
directly converted/printed
Not registered in Definition.t
directly converted/printed | *) |
| |
Model of |
(* | *) |
type
model = {
|
m_category : |
|
m_params : |
|
m_resort : |
|
m_result : |
|
m_source : |
type
source =
| |
Generated of |
| |
Extern of |
val tau_of_lfun : lfun -> tau
type
balance =
| |
Nary |
| |
Left |
| |
Right |
type 'a
linkinfo = {
|
mutable thdep : |
|
mutable link : |
val symbolf : ?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 ->
('a, Format.formatter, unit, lfun) Pervasives.format4 -> 'a
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 -> 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 ->
('a, Format.formatter, unit, lfun) Pervasives.format4 -> 'a
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 : ?category:lfun Qed.Logic.category ->
?params:Qed.Logic.sort list ->
?sort:Qed.Logic.sort ->
?result:tau ->
('a, Format.formatter, unit, lfun) Pervasives.format4 -> 'a
val generated_p : string -> lfun
val constructor : Cil_types.logic_ctor_info -> lfun
val logic_info : Cil_types.logic_info -> lfun
module Fun:sig
..end
val parameters : (lfun -> Qed.Logic.sort list) -> unit
class virtual idprinting :object
..end
module F:sig
..end
type
gamma = {
|
mutable hyps : |
|
mutable vars : |
val cpool : F.pool Context.value
val cgamma : gamma Context.value
val apool : F.pool option -> F.pool
val agamma : gamma option -> gamma
val new_pool : ?copy:F.pool -> unit -> F.pool
val new_gamma : ?copy:gamma -> unit -> gamma
val get_pool : unit -> F.pool
val get_gamma : unit -> gamma
val freshvar : ?basename:string -> F.tau -> F.var
val freshen : F.var -> F.var
val local : ?pool:F.pool -> ?gamma:gamma -> ('a -> 'b) -> 'a -> 'b
val masked : bool Pervasives.ref
val without_assume : ('a -> 'b) -> 'a -> 'b
val assume : F.term -> unit
val epsilon : ?basename:string -> F.tau -> (F.term -> F.pred) -> F.term
val hypotheses : gamma -> F.pred list
val variables : gamma -> F.var list
val get_hypotheses : unit -> F.pred list
val get_variables : unit -> F.var list
module Alpha:sig
..end