Merge pull request #6188 from tautschnig/array-linking

Linking forward declarations of arrays must not yield type casts

Author: kroening

regression/cbmc/Linking4/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 link1.c
 link2.c
 ^EXIT=0$

regression/linking-goto-binaries/array_size/main.c

@@ -0,0 +1,9 @@
+#include "supp.h"
+#include <assert.h>
+
+int main()
+{
+  int entry = A[1];
+  assert(entry == 42);
+  return 0;
+}

regression/linking-goto-binaries/array_size/supp.c

@@ -0,0 +1,3 @@
+#include "supp.h"
+
+int A[2] = {0, 42};

regression/linking-goto-binaries/array_size/supp.h

@@ -0,0 +1,6 @@
+#ifndef SUPP_H
+#define SUPP_H
+
+extern int A[];
+
+#endif // SUPP_H

regression/linking-goto-binaries/array_size/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+supp.c
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion entry == 42: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/linking-goto-binaries/chain.sh

@@ -5,21 +5,20 @@ set -e
 goto_cc=$1
 cbmc=$2
 is_windows=$3
-entry_point='generated_entry_function'
 
 main=${*:$#}
 main=${main%.c}
 args=${*:4:$#-4}
 next=${args%.c}
 
 if [[ "${is_windows}" == "true" ]]; then
-  $goto_cc "${main}.c"
-  $goto_cc "${next}.c"
-  mv "${main}.exe" "${main}.gb"
-  mv "${next}.exe" "${next}.gb"
+  $goto_cc /c "${main}.c" "/Fo${main}.gb"
+  $goto_cc /c "${next}.c" "/Fo${next}.gb"
+  $goto_cc "${main}.gb" "${next}.gb" "/Fefinal.gb"
 else
-  $goto_cc -o "${main}.gb" "${main}.c"
-  $goto_cc -o "${next}.gb" "${next}.c"
+  $goto_cc -c -o "${main}.gb" "${main}.c"
+  $goto_cc -c -o "${next}.gb" "${next}.c"
+  $goto_cc "${main}.gb" "${next}.gb" -o "final.gb"
 fi
 
-$cbmc "${main}.gb" "${next}.gb"
+$cbmc "final.gb"

src/linking/linking.cpp

@@ -36,8 +36,13 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
 
   const exprt &e = it->second;
 
-  typet type = s.type();
-  static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
+  if(e.type().id() != ID_array)
+  {
+    typet type = s.type();
+    static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
+  }
+  else
+    static_cast<exprt &>(s) = e;
 
   return false;
 }