Skip to content

Commit 2e0fcc8

Browse files
authored
Merge pull request diffblue#8105 from tautschnig/bugfixes/csmith-bugfix
CSmith test script: avoid a need for argv modelling
2 parents 41af31c + 5fa37a3 commit 2e0fcc8

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

scripts/csmith.sh

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,9 @@ csmith_test() {
6060
# Prepare the test CBMC by injecting the checksum as an assertion.
6161
gcc -E -I/usr/include/csmith -D__FRAMAC \
6262
-D'Frama_C_dump_assert_each()'="assert($check==(crc))" $f -o $bn.i
63+
# We don't model argv here, so make sure we don't end up with a spurious
64+
# null-pointer use.
65+
sed -i 's/strcmp(argv\[1\], "1")/0/' $bn.i
6366
# Run the test using CBMC for up to 90 seconds, unwinding loops up to 257
6467
# times.
6568
ec=0

0 commit comments

Comments
 (0)