module LogicBuiltins:sig
..end
Includes
typecategory =
Lang.lfun Qed.Logic.category
type
kind =
| |
Z |
(* |
integer
| *) |
| |
R |
(* |
real
| *) |
| |
I of |
(* |
C-ints
| *) |
| |
F of |
(* |
C-floats
| *) |
| |
A |
(* |
Abstract Data
| *) |
type
driver
val driver : driver Context.value
val new_driver : ?includes:string list -> id:string -> descr:string -> unit
val id : driver -> string
val descr : driver -> string
val is_default : driver -> bool
val compare : driver -> driver -> int
val find_lib : string -> string
val dependencies : string -> string list
val add_library : string -> string list -> unit
val add_builtin : string -> kind list -> Lang.lfun -> unit
val add_alias : string -> kind list -> alias:string -> unit -> unit
val add_type : string -> library:string -> ?link:string Lang.infoprover -> unit -> unit
val add_ctor : string ->
kind list ->
library:string -> link:Qed.Engine.link Lang.infoprover -> unit -> unit
val add_logic : kind ->
string ->
kind list ->
library:string ->
?category:category ->
link:Qed.Engine.link Lang.infoprover -> unit -> unit
val add_predicate : string ->
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 -> doption
add_option_sanitizer ~driver_dir group name
add a sanitizer for group group
and option name
val get_option : doption -> library:string -> string list
type
builtin =
| |
ACSLDEF |
| |
LFUN of |
val logic : Cil_types.logic_info -> builtin
val ctor : Cil_types.logic_ctor_info -> builtin
val constant : string -> builtin
val dump : unit -> unit