Skip to content

Commit 8e439ea

Browse files
committed
C front-end: ignore or reject conflicting function redeclaration
A declaration of a function currently being type checked should not replace the existing declaration. To accomplish this, make sure a definition `type name() { ... }` fixes the type of `name` to have no parameters and no ellipsis. This, more precise, typing highlighted a bug in the goto-harness/parameter_and_global_variable_distinction regression test (and the underlying implementation!), which assumed that the type of `int (*fptr_t)(void)` did not match `int call_f()`. Test generated by C-Reduce, starting from an SV-COMP task.
1 parent 536d6a2 commit 8e439ea

File tree

24 files changed

+96
-38
lines changed

24 files changed

+96
-38
lines changed
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#ifdef same_return_type
2+
# define T int
3+
#else
4+
# define T struct b
5+
#endif
6+
7+
int a()
8+
{
9+
T a(c);
10+
}
11+
12+
int main()
13+
{
14+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
-Dsame_return_type
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
Invariant check failed
8+
^CONVERSION ERROR$
9+
--
10+
This previously triggered the following (undesired) invariant violation:
11+
File: ../src/goto-programs/goto_convert_functions.cpp:167 function: convert_function
12+
Condition: parameter identifier should not be empty
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE test-c++-front-end
2+
main.c
3+
4+
^EXIT=(64|1)$
5+
^SIGNAL=0$
6+
(function symbol 'a' redefined with a different type|symbol 'c' is unknown)
7+
^CONVERSION ERROR$
8+
--
9+
Invariant check failed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,6 @@ activate-multi-line-match
66
^EXIT=0$
77
^SIGNAL=0$
88
Base name\.+: return'\nMode\.+: C\nType\.+: MYSTRUCT
9-
Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(\)
9+
Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(void\)
1010
--
1111
warning: ignoring

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ main.c
55
activate-multi-line-match
66
^EXIT=0$
77
^SIGNAL=0$
8-
Base name\.+: fun\nMode\.+: C\nType\.+: MYUNION \(\)
8+
Base name\.+: fun\nMode\.+: C\nType\.+: MYUNION \(void\)
99
--
1010
warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
activate-multi-line-match
66
^EXIT=0$
77
^SIGNAL=0$
8-
Base name\.+: fun\nMode\.+: C\nType\.+: struct tag_struct_name \(\)
9-
Base name\.+: fun2\nMode\.+: C\nType\.+: MYSTRUCT \(\)
8+
Base name\.+: fun\nMode\.+: C\nType\.+: struct tag_struct_name \(void\)
9+
Base name\.+: fun2\nMode\.+: C\nType\.+: MYSTRUCT \(void\)
1010
--
1111
warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
activate-multi-line-match
66
^EXIT=0$
77
^SIGNAL=0$
8-
Base name\.+: fun\nMode\.+: C\nType\.+: signed int \(\)
9-
Base name\.+: fun2\nMode\.+: C\nType\.+: MYINT \(\)
8+
Base name\.+: fun\nMode\.+: C\nType\.+: signed int \(void\)
9+
Base name\.+: fun2\nMode\.+: C\nType\.+: MYINT \(void\)
1010
--
1111
warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
activate-multi-line-match
66
^EXIT=0$
77
^SIGNAL=0$
8-
Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(\)
9-
Base name\.+: fun2\nMode\.+: C\nType\.+: ALTINT \(\)
8+
Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(void\)
9+
Base name\.+: fun2\nMode\.+: C\nType\.+: ALTINT \(void\)
1010
--
1111
warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ main.c
33
--show-symbol-table --function fun
44
// Enable multi-line checking
55
activate-multi-line-match
6-
Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(\)
7-
Base name\.+: fun2\nMode\.+: C\nType\.+: CHAINEDINT \(\)
6+
Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(void\)
7+
Base name\.+: fun2\nMode\.+: C\nType\.+: CHAINEDINT \(void\)
88
^EXIT=0$
99
^SIGNAL=0$
1010
--

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
activate-multi-line-match
66
^EXIT=0$
77
^SIGNAL=0$
8-
Base name\.+: fun\nMode\.+: C\nType\.+: union tag_union_name \(\)
9-
Base name\.+: fun2\nMode\.+: C\nType\.+: MYUNION \(\)
8+
Base name\.+: fun\nMode\.+: C\nType\.+: union tag_union_name \(void\)
9+
Base name\.+: fun2\nMode\.+: C\nType\.+: MYUNION \(void\)
1010
--
1111
warning: ignoring

0 commit comments

Comments
 (0)