property results are now uniform

Author: Daniel Kroening

doc/html-manual/cbmc.shtml

@@ -97,7 +97,7 @@ thus print a line as follows:
 </p>
 
 <code>
-[main.pointer_dereference.6] dereference failure: object bounds in argv[(signed long int)2]: FAILED
+[main.pointer_dereference.6] dereference failure: object bounds in argv[(signed long int)2]: FAILURE
 </code>
 
 <h3>Counterexample Traces</h3>
@@ -119,8 +119,8 @@ our example, the program trace ends in the faulty array access.  It also
 shows the values the input variables must have for the bug to occur.  In
 this example, <code>argc</code> must be one to trigger the out-of-bounds
 array access.  If you add a branch to the example that requires that
-<code>argc&gt;=3</code>, the bug is fixed and CBMC will report that all
-properties are OK.</p>
+<code>argc&gt;=3</code>, the bug is fixed and CBMC will report that the
+proofs of all properties have been successful.</p>
 
 <h3>Verifying Modules</h3>
 

regression/cbmc-concurrency/pthread_join1/test.desc

@@ -3,8 +3,8 @@ main.c
 --all-properties
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.1\] assertion i==1: FAILED$
-^\[main\.assertion\.2\] assertion i==2: OK$
+^\[main\.assertion\.1\] assertion i==1: FAILURE$
+^\[main\.assertion\.2\] assertion i==2: SUCCESS$
 ^\*\* 1 of 2 failed (2 iterations)$
 --
 ^warning: ignoring

regression/cbmc-java/NullPointer1/test.desc

@@ -1,6 +1,6 @@
 CORE
 NullPointer1.class
---pointer-check
+--pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^  file NullPointer1.java line 16$

regression/cbmc-java/NullPointer2/test.desc

@@ -1,6 +1,6 @@
 CORE
 NullPointer2.class
---pointer-check
+--pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^  file NullPointer2.java line 9$

regression/cbmc-java/NullPointer3/test.desc

@@ -1,6 +1,6 @@
 CORE
 NullPointer3.class
---pointer-check
+--pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^  file NullPointer3.java line 5$

regression/cbmc-java/NullPointer4/test.desc

@@ -1,6 +1,6 @@
 CORE
 NullPointer4.class
---pointer-check
+--pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^  file NullPointer4.java line 6$

regression/cbmc/Function5/test.desc

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

regression/cbmc/Multi_Dimensional_Array6/test.desc

@@ -3,8 +3,8 @@ main.c
 --unwind 3 --no-unwinding-assertions --all-properties
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.1\] : OK$
-^\[main\.assertion\.2\] : FAILED$
+^\[main\.assertion\.1\] : SUCCESS$
+^\[main\.assertion\.2\] : FAILURE$
 ^\*\* 1 of 2 failed (2 iterations)$
 --
 ^warning: ignoring

regression/cbmc/Overflow_Addition1/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 --signed-overflow-check
 ^SIGNAL=0$
-^\[.*\] arithmetic overflow on signed + in .*: FAILED$
+^\[.*\] arithmetic overflow on signed + in .*: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/Pointer_byte_extract2/test.desc

@@ -3,7 +3,7 @@ main.c
 --all-properties --little-endian
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.2\] .*: FAILED$
+^\[main\.assertion\.2\] .*: FAILURE$
 ^\*\* 1 of 2 failed (2 iterations)$
 --
 ^warning: ignoring

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -3,7 +3,7 @@ main.c
 --all-properties --bounds-check --32
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILED$
+^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILURE$
 ^\*\* 1 of 9 failed (2 iterations)$
 --
 ^warning: ignoring

regression/cbmc/goto4/test.desc

@@ -3,7 +3,7 @@ main.c
 --unwind 1 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*] assertion g == 0: OK$
-^\[.*] unwinding assertion loop 0: FAILED$
+^\[.*] assertion g == 0: SUCCESS$
+^\[.*] unwinding assertion loop 0: FAILURE$
 --
 ^warning: ignoring

regression/cbmc/pipe1/test.desc

@@ -3,7 +3,7 @@ main.c
 --all-properties
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.4\] assertion data\[1\]==31: FAILED$
+^\[main\.assertion\.4\] assertion data\[1\]==31: FAILURE$
 ^\*\* 1 of 5 failed (2 iterations)$
 --
 ^warning: ignoring

src/cbmc/all_properties.cpp

@@ -247,7 +247,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
     else
     {
       status() << "[" << it->first << "] "
-               << it->second.description << ": " << (it->second.failed?"FAILED":"OK")
+               << it->second.description << ": " << (it->second.failed?"FAILURE":"SUCCESS")
                << eom;
     }
   }