Skip to content

Commit 1911a2e

Browse files
tautschnigtautschnig
authored
Merge pull request #5694 from tautschnig/remove-ellipsis
C front-end: ignore or reject conflicting function redeclaration
2 parents 536d6a2 + 8e439ea commit 1911a2e

File tree

24 files changed

+96
-38
lines changed

24 files changed

+96
-38
lines changed

‎regression/ansi-c/invalid_redeclaration1/main.c

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+
}

‎regression/ansi-c/invalid_redeclaration1/test-same_type.desc

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

‎regression/ansi-c/invalid_redeclaration1/test.desc

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

‎regression/contracts-dfcc/named-contracts/test-contract-signature-conflict.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main-contract-signature-conflict.c
33
--dfcc main --enforce-contract foo
4-
^.*function 'foo' and the corresponding pure contract symbol 'contract::foo' have incompatible type signatures.*$
5-
^EXIT=6$
4+
function symbol 'foo' redefined with a different type
5+
^EXIT=(64|1)$
66
^SIGNAL=0$
77
--
88
--

‎regression/contracts/named-contracts/test-contract-signature-conflict.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main-contract-signature-conflict.c
33
--enforce-contract foo
4-
^Contract of 'foo' has different signature\.$
5-
^EXIT=6$
4+
function symbol 'foo' redefined with a different type
5+
^EXIT=(64|1)$
66
^SIGNAL=0$
77
--
88
--

‎regression/goto-harness/parameter_and_global_variable_distinction/test.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ fptr_t f;
66

77
int call_f()
88
{
9-
assert(f != ((void *)0));
10-
return f();
9+
assert(f == ((void *)0));
10+
return 0;
1111
}
1212

1313
void function(fptr_t f)

‎regression/goto-harness/parameter_and_global_variable_distinction/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ test.c
55
^SIGNAL=0$
66
\[function.assertion.1\] line \d+ assertion f\(\) == call_f\(\): SUCCESS
77
\[function.assertion.2\] line \d+ assertion f != \(\(void \*\)0\): FAILURE
8-
\[call_f.assertion.1\] line \d+ assertion f != \(\(void \*\)0\): SUCCESS
8+
\[call_f.assertion.1\] line \d+ assertion f == \(\(void \*\)0\): SUCCESS
99
--
1010
^warning: ignoring

‎regression/goto-instrument-typedef/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/goto-instrument-typedef/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/goto-instrument-typedef/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/goto-instrument-typedef/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/goto-instrument-typedef/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/goto-instrument-typedef/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
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/goto-instrument-typedef/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

‎src/ansi-c/c_typecheck_base.cpp

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -373,6 +373,17 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
373373
code_typet &old_ct=to_code_type(old_symbol.type);
374374
code_typet &new_ct=to_code_type(new_symbol.type);
375375

376+
if(
377+
old_ct.return_type() != new_ct.return_type() &&
378+
!old_ct.get_bool(ID_C_incomplete))
379+
{
380+
throw invalid_source_file_exceptiont{
381+
"function symbol '" + id2string(new_symbol.display_name()) +
382+
"' redefined with a different type:\n" +
383+
"Original: " + to_string(old_symbol.type) + "\n" +
384+
" New: " + to_string(new_symbol.type),
385+
new_symbol.location};
386+
}
376387
const bool inlined = old_ct.get_inlined() || new_ct.get_inlined();
377388

378389
if(old_ct.has_ellipsis() && !new_ct.has_ellipsis())
@@ -589,6 +600,12 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
589600
labels_used.clear();
590601
labels_defined.clear();
591602

603+
// A function declaration int foo(); does not specify the parameter list, but
604+
// a function definition int foo() { ... } does fix the parameter list to be
605+
// empty.
606+
if(code_type.parameters().empty() && code_type.has_ellipsis())
607+
code_type.remove_ellipsis();
608+
592609
// fix type
593610
symbol.value.type()=code_type;
594611

‎src/goto-instrument/contracts/contracts.cpp

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -549,11 +549,9 @@ get_contract(const irep_idt &function, const namespacet &ns)
549549
}
550550

551551
const auto &type = to_code_with_contract_type(contract_sym->type);
552-
if(type != function_symbol.type)
553-
{
554-
throw invalid_input_exceptiont(
555-
"Contract of '" + function_str + "' has different signature.");
556-
}
552+
DATA_INVARIANT(
553+
type == function_symbol.type,
554+
"front-end should have rejected re-declarations with a different type");
557555

558556
return type;
559557
}

‎src/goto-programs/builtin_functions.cpp

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -853,7 +853,11 @@ void goto_convertt::do_function_call_symbol(
853853
{
854854
do_function_call_symbol(*symbol);
855855

856-
code_function_callt function_call(lhs, function, arguments);
856+
// use symbol->symbol_expr() to ensure we use the type from the symbol table
857+
code_function_callt function_call(
858+
lhs,
859+
symbol->symbol_expr().with_source_location<symbol_exprt>(function),
860+
arguments);
857861
function_call.add_source_location() = function.source_location();
858862

859863
// remove void-typed assignments, which may have been created when the
@@ -1495,7 +1499,11 @@ void goto_convertt::do_function_call_symbol(
14951499
do_function_call_symbol(*symbol);
14961500

14971501
// insert function call
1498-
code_function_callt function_call(lhs, function, arguments);
1502+
// use symbol->symbol_expr() to ensure we use the type from the symbol table
1503+
code_function_callt function_call(
1504+
lhs,
1505+
symbol->symbol_expr().with_source_location<symbol_exprt>(function),
1506+
arguments);
14991507
function_call.add_source_location()=function.source_location();
15001508

15011509
// remove void-typed assignments, which may have been created when the

0 commit comments

Comments
 (0)