Merge pull request #5694 from tautschnig/remove-ellipsis

tautschnig · web-flow · commit 1911a2e22e52 · 2022-12-12T14:35:49.000+01:00
C front-end: ignore or reject conflicting function redeclaration
diff --git a/regression/ansi-c/invalid_redeclaration1/main.c b/regression/ansi-c/invalid_redeclaration1/main.c
@@ -0,0 +1,14 @@
+#ifdef same_return_type
+#  define T int
+#else
+#  define T struct b
+#endif
+
+int a()
+{
+  T a(c);
+}
+
+int main()
+{
+}
diff --git a/regression/ansi-c/invalid_redeclaration1/test-same_type.desc b/regression/ansi-c/invalid_redeclaration1/test-same_type.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+-Dsame_return_type
+^EXIT=0$
+^SIGNAL=0$
+--
+Invariant check failed
+^CONVERSION ERROR$
+--
+This previously triggered the following (undesired) invariant violation:
+File: ../src/goto-programs/goto_convert_functions.cpp:167 function: convert_function
+Condition: parameter identifier should not be empty
diff --git a/regression/ansi-c/invalid_redeclaration1/test.desc b/regression/ansi-c/invalid_redeclaration1/test.desc
@@ -0,0 +1,9 @@
+CORE test-c++-front-end
+main.c
+
+^EXIT=(64|1)$
+^SIGNAL=0$
+(function symbol 'a' redefined with a different type|symbol 'c' is unknown)
+^CONVERSION ERROR$
+--
+Invariant check failed
diff --git a/regression/cbmc/typedef-return-anon-struct1/test.desc b/regression/cbmc/typedef-return-anon-struct1/test.desc
@@ -6,6 +6,6 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 Base name\.+: return'\nMode\.+: C\nType\.+: MYSTRUCT
-Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(void\)
 --
 warning: ignoring
diff --git a/regression/cbmc/typedef-return-anon-union1/test.desc b/regression/cbmc/typedef-return-anon-union1/test.desc
@@ -5,6 +5,6 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-Base name\.+: fun\nMode\.+: C\nType\.+: MYUNION \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: MYUNION \(void\)
 --
 warning: ignoring
diff --git a/regression/cbmc/typedef-return-struct1/test.desc b/regression/cbmc/typedef-return-struct1/test.desc
@@ -5,7 +5,7 @@ main.c
 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 \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: struct tag_struct_name \(void\)
+Base name\.+: fun2\nMode\.+: C\nType\.+: MYSTRUCT \(void\)
 --
 warning: ignoring
diff --git a/regression/cbmc/typedef-return-type1/test.desc b/regression/cbmc/typedef-return-type1/test.desc
@@ -5,7 +5,7 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-Base name\.+: fun\nMode\.+: C\nType\.+: signed int \(\)
-Base name\.+: fun2\nMode\.+: C\nType\.+: MYINT \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: signed int \(void\)
+Base name\.+: fun2\nMode\.+: C\nType\.+: MYINT \(void\)
 --
 warning: ignoring
diff --git a/regression/cbmc/typedef-return-type2/test.desc b/regression/cbmc/typedef-return-type2/test.desc
@@ -5,7 +5,7 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(\)
-Base name\.+: fun2\nMode\.+: C\nType\.+: ALTINT \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(void\)
+Base name\.+: fun2\nMode\.+: C\nType\.+: ALTINT \(void\)
 --
 warning: ignoring
diff --git a/regression/cbmc/typedef-return-type3/test.desc b/regression/cbmc/typedef-return-type3/test.desc
@@ -3,8 +3,8 @@ main.c
 --show-symbol-table --function fun
 // Enable multi-line checking
 activate-multi-line-match
-Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(\)
-Base name\.+: fun2\nMode\.+: C\nType\.+: CHAINEDINT \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(void\)
+Base name\.+: fun2\nMode\.+: C\nType\.+: CHAINEDINT \(void\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc/typedef-return-union1/test.desc b/regression/cbmc/typedef-return-union1/test.desc
@@ -5,7 +5,7 @@ main.c
 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 \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: union tag_union_name \(void\)
+Base name\.+: fun2\nMode\.+: C\nType\.+: MYUNION \(void\)
 --
 warning: ignoring
diff --git a/regression/contracts-dfcc/named-contracts/test-contract-signature-conflict.desc b/regression/contracts-dfcc/named-contracts/test-contract-signature-conflict.desc
@@ -1,8 +1,8 @@
 CORE
 main-contract-signature-conflict.c
 --dfcc main --enforce-contract foo
-^.*function 'foo' and the corresponding pure contract symbol 'contract::foo' have incompatible type signatures.*$
-^EXIT=6$
+function symbol 'foo' redefined with a different type
+^EXIT=(64|1)$
 ^SIGNAL=0$
 --
 --
diff --git a/regression/contracts/named-contracts/test-contract-signature-conflict.desc b/regression/contracts/named-contracts/test-contract-signature-conflict.desc
@@ -1,8 +1,8 @@
 CORE
 main-contract-signature-conflict.c
 --enforce-contract foo
-^Contract of 'foo' has different signature\.$
-^EXIT=6$
+function symbol 'foo' redefined with a different type
+^EXIT=(64|1)$
 ^SIGNAL=0$
 --
 --
diff --git a/regression/goto-harness/parameter_and_global_variable_distinction/test.c b/regression/goto-harness/parameter_and_global_variable_distinction/test.c
@@ -6,8 +6,8 @@ fptr_t f;
 
 int call_f()
 {
-  assert(f != ((void *)0));
-  return f();
+  assert(f == ((void *)0));
+  return 0;
 }
 
 void function(fptr_t f)
diff --git a/regression/goto-harness/parameter_and_global_variable_distinction/test.desc b/regression/goto-harness/parameter_and_global_variable_distinction/test.desc
@@ -5,6 +5,6 @@ test.c
 ^SIGNAL=0$
 \[function.assertion.1\] line \d+ assertion f\(\) == call_f\(\): SUCCESS
 \[function.assertion.2\] line \d+ assertion f != \(\(void \*\)0\): FAILURE
-\[call_f.assertion.1\] line \d+ assertion f != \(\(void \*\)0\): SUCCESS
+\[call_f.assertion.1\] line \d+ assertion f == \(\(void \*\)0\): SUCCESS
 --
 ^warning: ignoring
diff --git a/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc b/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc
@@ -6,6 +6,6 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 Base name\.+: return'\nMode\.+: C\nType\.+: MYSTRUCT
-Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: MYSTRUCT \(void\)
 --
 warning: ignoring
diff --git a/regression/goto-instrument-typedef/typedef-return-anon-union1/test.desc b/regression/goto-instrument-typedef/typedef-return-anon-union1/test.desc
@@ -5,6 +5,6 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-Base name\.+: fun\nMode\.+: C\nType\.+: MYUNION \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: MYUNION \(void\)
 --
 warning: ignoring
diff --git a/regression/goto-instrument-typedef/typedef-return-struct1/test.desc b/regression/goto-instrument-typedef/typedef-return-struct1/test.desc
@@ -5,7 +5,7 @@ main.c
 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 \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: struct tag_struct_name \(void\)
+Base name\.+: fun2\nMode\.+: C\nType\.+: MYSTRUCT \(void\)
 --
 warning: ignoring
diff --git a/regression/goto-instrument-typedef/typedef-return-type1/test.desc b/regression/goto-instrument-typedef/typedef-return-type1/test.desc
@@ -5,7 +5,7 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-Base name\.+: fun\nMode\.+: C\nType\.+: signed int \(\)
-Base name\.+: fun2\nMode\.+: C\nType\.+: MYINT \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: signed int \(void\)
+Base name\.+: fun2\nMode\.+: C\nType\.+: MYINT \(void\)
 --
 warning: ignoring
diff --git a/regression/goto-instrument-typedef/typedef-return-type2/test.desc b/regression/goto-instrument-typedef/typedef-return-type2/test.desc
@@ -5,7 +5,7 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(\)
-Base name\.+: fun2\nMode\.+: C\nType\.+: ALTINT \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(void\)
+Base name\.+: fun2\nMode\.+: C\nType\.+: ALTINT \(void\)
 --
 warning: ignoring
diff --git a/regression/goto-instrument-typedef/typedef-return-type3/test.desc b/regression/goto-instrument-typedef/typedef-return-type3/test.desc
@@ -3,8 +3,8 @@ main.c
 --show-symbol-table
 // Enable multi-line checking
 activate-multi-line-match
-Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(\)
-Base name\.+: fun2\nMode\.+: C\nType\.+: CHAINEDINT \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: MYINT \(void\)
+Base name\.+: fun2\nMode\.+: C\nType\.+: CHAINEDINT \(void\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument-typedef/typedef-return-union1/test.desc b/regression/goto-instrument-typedef/typedef-return-union1/test.desc
@@ -5,7 +5,7 @@ main.c
 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 \(\)
+Base name\.+: fun\nMode\.+: C\nType\.+: union tag_union_name \(void\)
+Base name\.+: fun2\nMode\.+: C\nType\.+: MYUNION \(void\)
 --
 warning: ignoring
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
@@ -373,6 +373,17 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
     code_typet &old_ct=to_code_type(old_symbol.type);
     code_typet &new_ct=to_code_type(new_symbol.type);
 
+    if(
+      old_ct.return_type() != new_ct.return_type() &&
+      !old_ct.get_bool(ID_C_incomplete))
+    {
+      throw invalid_source_file_exceptiont{
+        "function symbol '" + id2string(new_symbol.display_name()) +
+          "' redefined with a different type:\n" +
+          "Original: " + to_string(old_symbol.type) + "\n" +
+          "     New: " + to_string(new_symbol.type),
+        new_symbol.location};
+    }
     const bool inlined = old_ct.get_inlined() || new_ct.get_inlined();
 
     if(old_ct.has_ellipsis() && !new_ct.has_ellipsis())
@@ -589,6 +600,12 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
   labels_used.clear();
   labels_defined.clear();
 
+  // A function declaration int foo(); does not specify the parameter list, but
+  // a function definition int foo() { ... } does fix the parameter list to be
+  // empty.
+  if(code_type.parameters().empty() && code_type.has_ellipsis())
+    code_type.remove_ellipsis();
+
   // fix type
   symbol.value.type()=code_type;
 
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
@@ -549,11 +549,9 @@ get_contract(const irep_idt &function, const namespacet &ns)
   }
 
   const auto &type = to_code_with_contract_type(contract_sym->type);
-  if(type != function_symbol.type)
-  {
-    throw invalid_input_exceptiont(
-      "Contract of '" + function_str + "' has different signature.");
-  }
+  DATA_INVARIANT(
+    type == function_symbol.type,
+    "front-end should have rejected re-declarations with a different type");
 
   return type;
 }
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
@@ -853,7 +853,11 @@ void goto_convertt::do_function_call_symbol(
   {
     do_function_call_symbol(*symbol);
 
-    code_function_callt function_call(lhs, function, arguments);
+    // use symbol->symbol_expr() to ensure we use the type from the symbol table
+    code_function_callt function_call(
+      lhs,
+      symbol->symbol_expr().with_source_location<symbol_exprt>(function),
+      arguments);
     function_call.add_source_location() = function.source_location();
 
     // remove void-typed assignments, which may have been created when the
@@ -1495,7 +1499,11 @@ void goto_convertt::do_function_call_symbol(
     do_function_call_symbol(*symbol);
 
     // insert function call
-    code_function_callt function_call(lhs, function, arguments);
+    // use symbol->symbol_expr() to ensure we use the type from the symbol table
+    code_function_callt function_call(
+      lhs,
+      symbol->symbol_expr().with_source_location<symbol_exprt>(function),
+      arguments);
     function_call.add_source_location()=function.source_location();
 
     // remove void-typed assignments, which may have been created when the
