diff --git a/regression/Makefile b/regression/Makefile index 5c59fd6e34c..296f583cc5e 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -5,6 +5,7 @@ DIRS = ansi-c \ cbmc-java \ goto-analyzer \ goto-instrument \ + goto-instrument-typedef \ test-script \ # Empty last line diff --git a/regression/ansi-c/gcc_types_compatible_p1/main.c b/regression/ansi-c/gcc_types_compatible_p1/main.c index 403596c4276..4f327d51085 100644 --- a/regression/ansi-c/gcc_types_compatible_p1/main.c +++ b/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) diff --git a/regression/ansi-c/gcc_types_compatible_p4/main.c b/regression/ansi-c/gcc_types_compatible_p4/main.c new file mode 100644 index 00000000000..69b84a8304b --- /dev/null +++ b/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) +{ +} diff --git a/regression/ansi-c/gcc_types_compatible_p4/test.desc b/regression/ansi-c/gcc_types_compatible_p4/test.desc new file mode 100644 index 00000000000..466da18b2b5 --- /dev/null +++ b/regression/ansi-c/gcc_types_compatible_p4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/cbmc/typedef-anon-struct1/main.c b/regression/cbmc/typedef-anon-struct1/main.c new file mode 100644 index 00000000000..d1e7196a3b1 --- /dev/null +++ b/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}; +} diff --git a/regression/cbmc/typedef-anon-struct1/test.desc b/regression/cbmc/typedef-anon-struct1/test.desc new file mode 100644 index 00000000000..d9d9769f677 --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-anon-struct2/main.c b/regression/cbmc/typedef-anon-struct2/main.c new file mode 100644 index 00000000000..35475513f7d --- /dev/null +++ b/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}; +} diff --git a/regression/cbmc/typedef-anon-struct2/test.desc b/regression/cbmc/typedef-anon-struct2/test.desc new file mode 100644 index 00000000000..83af4f59a9f --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-anon-union1/main.c b/regression/cbmc/typedef-anon-union1/main.c new file mode 100644 index 00000000000..9322c77cb6e --- /dev/null +++ b/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}; +} diff --git a/regression/cbmc/typedef-anon-union1/test.desc b/regression/cbmc/typedef-anon-union1/test.desc new file mode 100644 index 00000000000..6f74f9f5574 --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-anon-union2/main.c b/regression/cbmc/typedef-anon-union2/main.c new file mode 100644 index 00000000000..b2dd6594432 --- /dev/null +++ b/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}; +} diff --git a/regression/cbmc/typedef-anon-union2/test.desc b/regression/cbmc/typedef-anon-union2/test.desc new file mode 100644 index 00000000000..f5242dc7ac7 --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-const-struct1/main.c b/regression/cbmc/typedef-const-struct1/main.c new file mode 100644 index 00000000000..ab8137e82e4 --- /dev/null +++ b/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}; +} diff --git a/regression/cbmc/typedef-const-struct1/test.desc b/regression/cbmc/typedef-const-struct1/test.desc new file mode 100644 index 00000000000..f6c2d8e4b48 --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-const-type1/main.c b/regression/cbmc/typedef-const-type1/main.c new file mode 100644 index 00000000000..8cd4a4346eb --- /dev/null +++ b/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; +} diff --git a/regression/cbmc/typedef-const-type1/test.desc b/regression/cbmc/typedef-const-type1/test.desc new file mode 100644 index 00000000000..0e1b67ce3da --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-const-union1/main.c b/regression/cbmc/typedef-const-union1/main.c new file mode 100644 index 00000000000..b8defe635a6 --- /dev/null +++ b/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}; +} diff --git a/regression/cbmc/typedef-const-union1/test.desc b/regression/cbmc/typedef-const-union1/test.desc new file mode 100644 index 00000000000..019a6551911 --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-param-anon-struct1/main.c b/regression/cbmc/typedef-param-anon-struct1/main.c new file mode 100644 index 00000000000..e8f3fb8fd7c --- /dev/null +++ b/regression/cbmc/typedef-param-anon-struct1/main.c @@ -0,0 +1,11 @@ + +typedef struct +{ + int x; + float y; +} MYSTRUCT; + +void fun(MYSTRUCT mystruct_param) +{ + +} diff --git a/regression/cbmc/typedef-param-anon-struct1/test.desc b/regression/cbmc/typedef-param-anon-struct1/test.desc new file mode 100644 index 00000000000..1d7c939008a --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-param-anon-union1/main.c b/regression/cbmc/typedef-param-anon-union1/main.c new file mode 100644 index 00000000000..71791d9adfc --- /dev/null +++ b/regression/cbmc/typedef-param-anon-union1/main.c @@ -0,0 +1,10 @@ + +typedef union +{ + int x; + float y; +} MYUNION; + +void fun(MYUNION myunion_param) +{ +} diff --git a/regression/cbmc/typedef-param-anon-union1/test.desc b/regression/cbmc/typedef-param-anon-union1/test.desc new file mode 100644 index 00000000000..34c29cefda9 --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-param-struct1/main.c b/regression/cbmc/typedef-param-struct1/main.c new file mode 100644 index 00000000000..a358c15a030 --- /dev/null +++ b/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) +{ +} diff --git a/regression/cbmc/typedef-param-struct1/test.desc b/regression/cbmc/typedef-param-struct1/test.desc new file mode 100644 index 00000000000..ad0d23ed7a9 --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-param-type1/main.c b/regression/cbmc/typedef-param-type1/main.c new file mode 100644 index 00000000000..b4c915066b6 --- /dev/null +++ b/regression/cbmc/typedef-param-type1/main.c @@ -0,0 +1,7 @@ + +typedef int MYINT; + +void fun(int int_param, MYINT myint_param) +{ + +} diff --git a/regression/cbmc/typedef-param-type1/test.desc b/regression/cbmc/typedef-param-type1/test.desc new file mode 100644 index 00000000000..14659940cde --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-param-type2/main.c b/regression/cbmc/typedef-param-type2/main.c new file mode 100644 index 00000000000..b5974fb6bbb --- /dev/null +++ b/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) +{ + +} diff --git a/regression/cbmc/typedef-param-type2/test.desc b/regression/cbmc/typedef-param-type2/test.desc new file mode 100644 index 00000000000..14e7db9d3d4 --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-param-type3/main.c b/regression/cbmc/typedef-param-type3/main.c new file mode 100644 index 00000000000..4d542e10c13 --- /dev/null +++ b/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) +{ +} diff --git a/regression/cbmc/typedef-param-type3/test.desc b/regression/cbmc/typedef-param-type3/test.desc new file mode 100644 index 00000000000..1f10dea2551 --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-param-union1/main.c b/regression/cbmc/typedef-param-union1/main.c new file mode 100644 index 00000000000..8f961614e5d --- /dev/null +++ b/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) +{ +} diff --git a/regression/cbmc/typedef-param-union1/test.desc b/regression/cbmc/typedef-param-union1/test.desc new file mode 100644 index 00000000000..37ab0aee08c --- /dev/null +++ b/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 diff --git a/regression/cbmc/typedef-return-anon-struct1/main.c b/regression/cbmc/typedef-return-anon-struct1/main.c new file mode 100644 index 00000000000..0195b955cdd --- /dev/null +++ b/regression/cbmc/typedef-return-anon-struct1/main.c @@ -0,0 +1,12 @@ + +typedef struct +{ + int x; + float y; +} MYSTRUCT; + +MYSTRUCT fun() +{ + MYSTRUCT return_variable = {.x = 1, .y = 3.14f}; + return return_variable; +} diff --git a/regression/cbmc/typedef-return-anon-struct1/test.desc b/regression/cbmc/typedef-return-anon-struct1/test.desc new file mode 100644 index 00000000000..420ac1295ac --- /dev/null +++ b/regression/cbmc/typedef-return-anon-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\.+: return\nMode\.+: C\nType\.+: MYSTRUCT +Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(\) +-- +warning: ignoring diff --git a/regression/cbmc/typedef-return-anon-union1/main.c b/regression/cbmc/typedef-return-anon-union1/main.c new file mode 100644 index 00000000000..3bc7d19d5b7 --- /dev/null +++ b/regression/cbmc/typedef-return-anon-union1/main.c @@ -0,0 +1,15 @@ + +typedef union +{ + int x; + float y; +} MYUNION; + + +MYUNION fun() +{ + MYUNION return_variable = {1}; + return return_variable; +} + + diff --git a/regression/cbmc/typedef-return-anon-union1/test.desc b/regression/cbmc/typedef-return-anon-union1/test.desc new file mode 100644 index 00000000000..8d8d41a4dfe --- /dev/null +++ b/regression/cbmc/typedef-return-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\.+: fun\nMode\.+: C\nType\.+: MYUNION \(\) +-- +warning: ignoring diff --git a/regression/cbmc/typedef-return-struct1/main.c b/regression/cbmc/typedef-return-struct1/main.c new file mode 100644 index 00000000000..30c1323555c --- /dev/null +++ b/regression/cbmc/typedef-return-struct1/main.c @@ -0,0 +1,20 @@ + +typedef struct tag_struct_name +{ + int x; + float y; +} MYSTRUCT; + +struct tag_struct_name fun() +{ + struct tag_struct_name return_variable = { .x = 1, .y = 3.14f}; + return return_variable; +} + +MYSTRUCT fun2() +{ + MYSTRUCT return_variable = { .x = 1, .y = 3.14f}; + return return_variable; +} + + diff --git a/regression/cbmc/typedef-return-struct1/test.desc b/regression/cbmc/typedef-return-struct1/test.desc new file mode 100644 index 00000000000..c4a9dc3550c --- /dev/null +++ b/regression/cbmc/typedef-return-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\.+: fun\nMode\.+: C\nType\.+: struct tag_struct_name \(\) +Base name\.+: fun2\nMode\.+: C\nType\.+: MYSTRUCT \(\) +-- +warning: ignoring diff --git a/regression/cbmc/typedef-return-type1/main.c b/regression/cbmc/typedef-return-type1/main.c new file mode 100644 index 00000000000..1ba7f426f89 --- /dev/null +++ b/regression/cbmc/typedef-return-type1/main.c @@ -0,0 +1,12 @@ + +typedef int MYINT; + +int fun() +{ + return 4; +} + +MYINT fun2() +{ + return 5; +} diff --git a/regression/cbmc/typedef-return-type1/test.desc b/regression/cbmc/typedef-return-type1/test.desc new file mode 100644 index 00000000000..0ebbe5109a7 --- /dev/null +++ b/regression/cbmc/typedef-return-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\.+: fun\nMode\.+: C\nType\.+: signed int \(\) +Base name\.+: fun2\nMode\.+: C\nType\.+: MYINT \(\) +-- +warning: ignoring diff --git a/regression/cbmc/typedef-return-type2/main.c b/regression/cbmc/typedef-return-type2/main.c new file mode 100644 index 00000000000..0d94ab54da3 --- /dev/null +++ b/regression/cbmc/typedef-return-type2/main.c @@ -0,0 +1,13 @@ + +typedef int MYINT; +typedef int ALTINT; + +MYINT fun() +{ + +} + +ALTINT fun2() +{ + +} diff --git a/regression/cbmc/typedef-return-type2/test.desc b/regression/cbmc/typedef-return-type2/test.desc new file mode 100644 index 00000000000..27b2e77902d --- /dev/null +++ b/regression/cbmc/typedef-return-type2/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\.+: fun\nMode\.+: C\nType\.+: MYINT \(\) +Base name\.+: fun2\nMode\.+: C\nType\.+: ALTINT \(\) +-- +warning: ignoring diff --git a/regression/cbmc/typedef-return-type3/main.c b/regression/cbmc/typedef-return-type3/main.c new file mode 100644 index 00000000000..e246757c692 --- /dev/null +++ b/regression/cbmc/typedef-return-type3/main.c @@ -0,0 +1,12 @@ + +typedef int MYINT; +typedef MYINT CHAINEDINT; + +MYINT fun() +{ +} + +CHAINEDINT fun2() +{ + +} \ No newline at end of file diff --git a/regression/cbmc/typedef-return-type3/test.desc b/regression/cbmc/typedef-return-type3/test.desc new file mode 100644 index 00000000000..7cfecafece9 --- /dev/null +++ b/regression/cbmc/typedef-return-type3/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show-symbol-table --function fun +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(\) +Base name\.+: fun2\nMode\.+: C\nType\.+: CHAINEDINT \(\) +-- +warning: ignoring diff --git a/regression/cbmc/typedef-return-union1/main.c b/regression/cbmc/typedef-return-union1/main.c new file mode 100644 index 00000000000..ad69cb04545 --- /dev/null +++ b/regression/cbmc/typedef-return-union1/main.c @@ -0,0 +1,20 @@ + +typedef union tag_union_name +{ + int x; + float y; +} MYUNION; + +union tag_union_name fun() +{ + union tag_union_name return_variable = {1}; + return return_variable; +} + +MYUNION fun2() +{ + MYUNION return_variable = {1}; + return return_variable; +} + + diff --git a/regression/cbmc/typedef-return-union1/test.desc b/regression/cbmc/typedef-return-union1/test.desc new file mode 100644 index 00000000000..b1668066f08 --- /dev/null +++ b/regression/cbmc/typedef-return-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\.+: fun\nMode\.+: C\nType\.+: union tag_union_name \(\) +Base name\.+: fun2\nMode\.+: C\nType\.+: MYUNION \(\) +-- +warning: ignoring diff --git a/regression/cbmc/typedef-struct1/main.c b/regression/cbmc/typedef-struct1/main.c new file mode 100644 index 00000000000..dac5abf77b8 --- /dev/null +++ b/regression/cbmc/typedef-struct1/main.c @@ -0,0 +1,12 @@ + +typedef struct tag_struct_name +{ + int x; + float y; +} MYSTRUCT; + +void fun() +{ + struct tag_struct_name tag_struct_var = {.x = 1, .y = 3.14f}; + MYSTRUCT mystruct_var = {.x = 3, .y = 2.1f}; +} diff --git a/regression/cbmc/typedef-struct1/test.desc b/regression/cbmc/typedef-struct1/test.desc new file mode 100644 index 00000000000..90f1c22933a --- /dev/null +++ b/regression/cbmc/typedef-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\.+: struct tag_struct_name +Base name\.+: mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT +-- +warning: ignoring diff --git a/regression/cbmc/typedef-struct2/main.c b/regression/cbmc/typedef-struct2/main.c new file mode 100644 index 00000000000..dac5abf77b8 --- /dev/null +++ b/regression/cbmc/typedef-struct2/main.c @@ -0,0 +1,12 @@ + +typedef struct tag_struct_name +{ + int x; + float y; +} MYSTRUCT; + +void fun() +{ + struct tag_struct_name tag_struct_var = {.x = 1, .y = 3.14f}; + MYSTRUCT mystruct_var = {.x = 3, .y = 2.1f}; +} diff --git a/regression/cbmc/typedef-struct2/test.desc b/regression/cbmc/typedef-struct2/test.desc new file mode 100644 index 00000000000..90f1c22933a --- /dev/null +++ b/regression/cbmc/typedef-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\.+: tag_struct_var\nMode\.+: C\nType\.+: struct tag_struct_name +Base name\.+: mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT +-- +warning: ignoring diff --git a/regression/cbmc/typedef-type1/main.c b/regression/cbmc/typedef-type1/main.c new file mode 100644 index 00000000000..43f028c7772 --- /dev/null +++ b/regression/cbmc/typedef-type1/main.c @@ -0,0 +1,8 @@ + +typedef int MYINT; + +void fun() +{ + int int_var = 3; + MYINT myint_var = 5; +} diff --git a/regression/cbmc/typedef-type1/test.desc b/regression/cbmc/typedef-type1/test.desc new file mode 100644 index 00000000000..08d1f5abfcd --- /dev/null +++ b/regression/cbmc/typedef-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\.+: signed int +Base name\.+: myint_var\nMode\.+: C\nType\.+: MYINT +-- +warning: ignoring diff --git a/regression/cbmc/typedef-type2/main.c b/regression/cbmc/typedef-type2/main.c new file mode 100644 index 00000000000..acb1cce2da4 --- /dev/null +++ b/regression/cbmc/typedef-type2/main.c @@ -0,0 +1,10 @@ + +typedef int MYINT; +typedef int ALTINT; + +void fun() +{ + int int_var = 3; + MYINT myint_var = 5; + ALTINT altint_var = 7; +} diff --git a/regression/cbmc/typedef-type2/test.desc b/regression/cbmc/typedef-type2/test.desc new file mode 100644 index 00000000000..76d1d114a19 --- /dev/null +++ b/regression/cbmc/typedef-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_var\nMode\.+: C\nType\.+: signed int +Base name\.+: myint_var\nMode\.+: C\nType\.+: MYINT +Base name\.+: altint_var\nMode\.+: C\nType\.+: ALTINT +-- +warning: ignoring diff --git a/regression/cbmc/typedef-type3/main.c b/regression/cbmc/typedef-type3/main.c new file mode 100644 index 00000000000..5855e0c24cb --- /dev/null +++ b/regression/cbmc/typedef-type3/main.c @@ -0,0 +1,10 @@ + +typedef int MYINT; +typedef MYINT CHAINEDINT; + +void fun() +{ + int int_var = 3; + MYINT myint_var = 5; + CHAINEDINT chainedint_var = 5; +} diff --git a/regression/cbmc/typedef-type3/test.desc b/regression/cbmc/typedef-type3/test.desc new file mode 100644 index 00000000000..cc5ad52d953 --- /dev/null +++ b/regression/cbmc/typedef-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_var\nMode\.+: C\nType\.+: signed int +Base name\.+: myint_var\nMode\.+: C\nType\.+: MYINT +Base name\.+: chainedint_var\nMode\.+: C\nType\.+: CHAINEDINT +-- +warning: ignoring diff --git a/regression/cbmc/typedef-type4/main.c b/regression/cbmc/typedef-type4/main.c new file mode 100644 index 00000000000..aa2ec9ad7fb --- /dev/null +++ b/regression/cbmc/typedef-type4/main.c @@ -0,0 +1,8 @@ + +typedef int MYINT; + +void fun() +{ + int int_var = 3; + MYINT myint_var = 5, another_myint_var = 10; +} diff --git a/regression/cbmc/typedef-type4/test.desc b/regression/cbmc/typedef-type4/test.desc new file mode 100644 index 00000000000..1c0c063b8e1 --- /dev/null +++ b/regression/cbmc/typedef-type4/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_var\nMode\.+: C\nType\.+: signed int +Base name\.+: myint_var\nMode\.+: C\nType\.+: MYINT +Base name\.+: another_myint_var\nMode\.+: C\nType\.+: MYINT +-- +warning: ignoring diff --git a/regression/cbmc/typedef-union1/main.c b/regression/cbmc/typedef-union1/main.c new file mode 100644 index 00000000000..6f56f3c731b --- /dev/null +++ b/regression/cbmc/typedef-union1/main.c @@ -0,0 +1,12 @@ + +typedef union tag_union_name +{ + int x; + float y; +} MYUNION; + +void fun() +{ + union tag_union_name tag_union_var = {1}; + MYUNION myunion_var = {.y = 2.1f}; +} diff --git a/regression/cbmc/typedef-union1/test.desc b/regression/cbmc/typedef-union1/test.desc new file mode 100644 index 00000000000..e7ce9b6b459 --- /dev/null +++ b/regression/cbmc/typedef-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\.+: union tag_union_name +Base name\.+: myunion_var\nMode\.+: C\nType\.+: MYUNION +-- +warning: ignoring diff --git a/regression/cbmc/typedef-union2/main.c b/regression/cbmc/typedef-union2/main.c new file mode 100644 index 00000000000..9ca707cf767 --- /dev/null +++ b/regression/cbmc/typedef-union2/main.c @@ -0,0 +1,12 @@ + +typedef union tag_union_name +{ + int x; + float y; +} MYUNION; + +void fun() +{ + union tag_union_name tag_union_var = {1}, another_tag_union_var = {1}; + MYUNION myunion_var = {.y = 2.1f}, another_myunion_var = {.y = 3.1f}; +} diff --git a/regression/cbmc/typedef-union2/test.desc b/regression/cbmc/typedef-union2/test.desc new file mode 100644 index 00000000000..33cbbff29af --- /dev/null +++ b/regression/cbmc/typedef-union2/test.desc @@ -0,0 +1,13 @@ +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\.+: union tag_union_name +Base name\.+: another_tag_union_var\nMode\.+: C\nType\.+: union tag_union_name +Base name\.+: myunion_var\nMode\.+: C\nType\.+: MYUNION +Base name\.+: another_myunion_var\nMode\.+: C\nType\.+: MYUNION +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/Makefile b/regression/goto-instrument-typedef/Makefile new file mode 100644 index 00000000000..08fe97ae88c --- /dev/null +++ b/regression/goto-instrument-typedef/Makefile @@ -0,0 +1,31 @@ + +default: tests.log + +test: + @if ! ../test.pl -c ../chain.sh ; then \ + ../failed-tests-printer.pl ; \ + exit 1; \ + fi + +tests.log: + @if ! ../test.pl -c ../chain.sh ; then \ + ../failed-tests-printer.pl ; \ + exit 1; \ + fi + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + @for dir in *; do \ + rm -f tests.log; \ + if [ -d "$$dir" ]; then \ + cd "$$dir"; \ + rm -f *.out *.gb; \ + cd ..; \ + fi \ + done diff --git a/regression/goto-instrument-typedef/chain.sh b/regression/goto-instrument-typedef/chain.sh new file mode 100755 index 00000000000..9cef4ffdfa4 --- /dev/null +++ b/regression/goto-instrument-typedef/chain.sh @@ -0,0 +1,14 @@ +#!/bin/bash + +SRC=../../../src + +GC=$SRC/goto-cc/goto-cc +GI=$SRC/goto-instrument/goto-instrument + +OPTS=$1 +NAME=${2%.c} + +rm $NAME.gb +$GC $NAME.c --function fun -o $NAME.gb +echo $GI $OPTS $NAME.gb +$GI $OPTS $NAME.gb diff --git a/regression/goto-instrument-typedef/typedef-anon-struct1/main.c b/regression/goto-instrument-typedef/typedef-anon-struct1/main.c new file mode 100644 index 00000000000..d1e7196a3b1 --- /dev/null +++ b/regression/goto-instrument-typedef/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}; +} diff --git a/regression/goto-instrument-typedef/typedef-anon-struct1/test.desc b/regression/goto-instrument-typedef/typedef-anon-struct1/test.desc new file mode 100644 index 00000000000..59aba0e01a6 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-anon-struct1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-anon-struct2/main.c b/regression/goto-instrument-typedef/typedef-anon-struct2/main.c new file mode 100644 index 00000000000..35475513f7d --- /dev/null +++ b/regression/goto-instrument-typedef/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}; +} diff --git a/regression/goto-instrument-typedef/typedef-anon-struct2/test.desc b/regression/goto-instrument-typedef/typedef-anon-struct2/test.desc new file mode 100644 index 00000000000..490b6cc2623 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-anon-struct2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// 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 diff --git a/regression/goto-instrument-typedef/typedef-anon-union1/main.c b/regression/goto-instrument-typedef/typedef-anon-union1/main.c new file mode 100644 index 00000000000..9322c77cb6e --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-anon-union1/main.c @@ -0,0 +1,11 @@ + +typedef union +{ + int x; + float y; +} MYUNION; + +void fun() +{ + MYUNION myunion_var = {.y = 2.1f}; +} diff --git a/regression/goto-instrument-typedef/typedef-anon-union1/test.desc b/regression/goto-instrument-typedef/typedef-anon-union1/test.desc new file mode 100644 index 00000000000..86caf078d6a --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-anon-union1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: myunion_var\nMode\.+: C\nType\.+: MYUNION +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-anon-union2/main.c b/regression/goto-instrument-typedef/typedef-anon-union2/main.c new file mode 100644 index 00000000000..b2dd6594432 --- /dev/null +++ b/regression/goto-instrument-typedef/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}; +} diff --git a/regression/goto-instrument-typedef/typedef-anon-union2/test.desc b/regression/goto-instrument-typedef/typedef-anon-union2/test.desc new file mode 100644 index 00000000000..8d8ca64aa93 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-anon-union2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// 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 diff --git a/regression/goto-instrument-typedef/typedef-const-struct1/main.c b/regression/goto-instrument-typedef/typedef-const-struct1/main.c new file mode 100644 index 00000000000..ab8137e82e4 --- /dev/null +++ b/regression/goto-instrument-typedef/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}; +} diff --git a/regression/goto-instrument-typedef/typedef-const-struct1/test.desc b/regression/goto-instrument-typedef/typedef-const-struct1/test.desc new file mode 100644 index 00000000000..a6aad1f799a --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-const-struct1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// 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 diff --git a/regression/goto-instrument-typedef/typedef-const-type1/main.c b/regression/goto-instrument-typedef/typedef-const-type1/main.c new file mode 100644 index 00000000000..8cd4a4346eb --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-const-type1/main.c @@ -0,0 +1,8 @@ + +typedef int MYINT; + +void fun() +{ + const int int_var = 3; + const MYINT myint_var = 5; +} diff --git a/regression/goto-instrument-typedef/typedef-const-type1/test.desc b/regression/goto-instrument-typedef/typedef-const-type1/test.desc new file mode 100644 index 00000000000..481b097653f --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-const-type1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// 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 diff --git a/regression/goto-instrument-typedef/typedef-const-union1/main.c b/regression/goto-instrument-typedef/typedef-const-union1/main.c new file mode 100644 index 00000000000..b8defe635a6 --- /dev/null +++ b/regression/goto-instrument-typedef/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}; +} diff --git a/regression/goto-instrument-typedef/typedef-const-union1/test.desc b/regression/goto-instrument-typedef/typedef-const-union1/test.desc new file mode 100644 index 00000000000..cd303b85195 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-const-union1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// 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 diff --git a/regression/goto-instrument-typedef/typedef-param-anon-struct1/main.c b/regression/goto-instrument-typedef/typedef-param-anon-struct1/main.c new file mode 100644 index 00000000000..e8f3fb8fd7c --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-param-anon-struct1/main.c @@ -0,0 +1,11 @@ + +typedef struct +{ + int x; + float y; +} MYSTRUCT; + +void fun(MYSTRUCT mystruct_param) +{ + +} diff --git a/regression/goto-instrument-typedef/typedef-param-anon-struct1/test.desc b/regression/goto-instrument-typedef/typedef-param-anon-struct1/test.desc new file mode 100644 index 00000000000..537526b4422 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-param-anon-struct1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: mystruct_param\nMode\.+: C\nType\.+: MYSTRUCT +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-param-anon-union1/main.c b/regression/goto-instrument-typedef/typedef-param-anon-union1/main.c new file mode 100644 index 00000000000..71791d9adfc --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-param-anon-union1/main.c @@ -0,0 +1,10 @@ + +typedef union +{ + int x; + float y; +} MYUNION; + +void fun(MYUNION myunion_param) +{ +} diff --git a/regression/goto-instrument-typedef/typedef-param-anon-union1/test.desc b/regression/goto-instrument-typedef/typedef-param-anon-union1/test.desc new file mode 100644 index 00000000000..270316982a3 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-param-anon-union1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: myunion_param\nMode\.+: C\nType\.+: MYUNION +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-param-struct1/main.c b/regression/goto-instrument-typedef/typedef-param-struct1/main.c new file mode 100644 index 00000000000..a358c15a030 --- /dev/null +++ b/regression/goto-instrument-typedef/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) +{ +} diff --git a/regression/goto-instrument-typedef/typedef-param-struct1/test.desc b/regression/goto-instrument-typedef/typedef-param-struct1/test.desc new file mode 100644 index 00000000000..c26ee458459 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-param-struct1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// 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 diff --git a/regression/goto-instrument-typedef/typedef-param-type1/main.c b/regression/goto-instrument-typedef/typedef-param-type1/main.c new file mode 100644 index 00000000000..b4c915066b6 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-param-type1/main.c @@ -0,0 +1,7 @@ + +typedef int MYINT; + +void fun(int int_param, MYINT myint_param) +{ + +} diff --git a/regression/goto-instrument-typedef/typedef-param-type1/test.desc b/regression/goto-instrument-typedef/typedef-param-type1/test.desc new file mode 100644 index 00000000000..050ac22b315 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-param-type1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// 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 diff --git a/regression/goto-instrument-typedef/typedef-param-type2/main.c b/regression/goto-instrument-typedef/typedef-param-type2/main.c new file mode 100644 index 00000000000..b5974fb6bbb --- /dev/null +++ b/regression/goto-instrument-typedef/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) +{ + +} diff --git a/regression/goto-instrument-typedef/typedef-param-type2/test.desc b/regression/goto-instrument-typedef/typedef-param-type2/test.desc new file mode 100644 index 00000000000..53cdc42193e --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-param-type2/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +"--show-symbol-table" +// 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 diff --git a/regression/goto-instrument-typedef/typedef-param-type3/main.c b/regression/goto-instrument-typedef/typedef-param-type3/main.c new file mode 100644 index 00000000000..4d542e10c13 --- /dev/null +++ b/regression/goto-instrument-typedef/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) +{ +} diff --git a/regression/goto-instrument-typedef/typedef-param-type3/test.desc b/regression/goto-instrument-typedef/typedef-param-type3/test.desc new file mode 100644 index 00000000000..6ba9d61f8ca --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-param-type3/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +"--show-symbol-table" +// 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 diff --git a/regression/goto-instrument-typedef/typedef-param-union1/main.c b/regression/goto-instrument-typedef/typedef-param-union1/main.c new file mode 100644 index 00000000000..8f961614e5d --- /dev/null +++ b/regression/goto-instrument-typedef/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) +{ +} diff --git a/regression/goto-instrument-typedef/typedef-param-union1/test.desc b/regression/goto-instrument-typedef/typedef-param-union1/test.desc new file mode 100644 index 00000000000..466dd76ed52 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-param-union1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// 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 diff --git a/regression/goto-instrument-typedef/typedef-return-anon-struct1/main.c b/regression/goto-instrument-typedef/typedef-return-anon-struct1/main.c new file mode 100644 index 00000000000..0195b955cdd --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-anon-struct1/main.c @@ -0,0 +1,12 @@ + +typedef struct +{ + int x; + float y; +} MYSTRUCT; + +MYSTRUCT fun() +{ + MYSTRUCT return_variable = {.x = 1, .y = 3.14f}; + return return_variable; +} diff --git a/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc b/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc new file mode 100644 index 00000000000..47964f71f66 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: return\nMode\.+: C\nType\.+: MYSTRUCT +Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(\) +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-return-anon-union1/main.c b/regression/goto-instrument-typedef/typedef-return-anon-union1/main.c new file mode 100644 index 00000000000..3bc7d19d5b7 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-anon-union1/main.c @@ -0,0 +1,15 @@ + +typedef union +{ + int x; + float y; +} MYUNION; + + +MYUNION fun() +{ + MYUNION return_variable = {1}; + return return_variable; +} + + diff --git a/regression/goto-instrument-typedef/typedef-return-anon-union1/test.desc b/regression/goto-instrument-typedef/typedef-return-anon-union1/test.desc new file mode 100644 index 00000000000..5a8d1b2062d --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-anon-union1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: fun\nMode\.+: C\nType\.+: MYUNION \(\) +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-return-struct1/main.c b/regression/goto-instrument-typedef/typedef-return-struct1/main.c new file mode 100644 index 00000000000..30c1323555c --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-struct1/main.c @@ -0,0 +1,20 @@ + +typedef struct tag_struct_name +{ + int x; + float y; +} MYSTRUCT; + +struct tag_struct_name fun() +{ + struct tag_struct_name return_variable = { .x = 1, .y = 3.14f}; + return return_variable; +} + +MYSTRUCT fun2() +{ + MYSTRUCT return_variable = { .x = 1, .y = 3.14f}; + return return_variable; +} + + diff --git a/regression/goto-instrument-typedef/typedef-return-struct1/test.desc b/regression/goto-instrument-typedef/typedef-return-struct1/test.desc new file mode 100644 index 00000000000..eade5942ac8 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-struct1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: fun\nMode\.+: C\nType\.+: struct tag_struct_name \(\) +Base name\.+: fun2\nMode\.+: C\nType\.+: MYSTRUCT \(\) +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-return-type1/main.c b/regression/goto-instrument-typedef/typedef-return-type1/main.c new file mode 100644 index 00000000000..1ba7f426f89 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-type1/main.c @@ -0,0 +1,12 @@ + +typedef int MYINT; + +int fun() +{ + return 4; +} + +MYINT fun2() +{ + return 5; +} diff --git a/regression/goto-instrument-typedef/typedef-return-type1/test.desc b/regression/goto-instrument-typedef/typedef-return-type1/test.desc new file mode 100644 index 00000000000..ba1b96ce6b6 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-type1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: fun\nMode\.+: C\nType\.+: signed int \(\) +Base name\.+: fun2\nMode\.+: C\nType\.+: MYINT \(\) +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-return-type2/main.c b/regression/goto-instrument-typedef/typedef-return-type2/main.c new file mode 100644 index 00000000000..0d94ab54da3 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-type2/main.c @@ -0,0 +1,13 @@ + +typedef int MYINT; +typedef int ALTINT; + +MYINT fun() +{ + +} + +ALTINT fun2() +{ + +} diff --git a/regression/goto-instrument-typedef/typedef-return-type2/test.desc b/regression/goto-instrument-typedef/typedef-return-type2/test.desc new file mode 100644 index 00000000000..1ecc9ea8e90 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-type2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(\) +Base name\.+: fun2\nMode\.+: C\nType\.+: ALTINT \(\) +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-return-type3/main.c b/regression/goto-instrument-typedef/typedef-return-type3/main.c new file mode 100644 index 00000000000..e246757c692 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-type3/main.c @@ -0,0 +1,12 @@ + +typedef int MYINT; +typedef MYINT CHAINEDINT; + +MYINT fun() +{ +} + +CHAINEDINT fun2() +{ + +} \ No newline at end of file diff --git a/regression/goto-instrument-typedef/typedef-return-type3/test.desc b/regression/goto-instrument-typedef/typedef-return-type3/test.desc new file mode 100644 index 00000000000..2401af3ce8d --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-type3/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(\) +Base name\.+: fun2\nMode\.+: C\nType\.+: CHAINEDINT \(\) +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-return-union1/main.c b/regression/goto-instrument-typedef/typedef-return-union1/main.c new file mode 100644 index 00000000000..ad69cb04545 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-union1/main.c @@ -0,0 +1,20 @@ + +typedef union tag_union_name +{ + int x; + float y; +} MYUNION; + +union tag_union_name fun() +{ + union tag_union_name return_variable = {1}; + return return_variable; +} + +MYUNION fun2() +{ + MYUNION return_variable = {1}; + return return_variable; +} + + diff --git a/regression/goto-instrument-typedef/typedef-return-union1/test.desc b/regression/goto-instrument-typedef/typedef-return-union1/test.desc new file mode 100644 index 00000000000..0855b28f479 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-return-union1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: fun\nMode\.+: C\nType\.+: union tag_union_name \(\) +Base name\.+: fun2\nMode\.+: C\nType\.+: MYUNION \(\) +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-struct1/main.c b/regression/goto-instrument-typedef/typedef-struct1/main.c new file mode 100644 index 00000000000..dac5abf77b8 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-struct1/main.c @@ -0,0 +1,12 @@ + +typedef struct tag_struct_name +{ + int x; + float y; +} MYSTRUCT; + +void fun() +{ + struct tag_struct_name tag_struct_var = {.x = 1, .y = 3.14f}; + MYSTRUCT mystruct_var = {.x = 3, .y = 2.1f}; +} diff --git a/regression/goto-instrument-typedef/typedef-struct1/test.desc b/regression/goto-instrument-typedef/typedef-struct1/test.desc new file mode 100644 index 00000000000..6a02f2d2174 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-struct1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: tag_struct_var\nMode\.+: C\nType\.+: struct tag_struct_name +Base name\.+: mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-struct2/main.c b/regression/goto-instrument-typedef/typedef-struct2/main.c new file mode 100644 index 00000000000..dac5abf77b8 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-struct2/main.c @@ -0,0 +1,12 @@ + +typedef struct tag_struct_name +{ + int x; + float y; +} MYSTRUCT; + +void fun() +{ + struct tag_struct_name tag_struct_var = {.x = 1, .y = 3.14f}; + MYSTRUCT mystruct_var = {.x = 3, .y = 2.1f}; +} diff --git a/regression/goto-instrument-typedef/typedef-struct2/test.desc b/regression/goto-instrument-typedef/typedef-struct2/test.desc new file mode 100644 index 00000000000..6a02f2d2174 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-struct2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: tag_struct_var\nMode\.+: C\nType\.+: struct tag_struct_name +Base name\.+: mystruct_var\nMode\.+: C\nType\.+: MYSTRUCT +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-type1/main.c b/regression/goto-instrument-typedef/typedef-type1/main.c new file mode 100644 index 00000000000..43f028c7772 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-type1/main.c @@ -0,0 +1,8 @@ + +typedef int MYINT; + +void fun() +{ + int int_var = 3; + MYINT myint_var = 5; +} diff --git a/regression/goto-instrument-typedef/typedef-type1/test.desc b/regression/goto-instrument-typedef/typedef-type1/test.desc new file mode 100644 index 00000000000..7599f1759c0 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-type1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: int_var\nMode\.+: C\nType\.+: signed int +Base name\.+: myint_var\nMode\.+: C\nType\.+: MYINT +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-type2/main.c b/regression/goto-instrument-typedef/typedef-type2/main.c new file mode 100644 index 00000000000..acb1cce2da4 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-type2/main.c @@ -0,0 +1,10 @@ + +typedef int MYINT; +typedef int ALTINT; + +void fun() +{ + int int_var = 3; + MYINT myint_var = 5; + ALTINT altint_var = 7; +} diff --git a/regression/goto-instrument-typedef/typedef-type2/test.desc b/regression/goto-instrument-typedef/typedef-type2/test.desc new file mode 100644 index 00000000000..3cf1e50a5a5 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-type2/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: int_var\nMode\.+: C\nType\.+: signed int +Base name\.+: myint_var\nMode\.+: C\nType\.+: MYINT +Base name\.+: altint_var\nMode\.+: C\nType\.+: ALTINT +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-type3/main.c b/regression/goto-instrument-typedef/typedef-type3/main.c new file mode 100644 index 00000000000..5855e0c24cb --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-type3/main.c @@ -0,0 +1,10 @@ + +typedef int MYINT; +typedef MYINT CHAINEDINT; + +void fun() +{ + int int_var = 3; + MYINT myint_var = 5; + CHAINEDINT chainedint_var = 5; +} diff --git a/regression/goto-instrument-typedef/typedef-type3/test.desc b/regression/goto-instrument-typedef/typedef-type3/test.desc new file mode 100644 index 00000000000..aca9069695c --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-type3/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: int_var\nMode\.+: C\nType\.+: signed int +Base name\.+: myint_var\nMode\.+: C\nType\.+: MYINT +Base name\.+: chainedint_var\nMode\.+: C\nType\.+: CHAINEDINT +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-type4/main.c b/regression/goto-instrument-typedef/typedef-type4/main.c new file mode 100644 index 00000000000..aa2ec9ad7fb --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-type4/main.c @@ -0,0 +1,8 @@ + +typedef int MYINT; + +void fun() +{ + int int_var = 3; + MYINT myint_var = 5, another_myint_var = 10; +} diff --git a/regression/goto-instrument-typedef/typedef-type4/test.desc b/regression/goto-instrument-typedef/typedef-type4/test.desc new file mode 100644 index 00000000000..28163714070 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-type4/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: int_var\nMode\.+: C\nType\.+: signed int +Base name\.+: myint_var\nMode\.+: C\nType\.+: MYINT +Base name\.+: another_myint_var\nMode\.+: C\nType\.+: MYINT +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-union1/main.c b/regression/goto-instrument-typedef/typedef-union1/main.c new file mode 100644 index 00000000000..6f56f3c731b --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-union1/main.c @@ -0,0 +1,12 @@ + +typedef union tag_union_name +{ + int x; + float y; +} MYUNION; + +void fun() +{ + union tag_union_name tag_union_var = {1}; + MYUNION myunion_var = {.y = 2.1f}; +} diff --git a/regression/goto-instrument-typedef/typedef-union1/test.desc b/regression/goto-instrument-typedef/typedef-union1/test.desc new file mode 100644 index 00000000000..8502d149cb1 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-union1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: tag_union_var\nMode\.+: C\nType\.+: union tag_union_name +Base name\.+: myunion_var\nMode\.+: C\nType\.+: MYUNION +-- +warning: ignoring diff --git a/regression/goto-instrument-typedef/typedef-union2/main.c b/regression/goto-instrument-typedef/typedef-union2/main.c new file mode 100644 index 00000000000..9ca707cf767 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-union2/main.c @@ -0,0 +1,12 @@ + +typedef union tag_union_name +{ + int x; + float y; +} MYUNION; + +void fun() +{ + union tag_union_name tag_union_var = {1}, another_tag_union_var = {1}; + MYUNION myunion_var = {.y = 2.1f}, another_myunion_var = {.y = 3.1f}; +} diff --git a/regression/goto-instrument-typedef/typedef-union2/test.desc b/regression/goto-instrument-typedef/typedef-union2/test.desc new file mode 100644 index 00000000000..0fc908a6ab5 --- /dev/null +++ b/regression/goto-instrument-typedef/typedef-union2/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +"--show-symbol-table" +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +Base name\.+: tag_union_var\nMode\.+: C\nType\.+: union tag_union_name +Base name\.+: another_tag_union_var\nMode\.+: C\nType\.+: union tag_union_name +Base name\.+: myunion_var\nMode\.+: C\nType\.+: MYUNION +Base name\.+: another_myunion_var\nMode\.+: C\nType\.+: MYUNION +-- +warning: ignoring diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index 4c82adc307a..7f9d0980583 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -146,6 +146,10 @@ typet ansi_c_declarationt::full_type( *p=type(); + // retain typedef for dump-c + if(get_is_typedef()) + result.set(ID_C_typedef, declarator.get_name()); + return result; } diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index f875bdec7d4..d82e81c0038 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -52,6 +52,7 @@ void c_typecheck_baset::typecheck_type(typet &type) c_qualifiers+=c_qualifierst(type.subtype()); bool packed=type.get_bool(ID_C_packed); exprt alignment=static_cast(type.find(ID_C_alignment)); + irept _typedef=type.find(ID_C_typedef); type.swap(type.subtype()); @@ -60,6 +61,8 @@ void c_typecheck_baset::typecheck_type(typet &type) type.set(ID_C_packed, true); if(alignment.is_not_nil()) type.add(ID_C_alignment, alignment); + if(_typedef.is_not_nil()) + type.add(ID_C_typedef, _typedef); return; // done } diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 86bd4183b91..401c96d64d1 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -232,6 +232,11 @@ std::string expr2ct::convert_rec( std::string d= declarator==""?declarator:" "+declarator; + if(src.find(ID_C_typedef).is_not_nil()) + { + return q+id2string(src.get(ID_C_typedef))+d; + } + if(src.id()==ID_bool) { return q+"_Bool"+d; diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index 066a5f831cc..f1938026621 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -251,6 +251,7 @@ concatenation infinity return_type typedef +C_typedef #typedef extern static auto