Enable default flags on for checks

regression/cbmc-shadow-memory/char1/test.desc

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

regression/cbmc-shadow-memory/constchar-pointers1/test.desc

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

regression/cbmc-shadow-memory/errno1/test.desc

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

regression/cbmc-shadow-memory/linked-list1/test.desc

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

regression/cbmc-shadow-memory/maybe-null1/test.desc

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

regression/cbmc-shadow-memory/pointer-checks1/test.desc

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

regression/cbmc-shadow-memory/pointer-checks2/test.desc

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

regression/cbmc-shadow-memory/static1/test.desc

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

regression/cbmc-shadow-memory/strdup1/main.c

@@ -8,6 +8,9 @@ int main()
   __CPROVER_field_decl_global("field1", (unsigned __CPROVER_bitvector[2])0);
 
   char *s = (char *)malloc(3 * sizeof(char));
+  // Terminate string so that `strdup` will not call `strlen`
+  // on a string without a null-terminator.
+  s[2] = '\0';
   assert(__CPROVER_get_field(&s[0], "field1") == 0);
   assert(__CPROVER_get_field(&s[1], "field1") == 0);
 

regression/cbmc-shadow-memory/strdup1/test.desc

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

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-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$

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$

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/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$

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$