sig
type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer
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 : Factory.setup -> Factory.driver -> WpContext.tuning
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