Commit 0a0fa832 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] rename Model into WpContext

parent 5400738a
......@@ -1411,8 +1411,6 @@ src/plugins/wp/MemVar.mli: CEA_WP
src/plugins/wp/MemZeroAlias.ml: CEA_WP
src/plugins/wp/MemZeroAlias.mli: CEA_WP
src/plugins/wp/Sigs.ml: CEA_WP
src/plugins/wp/Model.ml: CEA_WP
src/plugins/wp/Model.mli: CEA_WP
src/plugins/wp/Mstate.ml: CEA_WP
src/plugins/wp/Mstate.mli: CEA_WP
src/plugins/wp/Partitioning.ml: CEA_WP
......@@ -1883,6 +1881,8 @@ src/plugins/wp/share/why3/frama_c_wp/vset.mlw: CEA_WP
src/plugins/wp/share/wp.driver: CEA_WP
src/plugins/wp/wpAnnot.ml: CEA_WP
src/plugins/wp/wpAnnot.mli: CEA_WP
src/plugins/wp/wpContext.ml: CEA_WP
src/plugins/wp/wpContext.mli: CEA_WP
src/plugins/wp/wpPropId.ml: CEA_WP
src/plugins/wp/wpPropId.mli: CEA_WP
src/plugins/wp/wpReport.ml: CEA_WP
......
......@@ -107,7 +107,7 @@ let op_name = function
(* --- Registry --- *)
(* -------------------------------------------------------------------------- *)
module REGISTRY = Model.Static
module REGISTRY = WpContext.Static
(struct
type key = lfun
type data = op * c_float
......
......@@ -47,7 +47,7 @@ let pretty = STR.pretty
let cluster () =
Definitions.cluster ~id:"cstring" ~title:"String Literals" ()
module LIT = Model.Generator(STR)
module LIT = WpContext.Generator(STR)
(struct
type key = cst
type data = int * F.term
......
......@@ -238,7 +238,7 @@ let rec reduce_eqcomp = function
| _::ws -> reduce_eqcomp ws
| [] -> raise Not_found
module EQARRAY = Model.Generator(Matrix.NATURAL)
module EQARRAY = WpContext.Generator(Matrix.NATURAL)
(struct
open Matrix
type key = matrix
......
......@@ -121,7 +121,7 @@ end
(* --- Registry --- *)
(* -------------------------------------------------------------------------- *)
module Cluster = Model.Index
module Cluster = WpContext.Index
(struct
type key = string
type data = cluster
......@@ -130,7 +130,7 @@ module Cluster = Model.Index
let pretty = Format.pp_print_string
end)
module Symbol = Model.Index
module Symbol = WpContext.Index
(struct
type key = lfun
type data = dfun
......@@ -139,7 +139,7 @@ module Symbol = Model.Index
let pretty = Lang.Fun.pretty
end)
module Lemma = Model.Index
module Lemma = WpContext.Index
(struct
type key = string
type data = dlemma
......@@ -178,7 +178,7 @@ let define_type c t =
end
let parameters f =
if Model.is_model_defined () then
if WpContext.is_model_defined () then
try List.map Lang.F.QED.sort_of_var (Symbol.find f).d_params
with Not_found -> []
else []
......
......@@ -130,7 +130,7 @@ struct
(** A memory model context has to be set. *)
let hypotheses () =
let kf = Model.get_scope () in
let kf = WpContext.get_scope () in
let init = match kf with
| None -> false
| Some f -> WpStrategy.is_main_init f in
......@@ -168,7 +168,7 @@ let is_formal_ptr x =
x.vformal && Cil.isPointerType x.vtype
let refusage_param ~byref ~context x =
let kf = Model.get_scope () in
let kf = WpContext.get_scope () in
let init = match kf with
| None -> false
| Some f ->
......@@ -278,7 +278,7 @@ module COMPILERS = FCMap.Make
if cmp <> 0 then cmp else LogicBuiltins.compare d d'
end)
let instances = ref (COMPILERS.empty : Model.t COMPILERS.t)
let instances = ref (COMPILERS.empty : WpContext.t COMPILERS.t)
let instance (s:setup) (d:driver) =
try COMPILERS.find (s,d) !instances
......@@ -286,14 +286,14 @@ let instance (s:setup) (d:driver) =
let id,descr = describe s in
let module CC = (val compiler s.mheap s.mvar) in
let tuning = [configure s d] in
let hypotheses kf = Model.on_scope (Some kf) CC.M.hypotheses () in
let hypotheses kf = WpContext.on_scope (Some kf) CC.M.hypotheses () in
let id,descr =
if LogicBuiltins.is_default d then id,descr
else
( id ^ "_" ^ LogicBuiltins.id d ,
descr ^ " (Driver " ^ LogicBuiltins.descr d ^ ")" )
in
let model = Model.register ~id ~descr ~tuning ~hypotheses () in
let model = WpContext.register ~id ~descr ~tuning ~hypotheses () in
instances := COMPILERS.add (s,d) model !instances ; model
let ident s = fst (describe s)
......
......@@ -39,8 +39,8 @@ type driver = LogicBuiltins.driver
val ident : setup -> string
val descr : setup -> string
val compiler : mheap -> mvar -> (module Sigs.Compiler)
val configure : setup -> driver -> Model.tuning
val instance : setup -> driver -> Model.t
val configure : setup -> driver -> WpContext.tuning
val instance : setup -> driver -> WpContext.t
val default : setup (** ["Var,Typed,Nat,Real"] memory model. *)
val parse :
?default:setup ->
......
......@@ -26,7 +26,7 @@
class type computer =
object
method model : Model.t
method model : WpContext.t
method lemma : bool
method add_strategy : WpStrategy.strategy -> unit
method add_lemma : LogicUsage.logic_lemma -> unit
......
......@@ -26,7 +26,7 @@
class type computer =
object
method model : Model.t
method model : WpContext.t
method lemma : bool
method add_strategy : WpStrategy.strategy -> unit
method add_lemma : LogicUsage.logic_lemma -> unit
......
......@@ -366,7 +366,7 @@ class pane (enabled : GuiConfig.enabled) =
let browser = self#browse in
tactic#select ~process ~composer ~browser ~tree sel
in
Model.with_model model (List.iter select) tactics ;
WpContext.with_model model (List.iter select) tactics ;
let tgt =
if List.exists (fun tactics -> tactics#targeted) tactics
then sel else Tactical.Empty in
......@@ -512,7 +512,7 @@ class pane (enabled : GuiConfig.enabled) =
self#update in
let model = ProofEngine.tree_model proof in
let print = composer#print cc ~quit in
text#printf "%t@." (Model.with_model model print) ;
text#printf "%t@." (WpContext.with_model model print) ;
text#hrule ;
text#printf "%t@."
(printer#goal (ProofEngine.head proof)) ;
......@@ -526,7 +526,7 @@ class pane (enabled : GuiConfig.enabled) =
self#update in
let model = ProofEngine.tree_model proof in
let print = browser#print cc ~quit in
text#printf "%t@." (Model.with_model model print) ;
text#printf "%t@." (WpContext.with_model model print) ;
text#hrule ;
text#printf "%t@."
(printer#goal (ProofEngine.head proof)) ;
......
......@@ -452,7 +452,7 @@ struct
(* --- Registering User-Defined Signatures --- *)
(* -------------------------------------------------------------------------- *)
module Typedefs = Model.Index
module Typedefs = WpContext.Index
(struct
type key = logic_type_info
type data = unit
......@@ -461,7 +461,7 @@ struct
let pretty = Logic_type_info.pretty
end)
module Signature = Model.Index
module Signature = WpContext.Index
(struct
type key = logic_info
type data = signature
......
......@@ -62,10 +62,10 @@ PLUGIN_CMO:= \
rformat wprop \
wp_parameters wp_error \
dyncall ctypes clabels \
MemoryContext \
Context Warning MemoryContext wpContext \
LogicUsage RefUsage \
cil2cfg normAtLabels wpPropId mcfg \
Context Warning Model Lang Repr Matrix Passive Splitter \
Lang Repr Matrix Passive Splitter \
LogicBuiltins Definitions \
Cmath Cint Cfloat Vset Vlist Region Cstring Cvalues \
Letify Cleaning \
......@@ -165,7 +165,7 @@ WP_API_BASE= \
LogicUsage.mli RefUsage.mli \
normAtLabels.mli \
wpPropId.mli mcfg.ml \
Context.mli Warning.mli Model.mli \
Context.mli Warning.mli wpContext.mli \
Lang.mli Repr.mli Passive.mli Splitter.mli \
LogicBuiltins.mli Definitions.mli \
Cint.mli Cfloat.mli Vset.mli Cstring.mli \
......
......@@ -30,8 +30,8 @@ open Lang.F
type dim = int option
type matrix = c_object * dim list
module MACHINE : Model.Key with type t = matrix
module NATURAL : Model.Key with type t = matrix
module MACHINE : WpContext.Key with type t = matrix
module NATURAL : WpContext.Key with type t = matrix
val of_array : arrayinfo -> matrix
val id : dim list -> string (** unique w.r.t [equal] *)
......
......@@ -174,7 +174,7 @@ type registered_shift =
| RS_Field of fieldinfo * term (* offset of the field *)
| RS_Shift of Z.t (* size of the element *)
module RegisterShift = Model.Static
module RegisterShift = WpContext.Static
(struct
type key = lfun
type data = registered_shift
......@@ -542,7 +542,7 @@ let cluster_memory () =
let cluster_dummy () = Definitions.cluster ~id:"dummy" ()
module ShiftFieldDef = Model.StaticGenerator(Cil_datatype.Fieldinfo)
module ShiftFieldDef = WpContext.StaticGenerator(Cil_datatype.Fieldinfo)
(struct
let name = "MemTyped.ShiftFieldDef"
type key = fieldinfo
......@@ -569,7 +569,7 @@ module ShiftFieldDef = Model.StaticGenerator(Cil_datatype.Fieldinfo)
let compile = Lang.local generate
end)
module ShiftField = Model.Generator(Cil_datatype.Fieldinfo)
module ShiftField = WpContext.Generator(Cil_datatype.Fieldinfo)
(struct
let name = "MemTyped.ShiftField"
type key = fieldinfo
......@@ -590,7 +590,7 @@ end
(* This is a model-independent generator,
which will be inherited from the model-dependent clusters *)
module ShiftGen = Model.StaticGenerator(Cobj)
module ShiftGen = WpContext.StaticGenerator(Cobj)
(struct
let name = "MemTyped.ShiftDef"
type key = c_object
......@@ -634,7 +634,7 @@ module ShiftGen = Model.StaticGenerator(Cobj)
end)
(* The model-dependent derivation of model-independent ShiftDef *)
module Shift = Model.Generator(Cobj)
module Shift = WpContext.Generator(Cobj)
(struct
let name = "MemTyped.Shift"
type key = c_object
......@@ -663,7 +663,7 @@ module EID = State_builder.Ref(Datatype.Int)
let default () = 0
end)
module STRING = Model.Generator(LITERAL)
module STRING = WpContext.Generator(LITERAL)
(struct
let name = "MemTyped.STRING"
type key = LITERAL.t
......@@ -741,7 +741,7 @@ module STRING = Model.Generator(LITERAL)
end)
module RegisterBASE = Model.Static
module RegisterBASE = WpContext.Static
(struct
type key = lfun
type data = varinfo
......@@ -749,7 +749,7 @@ module RegisterBASE = Model.Static
include Lang.Fun
end)
module BASE = Model.Generator(Varinfo)
module BASE = WpContext.Generator(Varinfo)
(struct
let name = "MemTyped.BASE"
type key = varinfo
......@@ -932,7 +932,7 @@ struct
end
module COMP = Model.Generator(Compinfo)
module COMP = WpContext.Generator(Compinfo)
(struct
let name = "MemTyped.COMP"
type key = compinfo
......@@ -964,7 +964,7 @@ module COMP = Model.Generator(Compinfo)
let compile = Lang.local generate
end)
module ARRAY = Model.Generator(Matrix.NATURAL)
module ARRAY = WpContext.Generator(Matrix.NATURAL)
(struct
open Matrix
let name = "MemTyped.ARRAY"
......
......@@ -47,7 +47,7 @@ type tree = {
mutable root : node option ; (* the root node *)
}
module PROOFS = Model.StaticGenerator(Wpo.S)
module PROOFS = WpContext.StaticGenerator(Wpo.S)
(struct
type key = Wpo.S.t
type data = tree
......
......@@ -51,8 +51,8 @@ val goto : tree -> position -> unit
val main : tree -> Wpo.t
val head : tree -> Wpo.t
val goal : node -> Wpo.t
val tree_model : tree -> Model.t
val node_model : node -> Model.t
val tree_model : tree -> WpContext.t
val node_model : node -> WpContext.t
val opened : node -> bool (** not proved *)
val proved : node -> bool (** not opened *)
......
......@@ -30,7 +30,7 @@ type status =
let files : (string,status) Hashtbl.t = Hashtbl.create 32
let filename ?(legacy=false) wpo =
let m = Model.get_id wpo.po_model in
let m = WpContext.get_id wpo.po_model in
let d = Wp_parameters.get_session_dir m in
Printf.sprintf "%s/%s.json" d (if legacy then wpo.po_leg else wpo.po_gid)
......
......@@ -32,7 +32,7 @@ open Definitions
let dkey = Wp_parameters.register_category "prover"
let cluster_file c =
let dir = Model.directory () in
let dir = WpContext.directory () in
let base = cluster_id c in
Printf.sprintf "%s/%s.v" dir base
......@@ -249,7 +249,7 @@ let need_recompile ~source ~target =
(* Used to mark version of clusters already available *)
module CLUSTERS = Model.Index
module CLUSTERS = WpContext.Index
(struct
type key = cluster
type data = int * depend list
......@@ -331,7 +331,7 @@ and assemble_coqlib coqcc c =
let assemble_goal ~pid axioms prop =
let title = Pretty_utils.to_string WpPropId.pretty pid in
let model = Model.directory () in
let model = WpContext.directory () in
let id = WpPropId.get_propid pid in
let file = Printf.sprintf "%s/%s.coq" model id in
let goal = cluster ~id ~title () in
......@@ -657,7 +657,7 @@ let prove_prop wpo ~mode ~axioms ~prop =
let model = wpo.po_model in
let script = DISK.file_goal ~pid ~model ~prover:NativeCoq in
let includes , headers , goal =
Model.with_model model (assemble_goal ~pid axioms) prop
WpContext.with_model model (assemble_goal ~pid axioms) prop
in
prove_session ~mode {
cw_pid = pid ;
......@@ -673,7 +673,7 @@ let prove_annot wpo vcq ~mode =
Task.todo
begin fun () ->
let prop =
Model.with_model wpo.po_model GOAL.compute_proof vcq.VC_Annot.goal in
WpContext.with_model wpo.po_model GOAL.compute_proof vcq.VC_Annot.goal in
prove_prop wpo ~mode ~axioms:None ~prop
end
......
......@@ -70,7 +70,7 @@ let rec locate_error files file line =
else locate_error files file (line-n)
let cluster_file c =
let dir = Model.directory () in
let dir = WpContext.directory () in
let base = cluster_id c in
Printf.sprintf "%s/%s.ergo" dir base
......@@ -89,7 +89,7 @@ let pp_depend fmt = function
Definitions.pp_cluster cluster
[@@@warning "+32"]
module TYPES = Model.Index
module TYPES = WpContext.Index
(struct
type key = adt
type data = tau
......@@ -233,7 +233,7 @@ let write_cluster c job =
begin fun fmt ->
Format.fprintf fmt "---------------------------------------------@\n" ;
Format.fprintf fmt "--- File '%s/%s.ergo' @\n"
(Model.get_id (Model.get_model ())) (cluster_id c) ;
(WpContext.get_id (WpContext.get_model ())) (cluster_id c) ;
Format.fprintf fmt "---------------------------------------------@\n" ;
Command.pp_from_file fmt f ;
end ;
......@@ -243,7 +243,7 @@ let write_cluster c job =
(* --- File Assembly --- *)
(* -------------------------------------------------------------------------- *)
module CLUSTERS = Model.Index
module CLUSTERS = WpContext.Index
(struct
type key = cluster
type data = int * depend list
......@@ -479,10 +479,10 @@ let prove_prop ~config ~pid ~mode ~model ~axioms ~prop =
let logerr = DISK.file_logerr ~pid ~model ~prover in
let id = WpPropId.get_propid pid in
let title = Pretty_utils.to_string WpPropId.pretty pid in
let lines = Model.with_model model
let lines = WpContext.with_model model
(assemble_goal ~file ~id ~title ~axioms) prop in
if Wp_parameters.has_print_generated () then
Model.with_model model (fun () ->
WpContext.with_model model (fun () ->
let goal = cluster ~id ~title () in
Wp_parameters.print_generated (cluster_file goal)
) () ;
......
......@@ -85,7 +85,7 @@ let jfork tree ?node jtactic =
let anchor = ProofEngine.anchor tree ?node () in
let goal = ProofEngine.goal anchor in
let model = ProofEngine.node_model anchor in
match Model.with_model model (jconfigure console jtactic) goal with
match WpContext.with_model model (jconfigure console jtactic) goal with
| None -> None
| Some (script,process) ->
Some (ProofEngine.fork tree ~anchor script process)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment