Module Wp.Definitions

Generated Logic Definitions

type cluster
val dummy : unit -> cluster
val cluster : id:string -> ?title:string -> ?position:Frama_c_kernel.Filepath.position -> unit -> cluster
val axiomatic : LogicUsage.axiomatic -> 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 cluster_compare : cluster -> cluster -> int
val pp_cluster : Stdlib.Format.formatter -> cluster -> unit
val iter : ( cluster -> unit ) -> unit
type dlemma = {
l_name : string;
l_cluster : cluster;
l_kind : Frama_c_kernel.Cil_types.predicate_kind;
l_types : int;
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
and recursion =
| Def
| Rec
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 find_symbol : Lang.lfun -> dfun
  • raises Not_found

    if symbol is not compiled (yet)

val define_symbol : dfun -> unit
val update_symbol : dfun -> unit
val find_name : string -> dlemma
val find_lemma : LogicUsage.logic_lemma -> dlemma
  • raises Not_found

    if lemma is not compiled (yet)

val compile_lemma : ( LogicUsage.logic_lemma -> dlemma ) -> LogicUsage.logic_lemma -> unit
val define_lemma : dlemma -> 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
class virtual visitor : cluster -> object ... end