Merge branch 'fix/cil/rmtmps-static' into 'master'

[Cil] fix the dangling reference to removed unused static variables

Closes #624

See merge request frama-c/frama-c!2242

src/kernel_internals/typing/rmtmps.ml

@@ -821,7 +821,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
@@ -836,6 +837,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

tests/syntax/oracle/rmtmps_static.res.oracle

+[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;
+}
+
+

tests/syntax/rmtmps_static.i

+int f() {
+  static int x = 0;
+  return 0;
+}