From 61869eecdc52c13b97f22a5aeec799e216d45834 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 11 Mar 2019 19:16:01 +0100
Subject: [PATCH] [kernel] keep appropriate information about used suffixes in
alpha conv tables
---
src/kernel_internals/typing/alpha.ml | 5 ++++-
src/kernel_internals/typing/cabs2cil.ml | 15 ++++++++++++++-
tests/syntax/rename.i | 14 ++++++++++++++
3 files changed, 32 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/alpha.ml b/src/kernel_internals/typing/alpha.ml
index fd3269331a1..66f32b2e3e9 100644
--- a/src/kernel_internals/typing/alpha.ml
+++ b/src/kernel_internals/typing/alpha.ml
@@ -202,11 +202,14 @@ let alphaWorker ~(alphaTable: 'a alphaTable)
find_unused_suffix (Integer.succ min) infix infixes suffixes
in
let newsuffix = make_suffix newmin in
+ let newinfix = make_full_suffix infix newmin in
+ Kernel.(
+ debug ~dkey:dkey_alpha "New suffix: %s" newsuffix);
let base =
if is_generated_name prefix then prefix else lookupname
in
H.add
- infixes newsuffix
+ infixes newinfix
(ref (Integer.minus_one, [(Integer.minus_one, data)]));
(match undolist with
| Some l -> l:= AlphaAddedSuffix (prefix,newsuffix)::!l
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b72e5035f82..31b0267bff2 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3841,10 +3841,23 @@ let exitScope () =
| UndoRemoveFromEnv n :: t ->
H.remove env n; loop t
| UndoRemoveFromAlphaTable (p,i) :: t ->
+ Kernel.(
+ debug ~dkey:dkey_alpha_undo
+ "Removing %s %s from alpha table\n" p i);
(try
let h = H.find alphaTable p in
H.remove h i;
- if H.length h = 0 then H.remove alphaTable p
+ let l = H.length h in
+ if l = 0 then begin
+ H.remove alphaTable p;
+ Kernel.(
+ debug ~dkey:dkey_alpha_undo "No suffix for %s anymore" p)
+ end else begin
+ Kernel.(
+ debug ~dkey:dkey_alpha_undo "%d suffixes remaining@\n%t" l
+ (fun fmt ->
+ H.iter (fun i _ -> Format.fprintf fmt "%s@ " i) h))
+ end
with Not_found ->
Kernel.warning
"prefix (%s,%s) not in alpha conversion table. \
diff --git a/tests/syntax/rename.i b/tests/syntax/rename.i
index 08a549ccc24..86a78d54789 100644
--- a/tests/syntax/rename.i
+++ b/tests/syntax/rename.i
@@ -39,6 +39,20 @@ void f4(int *j_0_1) {
j_0_1+=j_0; }
}
+void f5() {
+ { int y_0; }
+ int y_0;
+}
+
+int y_0;
+
+void f6() {
+ { int y_2; }
+ int y_2;
+}
+
+int y_1;
+
struct not_anon {
int __anonCompField1;
};
--
GitLab