Include undetermined and unreachable in the verification summary (rus…

…t-lang#856)
celinval · Feb 23, 2022 · d536dc9 · d536dc9
1 parent c361394
commit d536dc9
Show file tree

Hide file tree

Showing 7 changed files with 24 additions and 2 deletions.
diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py
@@ -412,6 +412,8 @@ def construct_property_message(properties):
     """
 
     number_tests_failed = 0
+    number_tests_unreachable = 0
+    number_tests_undetermined = 0
     output_message = ""
     failed_tests = []
     index = 0
@@ -430,8 +432,12 @@ def construct_property_message(properties):
 
         if status == "SUCCESS":
             message = Fore.GREEN + f"{status}" + Style.RESET_ALL
-        elif status == "UNDETERMINED" or status == "UNREACHABLE":
+        elif status == "UNDETERMINED":
             message = Fore.YELLOW + f"{status}" + Style.RESET_ALL
+            number_tests_undetermined += 1
+        elif status == "UNREACHABLE":
+            message = Fore.YELLOW + f"{status}" + Style.RESET_ALL
+            number_tests_unreachable += 1
         else:
             number_tests_failed += 1
             failed_tests.append(property_instance)
@@ -443,7 +449,17 @@ def construct_property_message(properties):
         output_message += f"Check {index+1}: {name}\n\t - Status: " + \
             message + f"\n\t - Description: \"{description}\"\n" + "\n"
 
-    output_message += f"\nSUMMARY: \n ** {number_tests_failed} of {index+1} failed\n"
+    output_message += f"\nSUMMARY: \n ** {number_tests_failed} of {index+1} failed"
+    other_status = []
+    if number_tests_undetermined > 0:
+        other_status.append(f"{number_tests_undetermined} undetermined")
+    if number_tests_unreachable > 0:
+        other_status.append(f"{number_tests_unreachable} unreachable")
+    if other_status:
+        output_message += " ("
+        output_message += ",".join(other_status)
+        output_message += ")"
+    output_message += "\n"
 
     # The Verification is successful and the program is verified
     if number_tests_failed == 0:

diff --git a/tests/expected/reach/reachable_failure/expected b/tests/expected/reach/reachable_failure/expected
@@ -1,2 +1,3 @@
 FAILURE
+ ** 1 of 3 failed
 Failed Checks: assertion failed: x != 5
diff --git a/tests/expected/reach/reachable_success/expected b/tests/expected/reach/reachable_success/expected
@@ -1,2 +1,3 @@
 SUCCESS
+ ** 0 of 2 failed
 SUCCESSFUL
diff --git a/tests/expected/reach/unreachable/expected b/tests/expected/reach/unreachable/expected
@@ -1 +1,2 @@
 UNREACHABLE
+ ** 1 of 5 failed (1 unreachable)
diff --git a/tests/expected/report/unsupported/failure/expected b/tests/expected/report/unsupported/failure/expected
@@ -1,4 +1,5 @@
 assertion failed: x == 0
 Failed Checks: assertion failed: x == 0
+ ** 2 of 4 failed (2 undetermined)
 Failed Checks: InlineAsm is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2
 ** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details.
diff --git a/tests/expected/report/unsupported/reachable/expected b/tests/expected/report/unsupported/reachable/expected
@@ -1,4 +1,5 @@
 UNDETERMINED
 assertion failed: x == 0
+ ** 1 of 3 failed (2 undetermined)
 Failed Checks: InlineAsm is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2
 ** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details.
diff --git a/tests/expected/report/unsupported/unreachable/expected b/tests/expected/report/unsupported/unreachable/expected
@@ -1,3 +1,4 @@
 SUCCESS
 assertion failed: x == 0
+ ** 0 of 4 failed
 SUCCESSFUL