Wp.Lang
Low-Level Logic Terms and Predicates
Logic Language based on Qed
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
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
*)| Wtype of string list * string * string list
Why3 imported type
*)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_link : 'a;
ext_library : library;
a library which it depends on
*)ext_debug : string;
just for printing during debugging
*)}
and field = private
| Mfield of mdt * fields * string * tau
| Cfield of Frama_c_kernel.Cil_types.fieldinfo * datakind
and tau = (field, 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
*)| FUN of lsymbol
External or Generated logic symbol
*)and lsymbol = {
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
| Wsymbol of string list * string * string list
Why3 imported logic symbol
*)val is_builtin : Frama_c_kernel.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 comp : Frama_c_kernel.Cil_types.compinfo -> adt
val comp_init : Frama_c_kernel.Cil_types.compinfo -> adt
val cfield : ?kind:datakind -> Frama_c_kernel.Cil_types.fieldinfo -> field
val atype : Frama_c_kernel.Cil_types.logic_type_info -> tau list -> tau
val adt : Frama_c_kernel.Cil_types.logic_type_info -> adt
Must not be a builtin
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 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 imported_t :
package:string list ->
theory:string ->
name:string list ->
adt
val imported_f :
package:string list ->
theory:string ->
name:string list ->
?params:Qed.Logic.sort list ->
?result:Qed.Logic.sort ->
?typecheck:(tau option list -> tau) ->
unit ->
lfun
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 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 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 context_of_lfun : lfun -> WpContext.context option
LFuns are unique by name and context
val is_coloring_lfun : lfun -> bool
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
val assume : F.pred -> unit
val get_pool : unit -> F.pool
val get_gamma : unit -> gamma
val get_hypotheses : unit -> F.pred list
val sigma : unit -> F.sigma
uses current pool
val alpha : unit -> F.sigma
freshen all variables
val is_literal : F.term -> bool
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