Skip to content

Commit 5fa37a3

Browse files
committed
CSmith test script: avoid a need for argv modelling
With additional checks turned on as of #8093, we failed CSmith tests with (legitimate) pointer property failures in `strcmp`. These are caused by trying to compare `argv[1]` to a string. As we do not model `argv` in these tests, `argv[1]` was not a valid pointer. This fix just removes the string comparison, which is only used for turning on/off debug output in test execution.
1 parent 41af31c commit 5fa37a3

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

scripts/csmith.sh

+3
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)