From 008d020c4defd135b779d0d052c077260a33829f Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Tue, 29 Mar 2022 19:10:29 +0200
Subject: [PATCH] note unexpected return statuses in junit

---
 sbysrc/sby_core.py              |  8 ++++++--
 tests/.gitignore                |  1 +
 tests/Makefile                  |  5 ++++-
 tests/scripted/.gitignore       |  1 +
 tests/scripted/Makefile         | 11 +++++++++++
 tests/scripted/junit_expect.sby | 16 ++++++++++++++++
 tests/scripted/junit_expect.sh  |  5 +++++
 7 files changed, 44 insertions(+), 3 deletions(-)
 create mode 100644 tests/scripted/.gitignore
 create mode 100644 tests/scripted/Makefile
 create mode 100644 tests/scripted/junit_expect.sby
 create mode 100644 tests/scripted/junit_expect.sh

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index b78ef85..1e96d00 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -788,7 +788,11 @@ class SbyTask:
             if self.retcode == 16:
                 print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
             elif self.retcode != 0:
-                print(f'<failure type="{junit_type}" message="{self.status}" />', file=f)
+                if len(self.expect) > 1 or "PASS" not in self.expect:
+                    expected = " ".join(self.expect)
+                    print(f'<failure type="EXPECT" message="Task returned status {self.status}. Expected values were: {expected}" />', file=f)
+                else:
+                    print(f'<failure type="{self.status}" message="Task returned status {self.status}." />', file=f)
             print(f'</testcase>', file=f)
 
             for check in checks:
@@ -814,11 +818,11 @@ class SbyTask:
                     print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
                 print(f'</testcase>', file=f)
         else:
-            junit_type = "assert" if self.opt_mode in ["bmc", "prove"] else self.opt_mode
             print(f'<testcase classname="{junit_tc_name}" name="{junit_tc_name}" time="{self.total_time}">', file=f)
             if junit_errors:
                 print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
             elif junit_failures:
+                junit_type = "assert" if self.opt_mode in ["bmc", "prove"] else self.opt_mode
                 print(f'<failure type="{junit_type}" message="{self.status}" />', file=f)
             print(f'</testcase>', file=f)
         print('<system-out>', end="", file=f)
diff --git a/tests/.gitignore b/tests/.gitignore
index 120675b..c6bf5b5 100644
--- a/tests/.gitignore
+++ b/tests/.gitignore
@@ -11,3 +11,4 @@
 /submod_props*/
 /multi_assert*/
 /aim_vs_smt2_nonzero_start_offset*/
+/2props1trace*/
diff --git a/tests/Makefile b/tests/Makefile
index 8f1d00c..15e87ff 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -4,7 +4,7 @@ JUNIT_TESTS=junit_assert_pass junit_assert_fail junit_assert_preunsat \
 junit_cover_pass junit_cover_uncovered junit_cover_assert junit_cover_preunsat \
 junit_timeout_error_timeout junit_timeout_error_syntax junit_timeout_error_solver
 
-.PHONY: test validate_junit
+.PHONY: test validate_junit scripted
 
 test: $(JUNIT_TESTS)
 
@@ -14,4 +14,7 @@ test_%: %.sby FORCE
 $(JUNIT_TESTS): $(SBY_TESTS)
 	python3 validate_junit.py $@/$@.xml
 
+scripted:
+	make -C scripted
+
 FORCE:
diff --git a/tests/scripted/.gitignore b/tests/scripted/.gitignore
new file mode 100644
index 0000000..6403b85
--- /dev/null
+++ b/tests/scripted/.gitignore
@@ -0,0 +1 @@
+/junit_*/
diff --git a/tests/scripted/Makefile b/tests/scripted/Makefile
new file mode 100644
index 0000000..ca27199
--- /dev/null
+++ b/tests/scripted/Makefile
@@ -0,0 +1,11 @@
+SH_FILES=$(wildcard *.sh)
+SH_TESTS=$(addprefix test_,$(SH_FILES:.sh=))
+
+test: $(SH_TESTS)
+
+test_%: %.sh FORCE
+	bash $<
+
+FORCE:
+
+.PHONY: test FORCE
diff --git a/tests/scripted/junit_expect.sby b/tests/scripted/junit_expect.sby
new file mode 100644
index 0000000..63d65a6
--- /dev/null
+++ b/tests/scripted/junit_expect.sby
@@ -0,0 +1,16 @@
+[options]
+mode bmc
+depth 1
+expect fail,timeout
+
+[engines]
+smtbmc
+
+[script]
+read -formal foo.v
+prep -top foo
+
+[file foo.v]
+module foo;
+always_comb assert(1);
+endmodule
diff --git a/tests/scripted/junit_expect.sh b/tests/scripted/junit_expect.sh
new file mode 100644
index 0000000..27b972d
--- /dev/null
+++ b/tests/scripted/junit_expect.sh
@@ -0,0 +1,5 @@
+#!/bin/bash
+
+# this is expected to return 1 so don't use 'set -e'
+python3 ../../sbysrc/sby.py -f junit_expect.sby
+grep '<failure type="EXPECT" message="Task returned status PASS. Expected values were: FAIL TIMEOUT" />' junit_expect/junit_expect.xml
-- 
2.30.2