Module Wp.LogicBuiltins

type kind =
| Z(*

integer

*)
| R(*

real

*)
| I of Ctypes.c_int(*

C-ints

*)
| F of Ctypes.c_float(*

C-floats

*)
| A(*

Abstract Data

*)
val kind_of_tau : Lang.tau -> kind
val add_builtin : string -> kind list -> Lang.lfun -> unit

Add a new builtin. This builtin will be shared with all created drivers

type driver
val driver : driver Context.value
val new_driver : id:string -> ?base:driver -> ?descr:string -> ?includes:string list -> ?configure:( unit -> unit ) -> unit -> driver

Creates a configured driver from an existing one. Default:

  • base: builtin WP driver
  • descr: id
  • includes:
  • configure: No-Op The configure is the only operation allowed to modify the content of the newly created driver. Except during static initialization of builtin driver.
val id : driver -> string
val descr : driver -> string
val is_default : driver -> bool
val compare : driver -> driver -> int
val find_lib : string -> string

find a file in the includes of the current drivers

val dependencies : string -> string list

Of external theories. Raises Not_found if undefined

val add_library : string -> string list -> unit

Add a new library or update the dependencies of an existing one

val add_alias : source:Frama_c_kernel.Filepath.position -> string -> kind list -> alias:string -> unit -> unit
val add_type : ?source:Frama_c_kernel.Filepath.position -> string -> library:string -> ?link:string -> unit -> unit
val add_ctor : source:Frama_c_kernel.Filepath.position -> string -> kind list -> library:string -> link:Qed.Engine.link -> unit -> unit
val add_logic : source:Frama_c_kernel.Filepath.position -> kind -> string -> kind list -> library:string -> ?category:category -> link:Qed.Engine.link -> unit -> unit
val add_predicate : source:Frama_c_kernel.Filepath.position -> string -> kind list -> library:string -> link:string -> unit -> unit
val add_option : driver_dir:string -> string -> string -> library:string -> string -> unit

add a value to an option (group, name)

val set_option : driver_dir:string -> string -> string -> library:string -> string -> unit

reset and add a value to an option (group, name)

type doption
type sanitizer = driver_dir:string -> string -> string
val create_option : sanitizer:sanitizer -> 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

return the values of option (group, name), return the empty list if not set

type builtin =
| ACSLDEF
| LFUN of Lang.lfun
| HACK of Lang.F.term list -> Lang.F.term
val constant : string -> builtin
val lookup : string -> kind list -> builtin
val hack : string -> ( Lang.F.term list -> Lang.F.term ) -> unit

Replace a logic definition or predicate by a built-in function. The LogicSemantics compilers will replace `Pcall` and `Tcall` instances of this symbol with the provided Qed function on terms.

val hack_type : string -> ( Lang.F.tau list -> Lang.F.tau ) -> unit

Replace a logic type definition or predicate by a built-in type.

val dump : unit -> unit