sig
type mheap =
Hoare
| ZeroAlias
| Region
| Typed of Wp.MemTyped.pointer
| Eva
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