Newer
Older
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Eva
type mvar = Raw | Var | Ref | Caveat
type setup = {
mvar : mvar ;
mheap : mheap ;
cint : Cint.model ;
cfloat : Cfloat.model ;
}
type driver = LogicBuiltins.driver
val ident : setup -> string
val descr : setup -> string
val compiler : mheap -> mvar -> (module Sigs.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]. *)
(* -------------------------------------------------------------------------- *)