[wp] Uses Eva public API instead of Db.Value.

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

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)))
 

src/plugins/wp/wp_eva.disabled.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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

src/plugins/wp/wp_eva.enabled.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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)

src/plugins/wp/wp_eva.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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