Merge pull request #358 from thk123/bug/typedef-structs-clean

Store the typedef identifier in the symbol_type (cleaned up)

Author: Daniel Kroening

regression/Makefile

@@ -5,6 +5,7 @@ DIRS = ansi-c \
        cbmc-java \
        goto-analyzer \
        goto-instrument \
+       goto-instrument-typedef \
        test-script \
        # Empty last line
 

regression/ansi-c/gcc_types_compatible_p1/main.c

@@ -7,6 +7,14 @@ double d;
 typedef enum T1 { hot, dog, poo, bear } dingos;
 typedef enum T2 { janette, laura, amanda } cranberry;
 
+typedef enum AnonEnum { jim, bob, fred } names;
+
+typedef dingos altdingos;
+typedef dingos diffdingos;
+
+typedef names altnames;
+typedef names diffnames;
+
 typedef float same1;
 typedef float same2;
 
@@ -52,6 +60,9 @@ STATIC_ASSERT(__builtin_types_compatible_p(typeof (dingos), unsigned)); // ha!
 STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot), typeof (laura)));
 STATIC_ASSERT(__builtin_types_compatible_p(int[5], int[]));
 STATIC_ASSERT(__builtin_types_compatible_p(same1, same2));
+STATIC_ASSERT(__builtin_types_compatible_p(dingos, altdingos));
+STATIC_ASSERT(__builtin_types_compatible_p(diffdingos, altdingos));
+STATIC_ASSERT(__builtin_types_compatible_p(diffnames, altnames));
 STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot) *, int *));
 STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot), typeof (janette)));
 STATIC_ASSERT(__builtin_types_compatible_p(__int128, signed __int128));
@@ -84,7 +95,6 @@ STATIC_ASSERT(!__builtin_types_compatible_p(__float128, long double));
 STATIC_ASSERT(!__builtin_types_compatible_p(__float128, double));
 STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
 #endif
-
 #endif
 
 int main(void)

regression/ansi-c/gcc_types_compatible_p4/main.c

@@ -0,0 +1,27 @@
+#define STATIC_ASSERT(condition) \
+  int some_array[(condition) ? 1 : -1];
+
+typedef struct struct_tag
+{
+  int x;
+  float y;
+} struct_typedef;
+
+typedef struct struct_tag alt_typedef;
+typedef struct_typedef another_typedef;
+
+#ifdef __GNUC__
+
+
+STATIC_ASSERT(__builtin_types_compatible_p(struct struct_tag, struct_typedef));
+STATIC_ASSERT(__builtin_types_compatible_p(struct struct_tag, alt_typedef));
+STATIC_ASSERT(__builtin_types_compatible_p(struct struct_tag, another_typedef));
+STATIC_ASSERT(__builtin_types_compatible_p(struct_typedef, alt_typedef));
+STATIC_ASSERT(__builtin_types_compatible_p(struct_typedef, another_typedef));
+STATIC_ASSERT(__builtin_types_compatible_p(alt_typedef, another_typedef));
+
+#endif
+
+int main(void)
+{
+}

regression/ansi-c/gcc_types_compatible_p4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc/typedef-anon-struct1/main.c

@@ -0,0 +1,11 @@
+
+typedef struct
+{
+  int x;
+  float y;
+} MYSTRUCT;
+
+void fun()
+{
+  MYSTRUCT mystruct_var = {.x = 3, .y = 2.1f};
+}

regression/cbmc/typedef-anon-struct1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT
+--
+warning: ignoring

regression/cbmc/typedef-anon-struct2/main.c

@@ -0,0 +1,11 @@
+
+typedef struct
+{
+  int x;
+  float y;
+} MYSTRUCT;
+
+void fun()
+{
+  MYSTRUCT mystruct_var  = {.x = 10, .y = 3.1f}, another_mystruct_var = {.x = 3, .y = 2.1f};
+}

regression/cbmc/typedef-anon-struct2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT
+Base name\.+: another_mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT
+--
+warning: ignoring

regression/cbmc/typedef-anon-union1/main.c

@@ -0,0 +1,11 @@
+
+typedef union
+{
+  int x;
+  float y;
+} MYUNION;
+
+void fun()
+{
+  MYUNION myunion_var = {.y = 2.1f};
+}

regression/cbmc/typedef-anon-union1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: myunion_var\nMode\.+: C\nType\.+: MYUNION
+--
+warning: ignoring

regression/cbmc/typedef-anon-union2/main.c

@@ -0,0 +1,11 @@
+
+typedef union
+{
+  int x;
+  float y;
+} MYUNION;
+
+void fun()
+{
+  MYUNION myunion_var = {.y = 2.1f}, another_myunion_var = {.y = 2.1f};
+}

regression/cbmc/typedef-anon-union2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: myunion_var\nMode\.+: C\nType\.+: MYUNION
+Base name\.+: another_myunion_var\nMode\.+: C\nType\.+: MYUNION
+--
+warning: ignoring

regression/cbmc/typedef-const-struct1/main.c

