sig
type category = Wp.Lang.lfun Qed.Logic.category
type kind = Z | R | I of Wp.Ctypes.c_int | F of Wp.Ctypes.c_float | A
val kind_of_tau : Wp.Lang.tau -> Wp.LogicBuiltins.kind
val add_builtin :
string -> Wp.LogicBuiltins.kind list -> Wp.Lang.lfun -> unit
type driver
val driver : Wp.LogicBuiltins.driver Wp.Context.value
val create :
id:string ->
?descr:string -> ?includes:string list -> unit -> Wp.LogicBuiltins.driver
val init :
id:string -> ?descr:string -> ?includes:string list -> unit -> unit
val id : Wp.LogicBuiltins.driver -> string
val descr : Wp.LogicBuiltins.driver -> string
val is_default : Wp.LogicBuiltins.driver -> bool
val compare : Wp.LogicBuiltins.driver -> Wp.LogicBuiltins.driver -> int
val find_lib : string -> string
val dependencies : string -> string list
val add_library : string -> string list -> unit
val add_alias :
source:Filepath.position ->
string -> Wp.LogicBuiltins.kind list -> alias:string -> unit -> unit
val add_type :
source:Filepath.position ->
string ->
library:string -> ?link:string Wp.Lang.infoprover -> unit -> unit
val add_ctor :
source:Filepath.position ->
string ->
Wp.LogicBuiltins.kind list ->
library:string -> link:Qed.Engine.link Wp.Lang.infoprover -> unit -> unit
val add_logic :
source:Filepath.position ->
Wp.LogicBuiltins.kind ->
string ->
Wp.LogicBuiltins.kind list ->
library:string ->
?category:Wp.LogicBuiltins.category ->
link:Qed.Engine.link Wp.Lang.infoprover -> unit -> unit
val add_predicate :
source:Filepath.position ->
string ->
Wp.LogicBuiltins.kind list ->
library:string -> link:string Wp.Lang.infoprover -> unit -> unit
val add_option :
driver_dir:string -> string -> string -> library:string -> string -> unit
val set_option :
driver_dir:string -> string -> string -> library:string -> string -> unit
type doption
type sanitizer = driver_dir:string -> string -> string
val create_option :
sanitizer:Wp.LogicBuiltins.sanitizer ->
string -> string -> Wp.LogicBuiltins.doption
val get_option : Wp.LogicBuiltins.doption -> library:string -> string list
type builtin =
ACSLDEF
| LFUN of Wp.Lang.lfun
| HACK of (Wp.Lang.F.term list -> Wp.Lang.F.term)
val logic : Cil_types.logic_info -> Wp.LogicBuiltins.builtin
val ctor : Cil_types.logic_ctor_info -> Wp.LogicBuiltins.builtin
val constant : string -> Wp.LogicBuiltins.builtin
val lookup :
string -> Wp.LogicBuiltins.kind list -> Wp.LogicBuiltins.builtin
val hack : string -> (Wp.Lang.F.term list -> Wp.Lang.F.term) -> unit
val dump : unit -> unit
end