diff --git a/src/plugins/wp/MemVal.ml b/src/plugins/wp/MemVal.ml
index aeecf7e84820410826c9442ad442f23a165461ed..079ea9dfb0d8c1ef845d1ca58e1ec741e11d9552 100644
--- a/src/plugins/wp/MemVal.ml
+++ b/src/plugins/wp/MemVal.ml
@@ -768,7 +768,7 @@ struct
let datatype = "Eva"
let configure () =
- if not (Db.Value.is_computed ()) then
+ if not (Wp_eva.is_computed ()) then
Wp_parameters.abort ~current:true
"Could not use Eva memory model without a previous run of the analysis.";
(fun () -> ())
@@ -780,8 +780,8 @@ struct
let bottom = Model.bottom
let join = Model.join
- let of_kinstr k = Db.Value.get_state k
- let of_stmt k = Db.Value.get_stmt_state k
+ let of_kinstr k = Wp_eva.get_cvalue_state k
+ let of_stmt s = Wp_eva.get_cvalue_state (Kstmt s)
let of_kf kf =
let state = ref bottom in
let vis = object
diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune
index 58e1f4bfe1d73de49ba16363acf1a9b0ac91ddd4..df0f83e4e75f233dbdd4eb885012f01020dbb0ca 100644
--- a/src/plugins/wp/dune
+++ b/src/plugins/wp/dune
@@ -40,7 +40,10 @@
frama-c.kernel
frama-c-rtegen.core
frama-c-server.core
- qed why3 zarith ocamlgraph))
+ qed why3 zarith ocamlgraph
+ (select wp_eva.ml from
+ (frama-c-eva.core -> wp_eva.enabled.ml)
+ ( -> wp_eva.disabled.ml))))
(plugin (optional) (name wp) (libraries frama-c-wp.core) (site (frama-c plugins)))
diff --git a/src/plugins/wp/wp_eva.disabled.ml b/src/plugins/wp/wp_eva.disabled.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5385f2767e3067848660023bacbdd97e9d8def1e
--- /dev/null
+++ b/src/plugins/wp/wp_eva.disabled.ml
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let is_computed () = false
+let get_cvalue_state kinstr = Cvalue.Model.top
diff --git a/src/plugins/wp/wp_eva.enabled.ml b/src/plugins/wp/wp_eva.enabled.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c9e22797dad7ed2acdcec48f0b27609291766548
--- /dev/null
+++ b/src/plugins/wp/wp_eva.enabled.ml
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let is_computed = Eva.Analysis.is_computed
+let get_cvalue_state kinstr = Eva.Results.(before_kinstr kinstr |> get_cvalue_model)
diff --git a/src/plugins/wp/wp_eva.mli b/src/plugins/wp/wp_eva.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e8fa5ede41c9ef5f1fdeee15083a02748ba156b6
--- /dev/null
+++ b/src/plugins/wp/wp_eva.mli
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val is_computed: unit -> bool
+val get_cvalue_state: Cil_types.kinstr -> Cvalue.Model.t