Skip to content

Commit 01f345e

Browse files
authored
Merge pull request #6188 from tautschnig/array-linking
Linking forward declarations of arrays must not yield type casts
2 parents 71da49a + 914f3d6 commit 01f345e

File tree

7 files changed

+42
-11
lines changed

7 files changed

+42
-11
lines changed

regression/cbmc/Linking4/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
link1.c
33
link2.c
44
^EXIT=0$
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#include "supp.h"
2+
#include <assert.h>
3+
4+
int main()
5+
{
6+
int entry = A[1];
7+
assert(entry == 42);
8+
return 0;
9+
}
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
#include "supp.h"
2+
3+
int A[2] = {0, 42};
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
#ifndef SUPP_H
2+
#define SUPP_H
3+
4+
extern int A[];
5+
6+
#endif // SUPP_H
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
supp.c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion entry == 42: SUCCESS
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
^warning: ignoring

regression/linking-goto-binaries/chain.sh

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,21 +5,20 @@ set -e
55
goto_cc=$1
66
cbmc=$2
77
is_windows=$3
8-
entry_point='generated_entry_function'
98

109
main=${*:$#}
1110
main=${main%.c}
1211
args=${*:4:$#-4}
1312
next=${args%.c}
1413

1514
if [[ "${is_windows}" == "true" ]]; then
16-
$goto_cc "${main}.c"
17-
$goto_cc "${next}.c"
18-
mv "${main}.exe" "${main}.gb"
19-
mv "${next}.exe" "${next}.gb"
15+
$goto_cc /c "${main}.c" "/Fo${main}.gb"
16+
$goto_cc /c "${next}.c" "/Fo${next}.gb"
17+
$goto_cc "${main}.gb" "${next}.gb" "/Fefinal.gb"
2018
else
21-
$goto_cc -o "${main}.gb" "${main}.c"
22-
$goto_cc -o "${next}.gb" "${next}.c"
19+
$goto_cc -c -o "${main}.gb" "${main}.c"
20+
$goto_cc -c -o "${next}.gb" "${next}.c"
21+
$goto_cc "${main}.gb" "${next}.gb" -o "final.gb"
2322
fi
2423

25-
$cbmc "${main}.gb" "${next}.gb"
24+
$cbmc "final.gb"

src/linking/linking.cpp

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,8 +36,13 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
3636

3737
const exprt &e = it->second;
3838

39-
typet type = s.type();
40-
static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
39+
if(e.type().id() != ID_array)
40+
{
41+
typet type = s.type();
42+
static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
43+
}
44+
else
45+
static_cast<exprt &>(s) = e;
4146

4247
return false;
4348
}

0 commit comments

Comments
 (0)