Wp.LogicBuiltins
type category = Lang.lfun Qed.Logic.category
type kind =
| Z | (* integer *) |
| R | (* real *) |
| I of Ctypes.c_int | (* C-ints *) |
| F of Ctypes.c_float | (* C-floats *) |
| A | (* Abstract Data *) |
Add a new builtin. This builtin will be shared with all created drivers
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:
val id : driver -> string
val descr : driver -> string
val is_default : driver -> bool
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
add a value to an option (group, name)
reset and add a value to an option (group, name)
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
val logic : Frama_c_kernel.Cil_types.logic_info -> builtin
val ctor : Frama_c_kernel.Cil_types.logic_ctor_info -> builtin
val constant : string -> 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.