From a1e9797875ed00a3561cf2648b8393cf6fae62a7 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 4 Oct 2019 14:37:33 +0200
Subject: [PATCH] [typing] avoid name clashes when generating names for
anonymous enum
More specifically, mark explicitely anonymous symbols from Frama-C's stdlib
as such if there's no other meaningful suffix to append to __anon{kind}
Fixes #672
---
src/kernel_internals/typing/cabs2cil.ml | 6 +++-
tests/syntax/anon_enum_libc.c | 13 +++++++++
tests/syntax/anon_enum_libc.h | 5 ++++
tests/syntax/oracle/anon_enum_libc.res.oracle | 28 +++++++++++++++++++
4 files changed, 51 insertions(+), 1 deletion(-)
create mode 100644 tests/syntax/anon_enum_libc.c
create mode 100644 tests/syntax/anon_enum_libc.h
create mode 100644 tests/syntax/oracle/anon_enum_libc.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 3137c53e5a2..c6490fa0157 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4343,7 +4343,11 @@ let rec doSpecList ghost (suggestedAnonName: string)
* collected and processed separately. *)
let attrs : A.attribute list ref = ref [] in (* __attribute__, etc. *)
let cvattrs : A.cvspec list ref = ref [] in (* const/volatile *)
-
+ let suggestedAnonName =
+ if suggestedAnonName <> "" then suggestedAnonName
+ else if get_current_stdheader () = "" then ""
+ else "fc_stdlib"
+ in
let doSpecElem (se: A.spec_elem)
(acc: A.typeSpecifier list)
: A.typeSpecifier list =
diff --git a/tests/syntax/anon_enum_libc.c b/tests/syntax/anon_enum_libc.c
new file mode 100644
index 00000000000..f59a10e2cf3
--- /dev/null
+++ b/tests/syntax/anon_enum_libc.c
@@ -0,0 +1,13 @@
+/* run.config
+OPT: -cpp-extra-args="-I @PTEST_DIR@" -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -ocode="" @PTEST_DIR@/result/@PTEST_NAME@.c -print
+*/
+
+struct { int x; float y; } s1;
+
+enum { BLA=4, BLI=12 };
+
+#include "anon_enum_libc.h"
+
+int f() { return BLA + s1.x; }
+
+int g() { return FOO + s2.t; }
diff --git a/tests/syntax/anon_enum_libc.h b/tests/syntax/anon_enum_libc.h
new file mode 100644
index 00000000000..e659c07ea7e
--- /dev/null
+++ b/tests/syntax/anon_enum_libc.h
@@ -0,0 +1,5 @@
+#include "features.h"
+__PUSH_FC_STDLIB
+struct { char z; unsigned long t; } s2;
+enum { FOO, BAR=3 };
+__POP_FC_STDLIB
diff --git a/tests/syntax/oracle/anon_enum_libc.res.oracle b/tests/syntax/oracle/anon_enum_libc.res.oracle
new file mode 100644
index 00000000000..0c3e5392e4f
--- /dev/null
+++ b/tests/syntax/oracle/anon_enum_libc.res.oracle
@@ -0,0 +1,28 @@
+[kernel] Parsing tests/syntax/anon_enum_libc.c (with preprocessing)
+[kernel] Parsing tests/syntax/result/anon_enum_libc.c (with preprocessing)
+/* Generated by Frama-C */
+#include "/home/virgile/Frama-C/frama-c-stable/tests/syntax/anon_enum_libc.h"
+struct __anonstruct_s1_1 {
+ int x ;
+ float y ;
+};
+enum __anonenum_2 {
+ BLA = 4,
+ BLI = 12
+};
+struct __anonstruct_s1_1 s1;
+int f(void)
+{
+ int __retres;
+ __retres = BLA + s1.x;
+ return __retres;
+}
+
+int g(void)
+{
+ int __retres;
+ __retres = (int)((unsigned long)FOO + s2.t);
+ return __retres;
+}
+
+
--
GitLab