module Factory: sig
.. end
"Var,Typed,Nat,Real"
memory model.
type
mheap =
type
mvar =
| |
Raw |
| |
Var |
| |
Ref |
| |
Caveat |
type
setup = {
}
type
driver = LogicBuiltins.driver
val ident : setup -> string
val descr : setup -> string
val compiler : mheap -> mvar -> (module Sigs.Compiler)
val configure : setup -> driver -> WpContext.tuning
val instance : setup -> driver -> WpContext.model
val default : setup
"Var,Typed,Nat,Real"
memory model.
val parse : ?default:setup ->
?warning:(string -> unit) -> string list -> setup
Apply specifications to default setup.
Default setup is Factory.default
.
Default warning is Wp_parameters.abort
.