Module Factory

module Factory: sig .. end

type mheap = 
| Hoare
| Typed of MemTyped.pointer
type mvar = 
| Raw
| Var
| Ref
type setup = {
   mvar : mvar;
   mheap : mheap;
   cint : Cint.model;
   cfloat : Cfloat.model;
}
type driver = LogicBuiltins.driver 
val main : Buffer.t * Buffer.t -> string -> unit
val add : Buffer.t * Buffer.t -> string -> unit
val descr_mtyped : Buffer.t * Buffer.t -> MemTyped.pointer -> unit
val descr_mheap : Buffer.t * Buffer.t -> mheap -> unit
val descr_mvar : Buffer.t * Buffer.t -> mvar -> unit
val descr_cint : Buffer.t * Buffer.t -> Cint.model -> unit
val descr_cfloat : Buffer.t * Buffer.t -> Cfloat.model -> unit
val descr_setup : setup -> string * string
val descriptions : (setup, string * string) Hashtbl.t
val descr : setup -> string
module VarHoare: sig .. end
module VarRef0: sig .. end
module VarRef2: sig .. end
module MHoareVar: MemVar.Make(VarHoare)(MemEmpty)
module MHoareRef: MemVar.Make(VarRef2)(MemEmpty)
module MTypedVar: MemVar.Make(VarRef0)(MemTyped)
module MTypedRef: MemVar.Make(VarRef2)(MemTyped)
module WP_HoareVar: CfgWP.Computer(MHoareVar)
module WP_HoareRef: CfgWP.Computer(MHoareRef)
module WP_TypedRaw: CfgWP.Computer(MemTyped)
module WP_TypedVar: CfgWP.Computer(MTypedVar)
module WP_TypedRef: CfgWP.Computer(MTypedRef)
val wp : setup -> Model.t -> Generator.computer
val configure_mheap : mheap -> unit
val configure : setup -> driver -> unit -> unit
module MODEL: FCMap.Make(sig
type t = Factory.setup * Factory.driver 
val compare : 'a * LogicBuiltins.driver -> 'a * LogicBuiltins.driver -> int
end)
type instance = {
   model : Model.t;
   driver : LogicBuiltins.driver;
}
val instances : instance MODEL.t Pervasives.ref
val instance : setup -> driver -> instance
val ident : setup -> string
val descr : setup -> string
val computer : setup -> driver -> Generator.computer
val split : string -> string list
val update_config : string -> setup -> string -> setup
val apply_config : setup -> string -> setup
val parse : string list -> setup