Module LogicBuiltins

module LogicBuiltins: sig .. end
Includes

integer


module W: Wp_parameters
type category = Lang.lfun Qed.Logic.category 
type builtin = 
| ACSLDEF
| LFUN of Lang.lfun
| CONST of Lang.F.term
type kind = 
| Z (*integer*)
| R (*real*)
| I of Ctypes.c_int (*C-ints*)
| F of Ctypes.c_float (*C-floats*)
| A (*Abstract Data*)
val okind : Ctypes.c_object -> kind
val ckind : Cil_types.typ -> kind
val skind : kind -> Qed.Logic.sort
val lkind : Cil_types.logic_type -> kind
val pp_kind : Format.formatter -> kind -> unit
val pp_kinds : Format.formatter -> kind list -> unit
val pp_libs : Format.formatter -> string list -> unit
val pp_link : Format.formatter -> builtin -> unit
type sigfun = kind list * builtin 
type driver = {
   driverid : string;
   description : string;
   includes : string list;
   hlogic : (string, sigfun list) Hashtbl.t;
   hdeps : (string, string list) Hashtbl.t;
   hoptions : (string * string * string, string list) Hashtbl.t;
}
val id : driver -> string
val descr : driver -> string
val is_default : driver -> bool
val compare : driver -> driver -> int
val driver : driver Context.value
val cdriver : unit -> driver
val chop_backslash : string -> string
val lookup : string -> kind list -> builtin
val register : string -> kind list -> builtin -> unit
val iter_table : (string * kind list * builtin -> unit) -> unit
val iter_libs : (string * string list -> unit) -> unit
val dump : unit -> unit
val logic : Cil_types.logic_info -> builtin
val ctor : Cil_types.logic_ctor_info -> builtin
val constant : string -> builtin
val dependencies : string -> string list
Of external theories. Raises Not_found if undefined
val add_library : string -> string list -> unit
External theories
val add_alias : string -> kind list -> alias:string -> unit -> unit
val add_logic : kind ->
string ->
kind list ->
library:Lang.library ->
?category:Lang.lfun Qed.Logic.category ->
link:Qed.Engine.link Lang.infoprover -> unit -> unit
val add_predicate : string ->
kind list ->
library:Lang.library -> link:string Lang.infoprover -> unit -> unit
val add_ctor : string ->
kind list ->
library:Lang.library -> link:Qed.Engine.link Lang.infoprover -> unit -> unit
val add_const : string -> Lang.F.term -> unit
val add_type : string -> library:string -> ?link:string Lang.infoprover -> unit -> unit
val sanitizers : (string * string, driver_dir:string -> string -> string) Hashtbl.t
exception Unknown_option of string * string
val sanitize : driver_dir:string -> string -> string -> string -> string
type doption = string * string 
val create_option : (driver_dir:string -> string -> string) ->
string -> string -> string * string
add_option_sanitizer ~driver_dir group name add a sanitizer for group group and option name
val get_option : string * string -> library:string -> string list
return the values of option (group, name), return the empty list if not set
val set_option : driver_dir:string -> string -> string -> library:string -> string -> unit
reset and add a value to an option (group, name)
val add_option : driver_dir:string -> string -> string -> library:string -> string -> unit
add a value to an option (group, name)

Includes
val find_lib : string -> string
find a file in the includes of the current drivers
val builtin_driver : driver
val add_builtin : string -> kind list -> Lang.lfun -> unit
val new_driver : ?includes:string list -> id:string -> descr:string -> unit
reset the context to an empty driver