Adjust default flags in regression/cbmc tests.

Author: NlightNFotis

regression/cbmc/ACSL/operators.desc

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

regression/cbmc/Address_of1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---stop-on-fail
+--stop-on-fail --no-pointer-check
 ^\[main\.assertion
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Anonymous_Struct1/test.desc

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

regression/cbmc/Array_UF21/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---arrays-uf-always --bounds-check
+--arrays-uf-always
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Array_operations1/full-slice.desc

@@ -10,9 +10,9 @@ main.c
 ^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE
-^\*\* 5 of 15 failed
+^\*\* 5 of 19 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
 --
-Verify the properties of various cprover array primitves
+Verify the properties of various CPROVER array primitives.

regression/cbmc/Array_operations1/test.desc

@@ -10,7 +10,7 @@ main.c
 ^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE
-^\*\* 5 of 15 failed
+^\*\* 5 of 19 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/Associativity1/test.desc

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

regression/cbmc/BV_Arithmetic3/test.desc

@@ -3,7 +3,7 @@ main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-(Starting CEGAR Loop|^Generated 1 VCC\(s\), 0 remaining after simplification$)
+(Starting CEGAR Loop|^Generated 68 VCC\(s\), 0 remaining after simplification$)
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc/BV_Arithmetic4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
- --unwind 32
+ --unwind 32 --no-signed-overflow-check --no-undefined-shift-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Bitfields3/paths.desc

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

regression/cbmc/Bitfields3/test.desc

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

regression/cbmc/Bool/bool5-full-slice.desc

@@ -1,7 +1,7 @@
 CORE
 bool5.c
 --full-slice
-Generated 4 VCC\(s\), 0 remaining after simplification
+Generated 10 VCC\(s\), 0 remaining after simplification
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Bool/bool5.desc

@@ -1,7 +1,7 @@
 CORE
 bool5.c
 
-Generated 4 VCC\(s\), 0 remaining after simplification
+Generated 10 VCC\(s\), 0 remaining after simplification
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Boolean_Guards1/test.desc

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

regression/cbmc/Endianness5/test.desc

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

regression/cbmc/Failed_Symbols1/test.desc

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

regression/cbmc/Float-flags-no-simp1/test.desc

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

regression/cbmc/Float13/test.desc

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

regression/cbmc/Free1/test.desc

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

regression/cbmc/Free3/test.desc

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

regression/cbmc/Free4/test.desc

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

regression/cbmc/Function1/test.desc

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

regression/cbmc/Function5/test.desc

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

regression/cbmc/Function_Pointer14/test.desc

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

regression/cbmc/Function_Pointer16/test.desc

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

regression/cbmc/Function_Pointer18/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 \[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS
-\[main.pointer_dereference.1\] line 28 dereferenced function pointer must be f2: FAILURE$
+\[main.pointer_dereference.\d*\] line 28 dereferenced function pointer must be f2: FAILURE$
 \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS
 \[main.assertion.2\] line [0-9]+ assertion x == 2: SUCCESS
 ^VERIFICATION FAILED$

regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---function foo --pointer-check
+--function foo
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: SUCCESS$
 ^\[foo.pointer_dereference.\d+\] line \d+ no candidates for dereferenced function pointer: FAILURE$
 ^EXIT=10$

regression/cbmc/Linking6/test.desc

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

regression/cbmc/Linking7/member-name-mismatch.desc

@@ -6,6 +6,6 @@ module2.c
 ^VERIFICATION FAILED$
 line 21 assertion \*g\.a == 42: SUCCESS
 line 22 assertion \*g\.c == 41: FAILURE
-^\*\* 1 of 3 failed
+^\*\* 1 of \d+ failed
 --
 ^warning: ignoring

regression/cbmc/Linking7/test.desc

@@ -4,7 +4,7 @@ module.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 1 of 3 failed
+^\*\* 1 of \d+ failed
 line 21 assertion \*g\.a == 42: SUCCESS
 line 22 assertion \*g\.b == 41: FAILURE
 --

regression/cbmc/Linking8/test.desc

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

regression/cbmc/Local_out_of_scope1/test.desc

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

regression/cbmc/Local_out_of_scope4/test.desc

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

regression/cbmc/Malloc1/test.desc

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

regression/cbmc/Malloc10/test.desc

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

regression/cbmc/Malloc11/slice-formula.desc

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

regression/cbmc/Malloc2/test.desc

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

regression/cbmc/Malloc23/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+
 ^EXIT=10$
 ^SIGNAL=0$
 pointer outside object bounds in \*p: FAILURE

regression/cbmc/Malloc24/test.desc

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

regression/cbmc/Malloc3/test.desc

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

regression/cbmc/Malloc4/test.desc

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

regression/cbmc/Malloc5/test.desc

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

regression/cbmc/Malloc6/test.desc

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

regression/cbmc/Malloc7/test.desc

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

regression/cbmc/Malloc8/test.desc

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

regression/cbmc/Malloc9/test.desc

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

regression/cbmc/Multi_Dimensional_Array6/test.desc

@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] .*: SUCCESS$
 ^\[main\.assertion\.2\] .*: FAILURE$
-^\*\* 1 of 2 failed 
+^\*\* 3 of 8 failed
 --
 ^warning: ignoring

regression/cbmc/Pointer1/test.desc

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