From 35356bda51458669224a54408022483d5f852151 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 14 Dec 2016 15:00:30 +0000 Subject: [PATCH 01/14] keep typedefs when dumping c with --use-system-headers --- src/ansi-c/ansi_c_declaration.cpp | 4 ++++ src/ansi-c/c_typecheck_type.cpp | 3 +++ 2 files changed, 7 insertions(+) diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index 4c82adc307a..6834298a40b 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_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..909b254c611 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_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_typedef, _typedef); return; // done } From 08cf4ee55227be3959f5c34a1ba7a4c143df0d82 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 14 Dec 2016 17:10:50 +0000 Subject: [PATCH 02/14] Added initial collection of tests for typedef'd types Covers the basic cases of typedef-ing a normal type (int) --- regression/goto-instrument-typedef/Makefile | 31 +++++++++++++++++++ regression/goto-instrument-typedef/chain.sh | 13 ++++++++ .../typedef-type1/main.c | 8 +++++ .../typedef-type1/test.desc | 11 +++++++ .../typedef-type2/main.c | 10 ++++++ .../typedef-type2/test.desc | 12 +++++++ .../typedef-type3/main.c | 10 ++++++ .../typedef-type3/test.desc | 12 +++++++ 8 files changed, 107 insertions(+) create mode 100644 regression/goto-instrument-typedef/Makefile create mode 100755 regression/goto-instrument-typedef/chain.sh create mode 100644 regression/goto-instrument-typedef/typedef-type1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-type1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-type2/main.c create mode 100644 regression/goto-instrument-typedef/typedef-type2/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-type3/main.c create mode 100644 regression/goto-instrument-typedef/typedef-type3/test.desc 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..248ca155b8d --- /dev/null +++ b/regression/goto-instrument-typedef/chain.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +SRC=../../../src + +GC=$SRC/goto-cc/goto-cc +GI=$SRC/goto-instrument/goto-instrument + +OPTS=$1 +NAME=${2%.c} + +$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-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 From 99067de178170a6ac42a2a412c859ad7e8690319 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 14 Dec 2016 17:12:13 +0000 Subject: [PATCH 03/14] If a type has a typedef then use that when printing the type --- src/ansi-c/expr2c.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 86bd4183b91..4f31653d91a 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_typedef).is_not_nil()) + { + return q+id2string(src.get(ID_typedef))+d; + } + if(src.id()==ID_bool) { return q+"_Bool"+d; From eb7e551c4b9d53f537f8733a5329febf156c55c5 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 15 Dec 2016 12:29:56 +0000 Subject: [PATCH 04/14] Adding tests for structs and parameters using typedefs --- .../typedef-anon-struct1/main.c | 11 ++++++++++ .../typedef-anon-struct1/test.desc | 10 ++++++++++ .../typedef-param-anon-struct1/main.c | 11 ++++++++++ .../typedef-param-anon-struct1/test.desc | 10 ++++++++++ .../typedef-param-struct1/main.c | 10 ++++++++++ .../typedef-param-struct1/test.desc | 11 ++++++++++ .../typedef-param-type1/main.c | 7 +++++++ .../typedef-param-type1/test.desc | 11 ++++++++++ .../typedef-param-type2/main.c | 8 ++++++++ .../typedef-param-type2/test.desc | 12 +++++++++++ .../typedef-param-type3/main.c | 7 +++++++ .../typedef-param-type3/test.desc | 12 +++++++++++ .../typedef-return-anon-struct1/main.c | 12 +++++++++++ .../typedef-return-anon-struct1/test.desc | 11 ++++++++++ .../typedef-return-struct1/main.c | 20 +++++++++++++++++++ .../typedef-return-struct1/test.desc | 11 ++++++++++ .../typedef-return-type1/main.c | 12 +++++++++++ .../typedef-return-type1/test.desc | 11 ++++++++++ .../typedef-return-type2/main.c | 13 ++++++++++++ .../typedef-return-type2/test.desc | 11 ++++++++++ .../typedef-return-type3/main.c | 12 +++++++++++ .../typedef-return-type3/test.desc | 10 ++++++++++ .../typedef-struct1/main.c | 12 +++++++++++ .../typedef-struct1/test.desc | 11 ++++++++++ 24 files changed, 266 insertions(+) create mode 100644 regression/goto-instrument-typedef/typedef-anon-struct1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-anon-struct1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-param-anon-struct1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-param-anon-struct1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-param-struct1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-param-struct1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-param-type1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-param-type1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-param-type2/main.c create mode 100644 regression/goto-instrument-typedef/typedef-param-type2/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-param-type3/main.c create mode 100644 regression/goto-instrument-typedef/typedef-param-type3/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-return-anon-struct1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-return-struct1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-return-struct1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-return-type1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-return-type1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-return-type2/main.c create mode 100644 regression/goto-instrument-typedef/typedef-return-type2/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-return-type3/main.c create mode 100644 regression/goto-instrument-typedef/typedef-return-type3/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-struct1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-struct1/test.desc 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-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-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-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-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-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 From 0152f671316b24217bab8f15cb53cf3e7376e1cf Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Dec 2016 10:04:08 +0000 Subject: [PATCH 05/14] Improved chain.sh to remove old .gb files first Made the first step of the chain.sh remove the generated .gb file from previous runs. This ensures that if the goto-cc step fails, misleading results are not generated. --- regression/goto-instrument-typedef/chain.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/regression/goto-instrument-typedef/chain.sh b/regression/goto-instrument-typedef/chain.sh index 248ca155b8d..9cef4ffdfa4 100755 --- a/regression/goto-instrument-typedef/chain.sh +++ b/regression/goto-instrument-typedef/chain.sh @@ -8,6 +8,7 @@ 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 From e8dbc4086de7d78deeb107d8da526a63d51dafaa Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Dec 2016 10:51:26 +0000 Subject: [PATCH 06/14] Adding tests for union typedefs --- .../typedef-param-union1/main.c | 10 ++++++++++ .../typedef-param-union1/test.desc | 11 ++++++++++ .../typedef-return-union1/main.c | 20 +++++++++++++++++++ .../typedef-return-union1/test.desc | 11 ++++++++++ .../typedef-union1/main.c | 12 +++++++++++ .../typedef-union1/test.desc | 11 ++++++++++ 6 files changed, 75 insertions(+) create mode 100644 regression/goto-instrument-typedef/typedef-param-union1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-param-union1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-return-union1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-return-union1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-union1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-union1/test.desc 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-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-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 From 5dd0c8a63cf871e12d6f5646ce276c8138d5b4ba Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Dec 2016 12:04:07 +0000 Subject: [PATCH 07/14] Adding const variables tests The tests relating to structs and unions are marked as known bugs as they are related to #355 --- .../typedef-const-struct1/main.c | 12 ++++++++++++ .../typedef-const-struct1/test.desc | 11 +++++++++++ .../typedef-const-type1/main.c | 8 ++++++++ .../typedef-const-type1/test.desc | 11 +++++++++++ .../typedef-const-union1/main.c | 12 ++++++++++++ .../typedef-const-union1/test.desc | 11 +++++++++++ 6 files changed, 65 insertions(+) create mode 100644 regression/goto-instrument-typedef/typedef-const-struct1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-const-struct1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-const-type1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-const-type1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-const-union1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-const-union1/test.desc 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 From bb09401a54699cfd236aa497a6703a23d4f8297d Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Dec 2016 14:22:20 +0000 Subject: [PATCH 08/14] Adding tests for anonymous unions These mirror the tests for anonymous structs --- .../typedef-anon-union1/main.c | 11 +++++++++++ .../typedef-anon-union1/test.desc | 10 ++++++++++ .../typedef-param-anon-union1/main.c | 10 ++++++++++ .../typedef-param-anon-union1/test.desc | 10 ++++++++++ .../typedef-return-anon-union1/main.c | 15 +++++++++++++++ .../typedef-return-anon-union1/test.desc | 10 ++++++++++ 6 files changed, 66 insertions(+) create mode 100644 regression/goto-instrument-typedef/typedef-anon-union1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-anon-union1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-param-anon-union1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-param-anon-union1/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-return-anon-union1/main.c create mode 100644 regression/goto-instrument-typedef/typedef-return-anon-union1/test.desc 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-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-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 From 79f1638a4b0f14a48fec81c29f1803f6a5e9058a Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Dec 2016 15:00:11 +0000 Subject: [PATCH 09/14] Adding regression tests for multiple declarations on one line This was mainly to check the declarator part of the conversion wasn't being tripped up by the typedef printing --- .../typedef-anon-struct2/main.c | 11 +++++++++++ .../typedef-anon-struct2/test.desc | 11 +++++++++++ .../typedef-anon-union2/main.c | 11 +++++++++++ .../typedef-anon-union2/test.desc | 11 +++++++++++ .../goto-instrument-typedef/typedef-struct2/main.c | 12 ++++++++++++ .../typedef-struct2/test.desc | 11 +++++++++++ .../goto-instrument-typedef/typedef-type4/main.c | 8 ++++++++ .../goto-instrument-typedef/typedef-type4/test.desc | 12 ++++++++++++ .../goto-instrument-typedef/typedef-union2/main.c | 12 ++++++++++++ .../typedef-union2/test.desc | 13 +++++++++++++ 10 files changed, 112 insertions(+) create mode 100644 regression/goto-instrument-typedef/typedef-anon-struct2/main.c create mode 100644 regression/goto-instrument-typedef/typedef-anon-struct2/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-anon-union2/main.c create mode 100644 regression/goto-instrument-typedef/typedef-anon-union2/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-struct2/main.c create mode 100644 regression/goto-instrument-typedef/typedef-struct2/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-type4/main.c create mode 100644 regression/goto-instrument-typedef/typedef-type4/test.desc create mode 100644 regression/goto-instrument-typedef/typedef-union2/main.c create mode 100644 regression/goto-instrument-typedef/typedef-union2/test.desc 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-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-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-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-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 From fc8d7c6e473383c5030f474a10558c950bc9d22f Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Dec 2016 15:03:54 +0000 Subject: [PATCH 10/14] Added regressions for typedefs on the source file Since there seemed to be some sublte differences in the data that was maintained whether you ran goto-cc first (independently) or directly fed the .c file into CBMC. These tests replicate the behaviour of tests found in regressions/goto-instrument-typedef/ --- regression/Makefile | 1 + regression/cbmc/typedef-anon-struct1/main.c | 11 ++++++++++ .../cbmc/typedef-anon-struct1/test.desc | 10 ++++++++++ regression/cbmc/typedef-anon-struct2/main.c | 11 ++++++++++ .../cbmc/typedef-anon-struct2/test.desc | 11 ++++++++++ regression/cbmc/typedef-anon-union1/main.c | 11 ++++++++++ regression/cbmc/typedef-anon-union1/test.desc | 10 ++++++++++ regression/cbmc/typedef-anon-union2/main.c | 11 ++++++++++ regression/cbmc/typedef-anon-union2/test.desc | 11 ++++++++++ regression/cbmc/typedef-const-struct1/main.c | 12 +++++++++++ .../cbmc/typedef-const-struct1/test.desc | 11 ++++++++++ regression/cbmc/typedef-const-type1/main.c | 8 ++++++++ regression/cbmc/typedef-const-type1/test.desc | 11 ++++++++++ regression/cbmc/typedef-const-union1/main.c | 12 +++++++++++ .../cbmc/typedef-const-union1/test.desc | 11 ++++++++++ .../cbmc/typedef-param-anon-struct1/main.c | 11 ++++++++++ .../cbmc/typedef-param-anon-struct1/test.desc | 10 ++++++++++ .../cbmc/typedef-param-anon-union1/main.c | 10 ++++++++++ .../cbmc/typedef-param-anon-union1/test.desc | 10 ++++++++++ regression/cbmc/typedef-param-struct1/main.c | 10 ++++++++++ .../cbmc/typedef-param-struct1/test.desc | 11 ++++++++++ regression/cbmc/typedef-param-type1/main.c | 7 +++++++ regression/cbmc/typedef-param-type1/test.desc | 11 ++++++++++ regression/cbmc/typedef-param-type2/main.c | 8 ++++++++ regression/cbmc/typedef-param-type2/test.desc | 12 +++++++++++ regression/cbmc/typedef-param-type3/main.c | 7 +++++++ regression/cbmc/typedef-param-type3/test.desc | 12 +++++++++++ regression/cbmc/typedef-param-union1/main.c | 10 ++++++++++ .../cbmc/typedef-param-union1/test.desc | 11 ++++++++++ .../cbmc/typedef-return-anon-struct1/main.c | 12 +++++++++++ .../typedef-return-anon-struct1/test.desc | 11 ++++++++++ .../cbmc/typedef-return-anon-union1/main.c | 15 ++++++++++++++ .../cbmc/typedef-return-anon-union1/test.desc | 10 ++++++++++ regression/cbmc/typedef-return-struct1/main.c | 20 +++++++++++++++++++ .../cbmc/typedef-return-struct1/test.desc | 11 ++++++++++ regression/cbmc/typedef-return-type1/main.c | 12 +++++++++++ .../cbmc/typedef-return-type1/test.desc | 11 ++++++++++ regression/cbmc/typedef-return-type2/main.c | 13 ++++++++++++ .../cbmc/typedef-return-type2/test.desc | 11 ++++++++++ regression/cbmc/typedef-return-type3/main.c | 12 +++++++++++ .../cbmc/typedef-return-type3/test.desc | 10 ++++++++++ regression/cbmc/typedef-return-union1/main.c | 20 +++++++++++++++++++ .../cbmc/typedef-return-union1/test.desc | 11 ++++++++++ regression/cbmc/typedef-struct1/main.c | 12 +++++++++++ regression/cbmc/typedef-struct1/test.desc | 11 ++++++++++ regression/cbmc/typedef-struct2/main.c | 12 +++++++++++ regression/cbmc/typedef-struct2/test.desc | 11 ++++++++++ regression/cbmc/typedef-type1/main.c | 8 ++++++++ regression/cbmc/typedef-type1/test.desc | 11 ++++++++++ regression/cbmc/typedef-type2/main.c | 10 ++++++++++ regression/cbmc/typedef-type2/test.desc | 12 +++++++++++ regression/cbmc/typedef-type3/main.c | 10 ++++++++++ regression/cbmc/typedef-type3/test.desc | 12 +++++++++++ regression/cbmc/typedef-type4/main.c | 8 ++++++++ regression/cbmc/typedef-type4/test.desc | 12 +++++++++++ regression/cbmc/typedef-union1/main.c | 12 +++++++++++ regression/cbmc/typedef-union1/test.desc | 11 ++++++++++ regression/cbmc/typedef-union2/main.c | 12 +++++++++++ regression/cbmc/typedef-union2/test.desc | 13 ++++++++++++ 59 files changed, 648 insertions(+) create mode 100644 regression/cbmc/typedef-anon-struct1/main.c create mode 100644 regression/cbmc/typedef-anon-struct1/test.desc create mode 100644 regression/cbmc/typedef-anon-struct2/main.c create mode 100644 regression/cbmc/typedef-anon-struct2/test.desc create mode 100644 regression/cbmc/typedef-anon-union1/main.c create mode 100644 regression/cbmc/typedef-anon-union1/test.desc create mode 100644 regression/cbmc/typedef-anon-union2/main.c create mode 100644 regression/cbmc/typedef-anon-union2/test.desc create mode 100644 regression/cbmc/typedef-const-struct1/main.c create mode 100644 regression/cbmc/typedef-const-struct1/test.desc create mode 100644 regression/cbmc/typedef-const-type1/main.c create mode 100644 regression/cbmc/typedef-const-type1/test.desc create mode 100644 regression/cbmc/typedef-const-union1/main.c create mode 100644 regression/cbmc/typedef-const-union1/test.desc create mode 100644 regression/cbmc/typedef-param-anon-struct1/main.c create mode 100644 regression/cbmc/typedef-param-anon-struct1/test.desc create mode 100644 regression/cbmc/typedef-param-anon-union1/main.c create mode 100644 regression/cbmc/typedef-param-anon-union1/test.desc create mode 100644 regression/cbmc/typedef-param-struct1/main.c create mode 100644 regression/cbmc/typedef-param-struct1/test.desc create mode 100644 regression/cbmc/typedef-param-type1/main.c create mode 100644 regression/cbmc/typedef-param-type1/test.desc create mode 100644 regression/cbmc/typedef-param-type2/main.c create mode 100644 regression/cbmc/typedef-param-type2/test.desc create mode 100644 regression/cbmc/typedef-param-type3/main.c create mode 100644 regression/cbmc/typedef-param-type3/test.desc create mode 100644 regression/cbmc/typedef-param-union1/main.c create mode 100644 regression/cbmc/typedef-param-union1/test.desc create mode 100644 regression/cbmc/typedef-return-anon-struct1/main.c create mode 100644 regression/cbmc/typedef-return-anon-struct1/test.desc create mode 100644 regression/cbmc/typedef-return-anon-union1/main.c create mode 100644 regression/cbmc/typedef-return-anon-union1/test.desc create mode 100644 regression/cbmc/typedef-return-struct1/main.c create mode 100644 regression/cbmc/typedef-return-struct1/test.desc create mode 100644 regression/cbmc/typedef-return-type1/main.c create mode 100644 regression/cbmc/typedef-return-type1/test.desc create mode 100644 regression/cbmc/typedef-return-type2/main.c create mode 100644 regression/cbmc/typedef-return-type2/test.desc create mode 100644 regression/cbmc/typedef-return-type3/main.c create mode 100644 regression/cbmc/typedef-return-type3/test.desc create mode 100644 regression/cbmc/typedef-return-union1/main.c create mode 100644 regression/cbmc/typedef-return-union1/test.desc create mode 100644 regression/cbmc/typedef-struct1/main.c create mode 100644 regression/cbmc/typedef-struct1/test.desc create mode 100644 regression/cbmc/typedef-struct2/main.c create mode 100644 regression/cbmc/typedef-struct2/test.desc create mode 100644 regression/cbmc/typedef-type1/main.c create mode 100644 regression/cbmc/typedef-type1/test.desc create mode 100644 regression/cbmc/typedef-type2/main.c create mode 100644 regression/cbmc/typedef-type2/test.desc create mode 100644 regression/cbmc/typedef-type3/main.c create mode 100644 regression/cbmc/typedef-type3/test.desc create mode 100644 regression/cbmc/typedef-type4/main.c create mode 100644 regression/cbmc/typedef-type4/test.desc create mode 100644 regression/cbmc/typedef-union1/main.c create mode 100644 regression/cbmc/typedef-union1/test.desc create mode 100644 regression/cbmc/typedef-union2/main.c create mode 100644 regression/cbmc/typedef-union2/test.desc 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/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 From 22e92672856cbe031c65464cbda3f92d47797ce6 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Dec 2016 15:35:27 +0000 Subject: [PATCH 11/14] Use ID_C_typedef rather than ID_typedef This is more consistent with other flags that do not affect the semantics of the program. --- src/ansi-c/ansi_c_declaration.cpp | 2 +- src/ansi-c/c_typecheck_type.cpp | 4 ++-- src/ansi-c/expr2c.cpp | 4 ++-- src/util/irep_ids.txt | 1 + 4 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index 6834298a40b..3f79252b867 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -148,7 +148,7 @@ typet ansi_c_declarationt::full_type( // retain typedef for dump-c if(get_is_typedef()) - result.set(ID_typedef,declarator.get_name()); + 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 909b254c611..d82e81c0038 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -52,7 +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_typedef); + irept _typedef=type.find(ID_C_typedef); type.swap(type.subtype()); @@ -62,7 +62,7 @@ void c_typecheck_baset::typecheck_type(typet &type) if(alignment.is_not_nil()) type.add(ID_C_alignment, alignment); if(_typedef.is_not_nil()) - type.add(ID_typedef, _typedef); + type.add(ID_C_typedef, _typedef); return; // done } diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 4f31653d91a..401c96d64d1 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -232,9 +232,9 @@ std::string expr2ct::convert_rec( std::string d= declarator==""?declarator:" "+declarator; - if(src.find(ID_typedef).is_not_nil()) + if(src.find(ID_C_typedef).is_not_nil()) { - return q+id2string(src.get(ID_typedef))+d; + return q+id2string(src.get(ID_C_typedef))+d; } if(src.id()==ID_bool) diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index 066a5f831cc..e581e70ea32 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -251,6 +251,7 @@ concatenation infinity return_type typedef +C_typedef extern static auto From 7c1aeb4e17aad8ffb20048e8de61c7f0f52b09f1 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 16 Jan 2017 18:10:30 +0000 Subject: [PATCH 12/14] Fixing relevant lint errors --- src/ansi-c/ansi_c_declaration.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index 3f79252b867..7f9d0980583 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -148,7 +148,7 @@ typet ansi_c_declarationt::full_type( // retain typedef for dump-c if(get_is_typedef()) - result.set(ID_C_typedef,declarator.get_name()); + result.set(ID_C_typedef, declarator.get_name()); return result; } From c64eaccbe88ad7762d3f725dcb375ac3d38201e2 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 17 Jan 2017 10:57:14 +0000 Subject: [PATCH 13/14] Fixed the failing ANSI-C test caused by typedef types not being equal Previously, basic types were being compared by directly calling operator== on the two types. However, we now add a flag to all types defined with a typedef saying what the typedef'd name was. This was causing the two types to not be equal. Now, instead of directly comparing them, we remove the ID_C_typedef flag from them if present and then compare the resulting types. Also added a few more checks to the test to cover some other typedef cases. --- .../ansi-c/gcc_types_compatible_p1/main.c | 12 +++++- .../ansi-c/gcc_types_compatible_p4/main.c | 27 +++++++++++++ .../ansi-c/gcc_types_compatible_p4/test.desc | 8 ++++ src/ansi-c/c_typecheck_base.h | 4 ++ src/ansi-c/c_typecheck_expr.cpp | 39 ++++++++++++++++++- 5 files changed, 87 insertions(+), 3 deletions(-) create mode 100644 regression/ansi-c/gcc_types_compatible_p4/main.c create mode 100644 regression/ansi-c/gcc_types_compatible_p4/test.desc 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/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 68191f54fe9..bad408a3c5c 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -262,6 +262,10 @@ class c_typecheck_baset: asm_label_mapt asm_label_map; void apply_asm_label(const irep_idt &asm_label, symbolt &symbol); + +private: + static bool are_types_equal_ignoring_typedef( + const typet type1, const typet &type2); }; #endif // CPROVER_ANSI_C_C_TYPECHECK_BASE_H diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 5961f64142e..4b721f9cf03 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -140,6 +140,8 @@ bool c_typecheck_baset::gcc_types_compatible_p( if(type1.id()==ID_c_enum) { if(type2.id()==ID_c_enum) // both are enums + // We don't need to remove the typedef flag here since as it is an enum + // we have already followed the enum tag to get to the underlying enum return type1==type2; // compares the tag else if(type2==type1.subtype()) return true; @@ -184,12 +186,13 @@ bool c_typecheck_baset::gcc_types_compatible_p( } else { - if(type1==type2) + if(are_types_equal_ignoring_typedef(type1, type2)) { // Need to distinguish e.g. long int from int or // long long int from long int. // The rules appear to match those of C++. - + // Isn't this explictly handled by checking type1==type2 (since + // operator== recursively checks all sub types). if(type1.get(ID_C_c_type)==type2.get(ID_C_c_type)) return true; } @@ -200,6 +203,38 @@ bool c_typecheck_baset::gcc_types_compatible_p( /*******************************************************************\ +Function: c_typecheck_baset::are_types_equal_ignoring_typedef + + Inputs: + type1 - the first type to compare + type2 - the second type to compare + + Outputs: True if the types are equal + + Purpose: To check whether two types are equal, ignoring if they have a + different typedef tag. We do this by explictly removing the + ID_C_typedef from the type before comparing. Then we just use + operator== to compare the resultant types. + +\*******************************************************************/ +bool c_typecheck_baset::are_types_equal_ignoring_typedef( + const typet type1, const typet &type2) +{ + typet non_typedefd_type1=type1; + typet non_typedefd_type2=type2; + if(type1.get(ID_C_typedef)!=ID_nil) + { + non_typedefd_type1.remove(ID_C_typedef); + } + if(type2.get(ID_C_typedef)!=ID_nil) + { + non_typedefd_type2.remove(ID_C_typedef); + } + return non_typedefd_type1==non_typedefd_type2; +} + +/*******************************************************************\ + Function: c_typecheck_baset::typecheck_expr_main Inputs: From eec7a5dcda6aee412a6ce542c6af5b2f05739d17 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 26 Jan 2017 15:11:13 +0000 Subject: [PATCH 14/14] Turn the ID_C_typedef into a comment This means that it will not be used to check types are equal, fixing the failing regression tests that were validating the types were equal (and they only differed by a typedef'd name). --- src/ansi-c/c_typecheck_base.h | 4 ---- src/ansi-c/c_typecheck_expr.cpp | 39 ++------------------------------- src/util/irep_ids.txt | 2 +- 3 files changed, 3 insertions(+), 42 deletions(-) diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index bad408a3c5c..68191f54fe9 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -262,10 +262,6 @@ class c_typecheck_baset: asm_label_mapt asm_label_map; void apply_asm_label(const irep_idt &asm_label, symbolt &symbol); - -private: - static bool are_types_equal_ignoring_typedef( - const typet type1, const typet &type2); }; #endif // CPROVER_ANSI_C_C_TYPECHECK_BASE_H diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 4b721f9cf03..5961f64142e 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -140,8 +140,6 @@ bool c_typecheck_baset::gcc_types_compatible_p( if(type1.id()==ID_c_enum) { if(type2.id()==ID_c_enum) // both are enums - // We don't need to remove the typedef flag here since as it is an enum - // we have already followed the enum tag to get to the underlying enum return type1==type2; // compares the tag else if(type2==type1.subtype()) return true; @@ -186,13 +184,12 @@ bool c_typecheck_baset::gcc_types_compatible_p( } else { - if(are_types_equal_ignoring_typedef(type1, type2)) + if(type1==type2) { // Need to distinguish e.g. long int from int or // long long int from long int. // The rules appear to match those of C++. - // Isn't this explictly handled by checking type1==type2 (since - // operator== recursively checks all sub types). + if(type1.get(ID_C_c_type)==type2.get(ID_C_c_type)) return true; } @@ -203,38 +200,6 @@ bool c_typecheck_baset::gcc_types_compatible_p( /*******************************************************************\ -Function: c_typecheck_baset::are_types_equal_ignoring_typedef - - Inputs: - type1 - the first type to compare - type2 - the second type to compare - - Outputs: True if the types are equal - - Purpose: To check whether two types are equal, ignoring if they have a - different typedef tag. We do this by explictly removing the - ID_C_typedef from the type before comparing. Then we just use - operator== to compare the resultant types. - -\*******************************************************************/ -bool c_typecheck_baset::are_types_equal_ignoring_typedef( - const typet type1, const typet &type2) -{ - typet non_typedefd_type1=type1; - typet non_typedefd_type2=type2; - if(type1.get(ID_C_typedef)!=ID_nil) - { - non_typedefd_type1.remove(ID_C_typedef); - } - if(type2.get(ID_C_typedef)!=ID_nil) - { - non_typedefd_type2.remove(ID_C_typedef); - } - return non_typedefd_type1==non_typedefd_type2; -} - -/*******************************************************************\ - Function: c_typecheck_baset::typecheck_expr_main Inputs: diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index e581e70ea32..f1938026621 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -251,7 +251,7 @@ concatenation infinity return_type typedef -C_typedef +C_typedef #typedef extern static auto