Merge pull request #150 from nakengelhardt/fix_junit_type_assignment

note unexpected return statuses in junit

tests/.gitignore

@@ -12,3 +12,4 @@
 /submod_props*/
 /multi_assert*/
 /aim_vs_smt2_nonzero_start_offset*/
+/2props1trace*/

tests/Makefile

@@ -6,7 +6,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) $(CHECK_PY_TASKS)
 
@@ -19,4 +19,7 @@ $(CHECK_PY_TASKS): check_%: %.check.py test_%
 $(JUNIT_TESTS): $(SBY_TESTS)
 	python3 validate_junit.py $@/$@.xml
 
+scripted:
+	make -C scripted
+
 FORCE:

tests/scripted/.gitignore

@@ -0,0 +1 @@
+/junit_*/

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

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

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