sig
type category = Lang.lfun Qed.Logic.category
type kind = Z | R | I of Ctypes.c_int | F of Ctypes.c_float | A
val kind_of_tau : Lang.tau -> LogicBuiltins.kind
val add_builtin : string -> LogicBuiltins.kind list -> Lang.lfun -> unit
type driver
val driver : LogicBuiltins.driver Context.value
val new_driver :
id:string ->
?base:LogicBuiltins.driver ->
?descr:string ->
?includes:string list ->
?configure:(unit -> unit) -> unit -> LogicBuiltins.driver
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 :
source:Filepath.position ->
string -> LogicBuiltins.kind list -> alias:string -> unit -> unit
val add_type :
?source:Filepath.position ->
string -> library:string -> ?link:string -> unit -> unit
val add_ctor :
source:Filepath.position ->
string ->
LogicBuiltins.kind list ->
library:string -> link:Qed.Engine.link -> unit -> unit
val add_logic :
source:Filepath.position ->
LogicBuiltins.kind ->
string ->
LogicBuiltins.kind list ->
library:string ->
?category:LogicBuiltins.category -> link:Qed.Engine.link -> unit -> unit
val add_predicate :
source:Filepath.position ->
string ->
LogicBuiltins.kind list -> library:string -> link:string -> 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:LogicBuiltins.sanitizer ->
string -> string -> LogicBuiltins.doption
val get_option : LogicBuiltins.doption -> library:string -> string list
type builtin =
ACSLDEF
| LFUN of Lang.lfun
| HACK of (Lang.F.term list -> Lang.F.term)
val logic : Cil_types.logic_info -> LogicBuiltins.builtin
val ctor : Cil_types.logic_ctor_info -> LogicBuiltins.builtin
val constant : string -> LogicBuiltins.builtin
val lookup : string -> LogicBuiltins.kind list -> LogicBuiltins.builtin
val hack : string -> (Lang.F.term list -> Lang.F.term) -> unit
val hack_type : string -> (Lang.F.tau list -> Lang.F.tau) -> unit
val dump : unit -> unit
end