@@ -0,0 +1,12 @@
+
+typedef struct tag_struct_name
+{
+  int x;
+  float y;
+} MYSTRUCT;
+
+void fun()
+{
+  const struct tag_struct_name tag_struct_var = {.x = 1, .y = 3.14f};
+  const MYSTRUCT mystruct_var = {.x = 3, .y = 2.1f};
+}

regression/cbmc/typedef-const-struct1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: tag_struct_var\nMode\.+: C\nType\.+: const struct tag_struct_name
+Base name\.+: mystruct_var\nMode\.+: C\nType\.+: const MYSTRUCT
+--
+warning: ignoring

regression/cbmc/typedef-const-type1/main.c

@@ -0,0 +1,8 @@
+
+typedef int MYINT;
+
+void fun()
+{
+  const int int_var = 3;
+  const MYINT myint_var = 5;
+}

regression/cbmc/typedef-const-type1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: int_var\nMode\.+: C\nType\.+: const signed int
+Base name\.+: myint_var\nMode\.+: C\nType\.+: const MYINT
+--
+warning: ignoring

regression/cbmc/typedef-const-union1/main.c

@@ -0,0 +1,12 @@
+
+typedef union tag_union_name
+{
+  int x;
+  float y;
+} MYUNION;
+
+void fun()
+{
+  const union tag_union_name tag_union_var = {1};
+  const MYUNION myunion_var = {.y = 2.1f};
+}

regression/cbmc/typedef-const-union1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: tag_union_var\nMode\.+: C\nType\.+: const union tag_union_name
+Base name\.+: myunion_var\nMode\.+: C\nType\.+: const MYUNION
+--
+warning: ignoring

regression/cbmc/typedef-param-anon-struct1/main.c

@@ -0,0 +1,11 @@
+
+typedef struct
+{
+  int x;
+  float y;
+} MYSTRUCT;
+
+void fun(MYSTRUCT mystruct_param)
+{
+
+}

regression/cbmc/typedef-param-anon-struct1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: mystruct_param\nMode\.+: C\nType\.+: MYSTRUCT
+--
+warning: ignoring

regression/cbmc/typedef-param-anon-union1/main.c

@@ -0,0 +1,10 @@
+
+typedef union
+{
+  int x;
+  float y;
+} MYUNION;
+
+void fun(MYUNION myunion_param)
+{
+}

regression/cbmc/typedef-param-anon-union1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: myunion_param\nMode\.+: C\nType\.+: MYUNION
+--
+warning: ignoring

regression/cbmc/typedef-param-struct1/main.c

@@ -0,0 +1,10 @@
+
+typedef struct tag_struct_name
+{
+  int x;
+  float y;
+} MYSTRUCT;
+
+void fun(struct tag_struct_name tag_struct_param, MYSTRUCT mystruct_param)
+{
+}

regression/cbmc/typedef-param-struct1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: tag_struct_param\nMode\.+: C\nType\.+: struct tag_struct_name
+Base name\.+: mystruct_param\nMode\.+: C\nType\.+: MYSTRUCT
+--
+warning: ignoring

regression/cbmc/typedef-param-type1/main.c

@@ -0,0 +1,7 @@
+
+typedef int MYINT;
+
+void fun(int int_param, MYINT myint_param)
+{
+
+}

regression/cbmc/typedef-param-type1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: int_param\nMode\.+: C\nType\.+: signed int
+Base name\.+: myint_param\nMode\.+: C\nType\.+: MYINT
+--
+warning: ignoring

regression/cbmc/typedef-param-type2/main.c

@@ -0,0 +1,8 @@
+
+typedef int MYINT;
+typedef int ALTINT;
+
+void fun(int int_param, MYINT myint_param, ALTINT altint_param)
+{
+
+}

regression/cbmc/typedef-param-type2/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: int_param\nMode\.+: C\nType\.+: signed int
+Base name\.+: myint_param\nMode\.+: C\nType\.+: MYINT
+Base name\.+: altint_param\nMode\.+: C\nType\.+: ALTINT
+--
+warning: ignoring

regression/cbmc/typedef-param-type3/main.c

@@ -0,0 +1,7 @@
+
+typedef int MYINT;
+typedef MYINT CHAINEDINT;
+
+void fun(int int_param, MYINT myint_param, CHAINEDINT chainedint_param)
+{
+}

regression/cbmc/typedef-param-type3/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: int_param\nMode\.+: C\nType\.+: signed int
+Base name\.+: myint_param\nMode\.+: C\nType\.+: MYINT
+Base name\.+: chainedint_param\nMode\.+: C\nType\.+: CHAINEDINT
+--
+warning: ignoring

regression/cbmc/typedef-param-union1/main.c

@@ -0,0 +1,10 @@
+
+typedef union tag_union_name
+{
+  int x;
+  float y;
+} MYUNION;
+
+void fun(union tag_union_name tag_union_param, MYUNION myunion_param)
+{
+}

regression/cbmc/typedef-param-union1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-symbol-table --function fun
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Base name\.+: tag_union_param\nMode\.+: C\nType\.+: union tag_union_name
+Base name\.+: myunion_param\nMode\.+: C\nType\.+: MYUNION
+--
+warning: ignoring