More tests adjusted

Author: NlightNFotis

Diff for: regression/cbmc/Float-div2/test.desc

@@ -1,6 +1,6 @@
 CORE broken-z3-smt-backend no-new-smt
 main.c
---floatbv
+--floatbv --no-built-in-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/Float-div3/test.desc

@@ -1,6 +1,6 @@
 CORE broken-z3-smt-backend no-new-smt
 main.c
---floatbv
+--floatbv --no-built-in-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/Float-flags-simp1/test.desc

@@ -1,6 +1,6 @@
 CORE broken-cprover-smt-backend no-new-smt
 main.c
---floatbv
+--floatbv --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/Malloc11/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/Pointer29/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/Pointer_byte_extract2/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.2\] .*: FAILURE$
-^\*\* 1 of 2 failed 
+^\*\* 2 of 4 failed
 --
 ^warning: ignoring

Diff for: regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -4,7 +4,7 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 11 failed
+\*\* 1 of \d+ failed
 --
 ^warning: ignoring
 --

Diff for: regression/cbmc/Pointer_comparison3/test.desc

@@ -3,7 +3,7 @@ main.c
 
 ^\[main.assertion.3\] line 21 always false for different objects: FAILURE$
 ^\[main.assertion.4\] line 23 always false for different objects: FAILURE$
-^\*\* 2 of 7 failed
+^\*\* 11 of 59 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

Diff for: regression/cbmc/Pointer_difference1/no-simplify.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-simplify
+--no-simplify --no-standard-checks
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/cbmc/Pointer_difference1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 --

Diff for: regression/cbmc/Pointer_difference2/test.desc

@@ -9,7 +9,7 @@ main.c
 ^\[main.pointer_arithmetic.\d+\] line 26 pointer relation: pointer outside object bounds in p: FAILURE$
 ^\[main.assertion.8\] line 28 end plus 2 is nondet: FAILURE$
 ^\[main.pointer_arithmetic.\d+\] line 28 pointer relation: pointer outside object bounds in p: FAILURE$
-^\*\* 7 of \d+ failed
+^\*\* 9 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

Diff for: regression/cbmc/Quantifiers-assertion/test.desc

@@ -8,7 +8,7 @@ main.c
 ^\[main.assertion.4\] .* NotExists-Forall: failed: FAILURE$
 ^\[main.assertion.5\] .* NotForall-Forall: successful: SUCCESS$
 ^\[main.assertion.6\] .* NotForall-NotForall: successful: SUCCESS$
-^\*\* 3 of 6 failed
+^\*\* 3 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

Diff for: regression/cbmc/Quantifiers-assignment/test.desc

@@ -6,7 +6,7 @@ main.c
 ^\[main.assertion.2\] .* assertion y: FAILURE$
 ^\[main.assertion.3\] .* assertion z1: SUCCESS$
 ^\[main.assertion.4\] .* assertion z2: SUCCESS$
-^\*\* 1 of 4 failed
+^\*\* 1 of 20 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

Diff for: regression/cbmc/Quantifiers-copy/test.desc

@@ -7,7 +7,7 @@ main.c
 ^\[main.assertion.3\] .* assertion b\[.*\] == 2: SUCCESS$
 ^\[main.assertion.4\] .* assertion b\[.*\] == 3: SUCCESS$
 ^\[main.assertion.5\] .* assertion b\[.*\] == 4: SUCCESS$
-^\*\* 0 of 5 failed
+^\*\* 0 of 9 failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/cbmc/Quantifiers-if/test.desc

@@ -7,7 +7,7 @@ main.c
 ^\[main.assertion.3\] .* success 1: SUCCESS$
 ^\[main.assertion.4\] .* failure 3: FAILURE$
 ^\[main.assertion.5\] .* success 2: SUCCESS$
-^\*\* 3 of 5 failed
+^\*\* 3 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

Diff for: regression/cbmc/Quantifiers-initialisation/test.desc

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

Diff for: regression/cbmc/Quantifiers-initialisation2/test.desc

@@ -7,7 +7,7 @@ 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
+^\*\* 1 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

Diff for: regression/cbmc/Quantifiers-not-exists/fixed.desc

@@ -8,7 +8,7 @@ fixed.c
 ^\[main.assertion.8\] line 36 assertion .*: SUCCESS$
 ^\[main.assertion.9\] line 38 assertion .*: SUCCESS$
 ^\[main.assertion.10\] line 39 assertion .*: SUCCESS$
-^\*\* 4 of 10 failed
+^\*\* 4 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

Diff for: regression/cbmc/Quantifiers-not/test.desc

@@ -7,7 +7,7 @@ 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 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

Diff for: regression/cbmc/Quantifiers-two-dimension-array/fixed.desc

@@ -7,7 +7,7 @@ fixed.c
 ^\[main.assertion.3\] line 16 assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.4\] line 17 assertion a\[.*\]\[.*\] == 2: SUCCESS$
 ^\[main.assertion.5\] line 18 assertion .*: SUCCESS$
-^\*\* 0 of 5 failed
+^\*\* 0 of \d+ failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/cbmc/Quantifiers-two-dimension-array/test.desc

