From a0a0e42365c121940d7c004059d21d9a17e6ea1f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 19 Jul 2022 16:17:51 +0200
Subject: [PATCH] [wp] Uses Eva public API instead of Db.Value.
---
src/plugins/wp/MemVal.ml | 6 +++---
src/plugins/wp/dune | 5 ++++-
src/plugins/wp/wp_eva.disabled.ml | 24 ++++++++++++++++++++++++
src/plugins/wp/wp_eva.enabled.ml | 24 ++++++++++++++++++++++++
src/plugins/wp/wp_eva.mli | 24 ++++++++++++++++++++++++
5 files changed, 79 insertions(+), 4 deletions(-)
create mode 100644 src/plugins/wp/wp_eva.disabled.ml
create mode 100644 src/plugins/wp/wp_eva.enabled.ml
create mode 100644 src/plugins/wp/wp_eva.mli
diff --git a/src/plugins/wp/MemVal.ml b/src/plugins/wp/MemVal.ml
index aeecf7e8482..079ea9dfb0d 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 58e1f4bfe1d..df0f83e4e75 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 00000000000..5385f2767e3
--- /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 00000000000..c9e22797dad
--- /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 00000000000..e8fa5ede41c
--- /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
--
GitLab