Frama-C:
Plug-ins:
Libraries:

Frama-C API - Factory

type mheap =
  1. | Hoare
  2. | ZeroAlias
  3. | Eva
  4. | Bytes
  5. | Region
  6. | Typed of MemTyped.pointer
type mvar =
  1. | Raw
  2. | Var
  3. | Ref
  4. | Caveat
type setup = {
  1. mvar : mvar;
  2. mheap : mheap;
  3. cint : Cint.model;
  4. cfloat : Cfloat.model;
}
type driver = LogicBuiltins.driver
val ident : setup -> string
val descr : setup -> string
val compiler : mheap -> mvar -> (module Memory.Compiler)
val configure_driver : setup -> driver -> unit -> WpContext.rollback
val instance : setup -> driver -> 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.