From 4984f5de8cd804e2a930e3d439a855423ef1ff5f Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 19 Aug 2019 09:09:20 +0200
Subject: [PATCH] [Cabs2cil] allow unions containing structs with FAMs

---
 src/kernel_internals/typing/cabs2cil.ml          |  2 +-
 tests/syntax/flexible_array_member.i             | 15 +++++++++++----
 tests/syntax/flexible_array_member_invalid1.i    |  4 ++--
 tests/syntax/flexible_array_member_invalid2.i    |  4 ++--
 tests/syntax/flexible_array_member_invalid3.i    |  4 ++--
 tests/syntax/flexible_array_member_invalid4.i    |  4 ++--
 tests/syntax/flexible_array_member_invalid5.i    |  4 ++--
 .../oracle/flexible_array_member.res.oracle      | 16 ++++++++++++----
 8 files changed, 34 insertions(+), 19 deletions(-)

diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 1b595764bf0..a8012c9c465 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5230,7 +5230,7 @@ and makeCompType ghost (isstruct: bool)
       if Cil.isFunctionType ftype then
         Kernel.error ~current:true
           "field `%s' declared as a function" n
-      else if Cil.has_flexible_array_member ftype then
+      else if Cil.has_flexible_array_member ftype && isstruct then
         Kernel.error ~current:true
           "field `%s' declared with a type containing a flexible array member."
           n
diff --git a/tests/syntax/flexible_array_member.i b/tests/syntax/flexible_array_member.i
index fbbd55dd676..9fda0812082 100644
--- a/tests/syntax/flexible_array_member.i
+++ b/tests/syntax/flexible_array_member.i
@@ -1,9 +1,16 @@
 // valid flexible array member declarations
-struct {
+struct s1 {
   int size;
   char data[];
-} s1;
+} ss1;
 
-struct {
+struct s2 {
   char len, data[];
-} s2;
+} ss2;
+
+union u {
+  struct s {
+    char len;
+    char data[];
+  } fam;
+} u1;
diff --git a/tests/syntax/flexible_array_member_invalid1.i b/tests/syntax/flexible_array_member_invalid1.i
index bd4b3f7fc0b..62ebdab3e24 100644
--- a/tests/syntax/flexible_array_member_invalid1.i
+++ b/tests/syntax/flexible_array_member_invalid1.i
@@ -1,4 +1,4 @@
 // invalid flexible array member (empty struct otherwise)
-struct {
+struct s1 {
   char data[];
-} s1;
+} ss1;
diff --git a/tests/syntax/flexible_array_member_invalid2.i b/tests/syntax/flexible_array_member_invalid2.i
index e5a1463ec54..eab5dccd0c3 100644
--- a/tests/syntax/flexible_array_member_invalid2.i
+++ b/tests/syntax/flexible_array_member_invalid2.i
@@ -1,6 +1,6 @@
 // invalid flexible array member (two incomplete fields)
-struct {
+struct s {
   int len;
   char data[];
   char more_data[];
-} s;
+} ss;
diff --git a/tests/syntax/flexible_array_member_invalid3.i b/tests/syntax/flexible_array_member_invalid3.i
index 30f2a733c7e..4baf088c14f 100644
--- a/tests/syntax/flexible_array_member_invalid3.i
+++ b/tests/syntax/flexible_array_member_invalid3.i
@@ -1,5 +1,5 @@
 // invalid flexible array member (two incomplete fields in same field group)
-struct {
+struct s {
   int len;
   char data[], more_data[];
-} s;
+} ss;
diff --git a/tests/syntax/flexible_array_member_invalid4.i b/tests/syntax/flexible_array_member_invalid4.i
index bd766622759..e84cce94b98 100644
--- a/tests/syntax/flexible_array_member_invalid4.i
+++ b/tests/syntax/flexible_array_member_invalid4.i
@@ -1,6 +1,6 @@
 // invalid flexible array member (incomplete field is not last)
-struct {
+struct s {
   int len;
   char data[];
   char b;
-} s;
+} ss;
diff --git a/tests/syntax/flexible_array_member_invalid5.i b/tests/syntax/flexible_array_member_invalid5.i
index dd3eac2f1c5..a0339194afe 100644
--- a/tests/syntax/flexible_array_member_invalid5.i
+++ b/tests/syntax/flexible_array_member_invalid5.i
@@ -4,7 +4,7 @@ typedef struct {
   char data[];
 } fam;
 
-struct {
+struct st {
   int len;
   fam f;
-} st;
+} sst;
diff --git a/tests/syntax/oracle/flexible_array_member.res.oracle b/tests/syntax/oracle/flexible_array_member.res.oracle
index a7317194e39..90af690c441 100644
--- a/tests/syntax/oracle/flexible_array_member.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member.res.oracle
@@ -1,13 +1,21 @@
 [kernel] Parsing tests/syntax/flexible_array_member.i (no preprocessing)
 /* Generated by Frama-C */
-struct __anonstruct_s1_1 {
+struct s1 {
    int size ;
    char data[] ;
 };
-struct __anonstruct_s2_2 {
+struct s2 {
    char len ;
    char data[] ;
 };
-struct __anonstruct_s1_1 s1;
-struct __anonstruct_s2_2 s2;
+struct s {
+   char len ;
+   char data[] ;
+};
+union u {
+   struct s fam ;
+};
+struct s1 ss1;
+struct s2 ss2;
+union u u1;
 
-- 
GitLab