sig
  type mheap = Hoare | ZeroAlias | Region | Typed of Wp.MemTyped.pointer
  type mvar = Raw | Var | Ref | Caveat
  type setup = {
    mvar : Wp.Factory.mvar;
    mheap : Wp.Factory.mheap;
    cint : Wp.Cint.model;
    cfloat : Wp.Cfloat.model;
  }
  type driver = Wp.LogicBuiltins.driver
  val ident : Wp.Factory.setup -> string
  val descr : Wp.Factory.setup -> string
  val compiler :
    Wp.Factory.mheap -> Wp.Factory.mvar -> (module Wp.Sigs.Compiler)
  val configure_driver :
    Wp.Factory.setup -> Wp.Factory.driver -> unit -> Wp.WpContext.rollback
  val instance : Wp.Factory.setup -> Wp.Factory.driver -> Wp.WpContext.model
  val default : Wp.Factory.setup
  val parse :
    ?default:Wp.Factory.setup ->
    ?warning:(string -> unit) -> string list -> Wp.Factory.setup
end