From 5fa37a3eacfd2e89b096d8e68098449d90567d18 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 14 Dec 2023 15:22:08 +0000 Subject: [PATCH] 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. --- scripts/csmith.sh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/csmith.sh b/scripts/csmith.sh index 8f778acdc0c..5d610477bee 100755 --- a/scripts/csmith.sh +++ b/scripts/csmith.sh @@ -60,6 +60,9 @@ csmith_test() { # Prepare the test CBMC by injecting the checksum as an assertion. gcc -E -I/usr/include/csmith -D__FRAMAC \ -D'Frama_C_dump_assert_each()'="assert($check==(crc))" $f -o $bn.i + # We don't model argv here, so make sure we don't end up with a spurious + # null-pointer use. + sed -i 's/strcmp(argv\[1\], "1")/0/' $bn.i # Run the test using CBMC for up to 90 seconds, unwinding loops up to 257 # times. ec=0