tests: drop number of iterations
When checking for success or failure of a test, the number of iterations in the actual test should be irrelevant. As MiniSAT and PicoSAT seem to disagree on this number, do not check for it, so that the testis pass again.
This commit is contained in:
parent
12a69173e5
commit
751208d28e
|
@ -5,6 +5,6 @@ main.c
|
|||
^SIGNAL=0$
|
||||
^\[main\.assertion\.1\] assertion i==1: FAILURE$
|
||||
^\[main\.assertion\.2\] assertion i==2: SUCCESS$
|
||||
^\*\* 1 of 2 failed \(2 iterations\)$
|
||||
^\*\* 1 of 2 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -10,6 +10,6 @@ main.c
|
|||
^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
|
||||
^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
|
||||
^\*\* .* of .* covered \(100.0%\)$
|
||||
^\*\* Used 10 iterations$
|
||||
^\*\* Used
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -10,6 +10,6 @@ main.c
|
|||
^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$
|
||||
^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$
|
||||
^\*\* .* of .* covered \(100.0%\)$
|
||||
^\*\* Used 6 iterations$
|
||||
^\*\* Used
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -13,6 +13,6 @@ main.c
|
|||
^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && F != FALSE.*: SATISFIED$
|
||||
^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && !\(F != FALSE\).*: SATISFIED$
|
||||
^\*\* .* of .* covered \(100.0%\)$
|
||||
^\*\* Used 10 iterations$
|
||||
^\*\* Used
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -6,6 +6,6 @@ main.c
|
|||
^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
|
||||
^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
|
||||
^\*\* .* of .* covered \(100.0%\)$
|
||||
^\*\* Used 2 iterations$
|
||||
^\*\* Used
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -7,6 +7,6 @@ main.c
|
|||
^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && !\(x > \(unsigned int\)3\).*: SATISFIED$
|
||||
^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && x > \(unsigned int\)3.*: SATISFIED$
|
||||
^\*\* .* of .* covered \(100.0%\)$
|
||||
^\*\* Used 4 iterations$
|
||||
^\*\* Used
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -9,6 +9,6 @@ main.c
|
|||
^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
|
||||
^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
|
||||
^\*\* .* of .* covered \(100.0%\)$
|
||||
^\*\* Used 9 iterations$
|
||||
^\*\* Used
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -6,6 +6,6 @@ main.c
|
|||
^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* false: SATISFIED$
|
||||
^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* true: SATISFIED$
|
||||
^\*\* .* of .* covered \(100.0%\)$
|
||||
^\*\* Used 2 iterations$
|
||||
^\*\* Used
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -8,6 +8,6 @@ main.c
|
|||
^\[main.coverage.3\] file main.c line 8 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
|
||||
^\[main.coverage.4\] file main.c line 8 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
|
||||
^\*\* .* of .* covered \(100.0%\)$
|
||||
^\*\* Used 2 iterations$
|
||||
^\*\* Used
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -8,6 +8,6 @@ main.c
|
|||
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$
|
||||
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$
|
||||
^\*\* .* of .* covered \(100.0%\)$
|
||||
^\*\* Used 6 iterations$
|
||||
^\*\* Used
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -9,6 +9,6 @@ main.c
|
|||
^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE && !\(D != FALSE\).* SATISFIED$
|
||||
^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$
|
||||
^\*\* .* of .* covered \(100.0%\)$
|
||||
^\*\* Used 8 iterations$
|
||||
^\*\* Used
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -4,7 +4,7 @@ test.class
|
|||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^.*assertion at file test.java line 26 function.*: FAILURE$
|
||||
\*\* 1 of [0-9]* failed \(2 iterations\)$
|
||||
\*\* 1 of [0-9]* failed
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -4,7 +4,7 @@ test.class
|
|||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^.*assertion at file test.java line 15 function.*: FAILURE$
|
||||
^\*\* 1 of [0-9]* failed \(2 iterations\)$
|
||||
^\*\* 1 of [0-9]* failed
|
||||
^VERIFICATION FAILED$
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -5,6 +5,6 @@ main.c
|
|||
^SIGNAL=0$
|
||||
^\[main\.assertion\.1\] assertion matriz\[\(signed long int\)j\]\[\(signed long int\)k\] <= maior: OK$
|
||||
^\[main\.assertion\.2\] assertion matriz\[\(signed long int\)0\]\[\(signed long int\)0\] < maior: FAILED$
|
||||
^\*\* 1 of 2 failed \(2 iterations\)$
|
||||
^\*\* 1 of 2 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -4,6 +4,6 @@ main.c
|
|||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main\.assertion\.2\] .*: FAILED$
|
||||
^\*\* 1 of 2 failed \(2 iterations\)$
|
||||
^\*\* 1 of 2 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -4,6 +4,6 @@ main.c
|
|||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILED$
|
||||
^\*\* 1 of 9 failed \(2 iterations\)$
|
||||
^\*\* 1 of 9 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -4,6 +4,6 @@ main.c
|
|||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
|
||||
^\*\* 1 of 9 failed \(2 iterations\)$
|
||||
^\*\* 1 of 9 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -4,6 +4,6 @@ main.c
|
|||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main\.assertion\.4\] assertion data\[1\]==31: FAILED$
|
||||
^\*\* 1 of 5 failed \(2 iterations\)$
|
||||
^\*\* 1 of 5 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -7,6 +7,6 @@ pointer outside dynamic object bounds in \*p: FAILURE
|
|||
pointer outside dynamic object bounds in \*p: FAILURE
|
||||
pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
|
||||
pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
|
||||
\*\* 4 of 36 failed \(3 iterations\)
|
||||
\*\* 4 of 36 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -5,6 +5,6 @@ main.c
|
|||
^SIGNAL=0$
|
||||
^\[main\.assertion\.1\] : SUCCESS$
|
||||
^\[main\.assertion\.2\] : FAILURE$
|
||||
^\*\* 1 of 2 failed \(2 iterations\)$
|
||||
^\*\* 1 of 2 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -4,6 +4,6 @@ main.c
|
|||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main\.assertion\.2\] .*: FAILURE$
|
||||
^\*\* 1 of 2 failed \(2 iterations\)$
|
||||
^\*\* 1 of 2 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -4,6 +4,6 @@ main.c
|
|||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
array\.List dynamic object upper bound in p->List\[2\]: FAILURE
|
||||
\*\* 1 of 11 failed \(2 iterations\)
|
||||
\*\* 1 of 11 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -4,6 +4,6 @@ main.c
|
|||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
|
||||
^\*\* 1 of 9 failed \(2 iterations\)$
|
||||
^\*\* 1 of 9 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -8,5 +8,5 @@ main.c
|
|||
^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
|
||||
^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
|
||||
^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
|
||||
^\*\* 2 of 6 failed \(2 iterations\)$
|
||||
^\*\* 2 of 6 failed
|
||||
^VERIFICATION FAILED$
|
||||
|
|
|
@ -6,5 +6,5 @@ main.c
|
|||
^\[main.assertion.2\] assertion y: FAILURE$
|
||||
^\[main.assertion.3\] assertion z1: SUCCESS$
|
||||
^\[main.assertion.4\] assertion z2: SUCCESS$
|
||||
^\*\* 1 of 4 failed \(2 iterations\)$
|
||||
^\*\* 1 of 4 failed
|
||||
^VERIFICATION FAILED$
|
||||
|
|
|
@ -7,5 +7,5 @@ main.c
|
|||
^\[main.assertion.3\] success 1: SUCCESS$
|
||||
^\[main.assertion.4\] failure 3: FAILURE$
|
||||
^\[main.assertion.5\] success 2: SUCCESS$
|
||||
^\*\* 3 of 5 failed \(2 iterations\)$
|
||||
^\*\* 3 of 5 failed
|
||||
^VERIFICATION FAILED$
|
||||
|
|
|
@ -7,5 +7,5 @@ main.c
|
|||
^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$
|
||||
^\[main.assertion.4\] forall c\[\]: SUCCESS$
|
||||
^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
|
||||
^\*\* 1 of 5 failed \(2 iterations\)$
|
||||
^\*\* 1 of 5 failed
|
||||
^VERIFICATION FAILED$
|
||||
|
|
|
@ -7,5 +7,5 @@ main.c
|
|||
^\[main.assertion.3\] failure 1: FAILURE$
|
||||
^\[main.assertion.4\] success 3: SUCCESS$
|
||||
^\[main.assertion.5\] failure 2: FAILURE$
|
||||
^\*\* 2 of 5 failed \(2 iterations\)$
|
||||
^\*\* 2 of 5 failed
|
||||
^VERIFICATION FAILED$
|
||||
|
|
|
@ -4,5 +4,5 @@ main.c
|
|||
^\*\* Results:$
|
||||
^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
|
||||
^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
|
||||
^\*\* 1 of 2 failed \(2 iterations\)$
|
||||
^\*\* 1 of 2 failed
|
||||
^VERIFICATION FAILED$
|
||||
|
|
|
@ -5,6 +5,6 @@ main.c
|
|||
^SIGNAL=0$
|
||||
^VERIFICATION FAILED$
|
||||
\[main.assertion.3\] assertion p\[1\]=='b': FAILURE
|
||||
\*\* 1 of \d+ failed \(2 iterations\)
|
||||
\*\* 1 of \d+ failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -7,6 +7,6 @@ main.c
|
|||
\[main.assertion.1\] assertion \*p==42: SUCCESS
|
||||
\[main.pointer_dereference.14\] dereference failure: pointer invalid in p\[.*1\]: FAILURE
|
||||
\[main.assertion.2\] assertion \*\(p\+1\)==42: SUCCESS
|
||||
\*\* 12 of 26 failed \(2 iterations\)
|
||||
\*\* 12 of 26 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -5,6 +5,6 @@ main.c
|
|||
^SIGNAL=0$
|
||||
^VERIFICATION FAILED$
|
||||
\[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE
|
||||
\*\* 1 of 12 failed \(2 iterations\)
|
||||
\*\* 1 of 12 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -4,6 +4,6 @@ main.c
|
|||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main\.assertion\.4\] assertion data\[1\]==31: FAILURE$
|
||||
^\*\* 1 of 5 failed \(2 iterations\)$
|
||||
^\*\* 1 of 5 failed
|
||||
--
|
||||
^warning: ignoring
|
||||
|
|
|
@ -2,7 +2,7 @@ CORE
|
|||
main.c
|
||||
--function fun --cover branch
|
||||
^\*\* 7 of 7 covered \(100.0%\)$
|
||||
^\*\* Used 4 iterations$
|
||||
^\*\* Used
|
||||
^Test suite:$
|
||||
^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$
|
||||
^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
|
||||
|
|
|
@ -2,7 +2,7 @@ CORE
|
|||
main.c
|
||||
--function fun --cover branch
|
||||
^\*\* 5 of 5 covered \(100\.0%\)$
|
||||
^\*\* Used 3 iterations$
|
||||
^\*\* Used
|
||||
^Test suite:$
|
||||
^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
|
||||
^a=&tmp\$\d+!0, tmp\$\d+=4$
|
||||
|
|
|
@ -5,4 +5,4 @@ test.c
|
|||
^SIGNAL=0$
|
||||
^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): SUCCESS
|
||||
^\[main.assertion.2\] assertion !__CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): FAILURE$
|
||||
^\*\* 1 of 2 failed \(2 iterations\)$
|
||||
^\*\* 1 of 2 failed
|
||||
|
|
Loading…
Reference in New Issue