From d536dc9b1d16f1b0a7919e4dbbeba90311fe9b02 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Wed, 23 Feb 2022 13:18:04 -0800
Subject: [PATCH] Include undetermined and unreachable in the verification
 summary (#856)

---
 scripts/cbmc_json_parser.py                   | 20 +++++++++++++++++--
 .../expected/reach/reachable_failure/expected |  1 +
 .../expected/reach/reachable_success/expected |  1 +
 tests/expected/reach/unreachable/expected     |  1 +
 .../report/unsupported/failure/expected       |  1 +
 .../report/unsupported/reachable/expected     |  1 +
 .../report/unsupported/unreachable/expected   |  1 +
 7 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py
index 7e8c930392480..3da07aa1851bc 100755
--- 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
index bad361ee08cec..22eecede5a0f0 100644
--- 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
index b20238a91644f..114119d26c74d 100644
--- 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
index 7703d171eb67b..8582b462241bb 100644
--- 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
index 9079da2591ae9..83ddd0ef3f23e 100644
--- 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
index 70ea92c34620f..f8eaed6964433 100644
--- 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
index d200f4c19aa45..2759f0e6c7fea 100644
--- 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