Module Wp.Factory

module Factory: sig .. end

type mheap =

type mvar =

type setup = {

}

type driver = Wp.LogicBuiltins.driver

val ident : setup -> string

val descr : setup -> string

val memory : mheap -> mvar -> (module Wp.Memory.Model)

val configure : setup -> driver -> Wp.Model.tuning

val instance : setup -> driver -> Wp.Model.t

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.