Wp.Definitions
Generated Logic Definitions
val dummy : unit -> cluster
val cluster :
id:string ->
?title:string ->
?position:Frama_c_kernel.Filepath.position ->
unit ->
cluster
val axiomatic : LogicUsage.axiomatic -> cluster
val section : LogicUsage.logic_section -> cluster
val compinfo : Frama_c_kernel.Cil_types.compinfo -> cluster
val matrix : unit -> cluster
val cluster_id : cluster -> string
Unique
val cluster_title : cluster -> string
val cluster_position : cluster -> Frama_c_kernel.Filepath.position option
val cluster_age : cluster -> int
val pp_cluster : Stdlib.Format.formatter -> cluster -> unit
val iter : (cluster -> unit) -> unit
type trigger = (Lang.F.var, Lang.lfun) Qed.Engine.ftrigger
type typedef = (Lang.F.tau, Lang.field, Lang.lfun) Qed.Engine.ftypedef
type dlemma = {
l_name : string;
l_cluster : cluster;
l_kind : Frama_c_kernel.Cil_types.predicate_kind;
l_forall : Lang.F.var list;
l_triggers : trigger list list;
OR of AND-triggers
*)l_lemma : Lang.F.pred;
}
type definition =
| Logic of Lang.F.tau
| Function of Lang.F.tau * recursion * Lang.F.term
| Predicate of recursion * Lang.F.pred
| Inductive of dlemma list
type dfun = {
d_lfun : Lang.lfun;
d_cluster : cluster;
d_types : int;
d_params : Lang.F.var list;
d_definition : definition;
}
module Trigger : sig ... end
val is_empty : cluster -> bool
val pp_record :
Stdlib.Format.formatter ->
Frama_c_kernel.Cil_types.compinfo ->
unit
val pp_irecord :
Stdlib.Format.formatter ->
Frama_c_kernel.Cil_types.compinfo ->
unit
val pp_typedef :
Stdlib.Format.formatter ->
Frama_c_kernel.Cil_types.logic_type_info ->
unit
val pp_dfun : Stdlib.Format.formatter -> dfun -> unit
val pp_trigger : Stdlib.Format.formatter -> trigger -> unit
val pp_lemma : Stdlib.Format.formatter -> dlemma -> unit
val dump : Stdlib.Format.formatter -> cluster -> unit
val define_symbol : dfun -> unit
val update_symbol : dfun -> unit
val find_name : string -> dlemma
val find_lemma : LogicUsage.logic_lemma -> dlemma
val compile_lemma :
(LogicUsage.logic_lemma -> dlemma) ->
LogicUsage.logic_lemma ->
unit
val define_lemma : dlemma -> unit
val define_type : cluster -> Frama_c_kernel.Cil_types.logic_type_info -> unit
val call_fun :
result:Lang.F.tau ->
Lang.lfun ->
(Lang.lfun -> dfun) ->
Lang.F.term list ->
Lang.F.term
val call_pred :
Lang.lfun ->
(Lang.lfun -> dfun) ->
Lang.F.term list ->
Lang.F.pred
type axioms = cluster * LogicUsage.logic_lemma list