Previous  Up  Next

Module Wp.Factory

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