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