module Factory: sig
.. end
type
mheap =
type
mvar =
type
setup = {
}
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
end
)
type
instance = {
}
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