Skip to content

Commit fbf9498

Browse files
committed
cbmc-cover/pointer-function-parameters test: negative numbers are ok
We need to cover three scenarios: `a` is `NULL`, or `*a` is 4, or `*a` is some integer other than 4. The latter includes negative values. Seen in https://github.com/diffblue/cbmc/actions/runs/7740169274/job/21104572343?pr=8141.
1 parent 57ca4bf commit fbf9498

File tree

1 file changed

+1
-1
lines changed
  • regression/cbmc-cover/pointer-function-parameters

1 file changed

+1
-1
lines changed

regression/cbmc-cover/pointer-function-parameters/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^Test suite:$
66
^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$
77
^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0@1)$
8-
^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0@1)$
8+
^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=([012356789]\d*|4\d+|-\d+))|(tmp(\$\d+)?=([012356789]\d*|4\d+|-\d+), a=&tmp(\$\d+)?!0@1)$
99
^EXIT=0$
1010
^SIGNAL=0$
1111
--

0 commit comments

Comments
 (0)