@@ -7,7 +7,7 @@ main.c
 ^\[main.assertion.3\] line 14 assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.4\] line 15 assertion a\[.*\]\[.*\] == 2: SUCCESS$
 ^\[main.assertion.5\] line 16 assertion .*: FAILURE$
-^\*\* 1 of 5 failed
+^\*\* 1 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

Diff for: regression/cbmc/String_Abstraction11/test.desc

@@ -1,6 +1,6 @@
 CORE
 anon-retval.c
---string-abstraction
+--string-abstraction --no-pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/String_Abstraction15/test.desc

@@ -1,6 +1,6 @@
 CORE
 pass-in.c
---string-abstraction
+--string-abstraction --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/String_Abstraction19/test.desc

@@ -1,6 +1,6 @@
 CORE
 structs.c
---string-abstraction
+--string-abstraction --no-pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/Unbounded_Array5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/Undefined_Shift1/test.desc

@@ -9,7 +9,7 @@ main.c
 ^\[.*\] line 15 shift distance is negative in .*: FAILURE$
 ^\[.*\] line 15 shift distance too large in .*: SUCCESS$
 ^\[.*\] line 20 shift operand is negative in .*: FAILURE$
-^\*\* 3 of 6 failed
+^\*\* 4 of 9 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

Diff for: regression/cbmc/__builtin_clz-01/big-endian.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---bounds-check --big-endian
+--big-endian
 ^\[main.bit_count.\d+\] line 61 count leading zeros is undefined for value zero in __builtin_clz\(0u\): FAILURE$
 ^\*\* 1 of \d+ failed
 ^VERIFICATION FAILED$

Diff for: regression/cbmc/__builtin_clz-01/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---bounds-check
+
 ^\[main.bit_count.\d+\] line 61 count leading zeros is undefined for value zero in __builtin_clz\(0u\): FAILURE$
 ^\*\* 1 of \d+ failed
 ^VERIFICATION FAILED$

Diff for: regression/cbmc/__builtin_ctz-01/big-endian.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---bounds-check --big-endian
+--big-endian
 ^\[main.bit_count.\d+\] line 46 count trailing zeros is undefined for value zero in __builtin_ctz\(0u\): FAILURE$
 ^\[main.assertion.2\] line 47 count trailing zeros of 0 is bit width: SUCCESS$
 ^\*\* 1 of \d+ failed

Diff for: regression/cbmc/__builtin_ctz-01/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---bounds-check
+
 ^\[main.bit_count.\d+\] line 46 count trailing zeros is undefined for value zero in __builtin_ctz\(0u\): FAILURE$
 ^\[main.assertion.2\] line 47 count trailing zeros of 0 is bit width: SUCCESS$
 ^\*\* 1 of \d+ failed

Diff for: regression/cbmc/__builtin_ffs-01/big-endian.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---pointer-check --bounds-check --big-endian
+--big-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/__builtin_ffs-01/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/address_space_size_limit3/test.desc

@@ -1,6 +1,6 @@
 CORE thorough-smt-backend no-new-smt
 main.i
---32 --little-endian --object-bits 26 --pointer-check
+--32 --little-endian --object-bits 26
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

Diff for: regression/cbmc/argc-and-argv/argc1.desc

@@ -1,6 +1,6 @@
 CORE
 argc1.c
---bounds-check --pointer-check --unwind 0
+--unwind 0
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*\] line .* dereference failure: pointer outside object bounds in argv\[.*n\]: FAILURE$

Diff for: regression/cbmc/argc-and-argv/argv1.desc

@@ -1,6 +1,6 @@
 CORE
 argv1.c
---bounds-check --pointer-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/array-bug-6230/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---malloc-may-fail --malloc-fail-null --pointer-check
+--malloc-may-fail --malloc-fail-null
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

Diff for: regression/cbmc/array-cell-sensitivity1/test_execution.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-bounds-check
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/cbmc/array-cell-sensitivity2/test_execution.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-bounds-check
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/cbmc/array-cell-sensitivity4/test_execution.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-bounds-check
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/cbmc/array-cell-sensitivity5/test_execution.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/cbmc/array-cell-sensitivity6/test_execution.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

Diff for: regression/cbmc/array-cell-sensitivity9/test_execution.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-bounds-check
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

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

@@ -1,6 +1,6 @@
 CORE no-new-smt
 test.c
---function test --min-null-tree-depth 2 --max-nondet-tree-depth 2 --bounds-check
+--function test --min-null-tree-depth 2 --max-nondet-tree-depth 2
 ^EXIT=10$
 ^SIGNAL=0$
 \[test.assertion.1\] line \d+ assertion Test.lists\[0\]->next: SUCCESS

Diff for: regression/cbmc/array_constraints1/test.desc

@@ -1,9 +1,9 @@
 CORE no-new-smt
 main.c
---unwind 2 --pointer-check
+--unwind 2
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 2 of 14
+^\*\* 4 of \d+
 --
 ^warning: ignoring

Diff for: regression/cbmc/atomic_X_fetch-1/test.desc

@@ -1,6 +1,6 @@
 CORE gcc-only
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

Diff for: regression/cbmc/atomic_fetch_X-1/test.desc

@@ -1,6 +1,6 @@
 CORE gcc-only no-new-smt
 main.c
-
+--no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

Diff for: regression/cbmc/aws-byte-buf-regression/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---pointer-check
+
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$