From 2c4c1a03dbc63dd662cfd780d444654a312ed1d9 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 23 Apr 2019 15:32:16 +0200
Subject: [PATCH] [Cil] fix the dangling reference to removed unused static
variables
Fix #624
---
src/kernel_internals/typing/rmtmps.ml | 4 +++-
tests/syntax/oracle/rmtmps_static.res.oracle | 12 ++++++++++++
tests/syntax/rmtmps_static.i | 4 ++++
3 files changed, 19 insertions(+), 1 deletion(-)
create mode 100644 tests/syntax/oracle/rmtmps_static.res.oracle
create mode 100644 tests/syntax/rmtmps_static.i
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index e22c8830104..90995963c09 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -819,7 +819,8 @@ let removeUnmarked isRoot ast reachable_tbl =
Keep variables that were already present in the code.
*)
let filterLocal local =
- if local.vtemp && not (is_reachable reachable_tbl (Var local)) then
+ if (local.vtemp || local.vstorage = Static) &&
+ not (is_reachable reachable_tbl (Var local)) then
begin
(* along the way, record the interesting locals that were removed *)
let name = local.vname in
@@ -834,6 +835,7 @@ let removeUnmarked isRoot ast reachable_tbl =
inherit Cil.nopCilVisitor
method! vblock b =
b.blocals <- List.filter filterLocal b.blocals;
+ b.bstatics <- List.filter filterLocal b.bstatics;
DoChildren
end
in
diff --git a/tests/syntax/oracle/rmtmps_static.res.oracle b/tests/syntax/oracle/rmtmps_static.res.oracle
new file mode 100644
index 00000000000..f8550f70da2
--- /dev/null
+++ b/tests/syntax/oracle/rmtmps_static.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/syntax/rmtmps_static.i (no preprocessing)
+/* Generated by Frama-C */
+int f(void);
+
+int f(void)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/rmtmps_static.i b/tests/syntax/rmtmps_static.i
new file mode 100644
index 00000000000..7f1f9625bd2
--- /dev/null
+++ b/tests/syntax/rmtmps_static.i
@@ -0,0 +1,4 @@
+int f() {
+ static int x = 0;
+ return 0;
+}
--
GitLab