replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

More permissive regression tests regarding tmp var suffixes

This commit is contained in:
Peter Schrammel 2018-04-16 19:29:48 +01:00
parent 47951ca606
commit ca678aa2d0
5 changed files with 15 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
regression/cbmc/Quantifiers-not-exists/test.desc
View File

@ -3,11 +3,11 @@ main.c
^\*\* Results:$
^\[main.assertion.1\] assertion a\[.*\]\[.*\] > 10: SUCCESS$
^\[main.assertion.2\] assertion tmp_if_expr\$3: SUCCESS$
^\[main.assertion.3\] assertion tmp_if_expr\$6: SUCCESS$
^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$
^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.3\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.4\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.6\] assertion tmp_if_expr\$\d+: SUCCESS$
^\*\* 0 of 6 failed
^VERIFICATION SUCCESSFUL$
^EXIT=0$

2
regression/cbmc/Quantifiers-two-dimension-array/test.desc
View File

@ -6,7 +6,7 @@ main.c
^\[main.assertion.2\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$
^\*\* 0 of 5 failed
^VERIFICATION SUCCESSFUL$
^EXIT=0$

4
regression/cbmc/Quantifiers-type/test.desc
View File

@ -2,8 +2,8 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
^\[main.assertion.1\] assertion tmp_if_expr(\$\d+)?: FAILURE$
^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$
^\*\* 1 of 2 failed
^VERIFICATION FAILED$
^EXIT=10$

8
regression/cbmc/pointer-function-parameters-2/test.desc
View File

@ -3,10 +3,10 @@ main.c
--function fun --cover branch
^\*\* 7 of 7 covered \(100.0%\)$
^Test suite:$
^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$
^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$
^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=4$
^a=\(\(signed int \*\*\)NULL\), tmp(\$\d+)?=[^,]*, tmp(\$\d+)?=[^,]*$
^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$
^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp\$\d+!0, tmp(\$\d+)?=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$
^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$
^EXIT=0$
^SIGNAL=0$
--

6
regression/cbmc/pointer-function-parameters/test.desc
View File

@ -3,9 +3,9 @@ main.c
--function fun --cover branch
^\*\* 5 of 5 covered \(100\.0%\)$
^Test suite:$
^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
^a=&tmp\$\d+!0, tmp\$\d+=4$
^a=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
^a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$
^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$
^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+)$
^EXIT=0$
^SIGNAL=0$
--