Skip to content

Commit 99ac9b0

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 608b7ea commit 99ac9b0

File tree

1 file changed

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

1 file changed

+1
-1
lines changed

Diff for: regression/cbmc-cover/pointer-function-parameters/test.desc

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