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