Merge pull request #900 from diffblue/smv-boolean-expected

SMV: add tests for type checking errors
diffblue · Dec 26, 2024 · 7ae93d8 · 7ae93d8
2 parents 5df5178 + c84cfff
commit 7ae93d8
Show file tree

Hide file tree

Showing 8 changed files with 48 additions and 0 deletions.
diff --git a/regression/smv/boolean/boolean_expected1.desc b/regression/smv/boolean/boolean_expected1.desc
@@ -0,0 +1,7 @@
+CORE
+boolean_expected1.smv
+
+^file boolean_expected1\.smv line 3: expected 0 or 1 here, but got 10$
+^EXIT=2$
+^SIGNAL=0$
+--
diff --git a/regression/smv/boolean/boolean_expected1.smv b/regression/smv/boolean/boolean_expected1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+SPEC 10
diff --git a/regression/smv/boolean/boolean_expected2.desc b/regression/smv/boolean/boolean_expected2.desc
@@ -0,0 +1,7 @@
+CORE
+boolean_expected2.smv
+
+^file boolean_expected2\.smv line 5: expected 0 or 1 here, but got 5$
+^EXIT=2$
+^SIGNAL=0$
+--
diff --git a/regression/smv/boolean/boolean_expected2.smv b/regression/smv/boolean/boolean_expected2.smv
@@ -0,0 +1,5 @@
+MODULE main
+
+VAR x : 1..10;
+
+ASSIGN x := 5 ? 1 : 2;
diff --git a/regression/smv/boolean/boolean_expected3.desc b/regression/smv/boolean/boolean_expected3.desc
@@ -0,0 +1,7 @@
+CORE
+boolean_expected3.smv
+
+^file boolean_expected3\.smv line 3: expected 0 or 1 here, but got 3$
+^EXIT=2$
+^SIGNAL=0$
+--
diff --git a/regression/smv/boolean/boolean_expected3.smv b/regression/smv/boolean/boolean_expected3.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+SPEC 1 & 3
diff --git a/regression/smv/boolean/boolean_expected4.desc b/regression/smv/boolean/boolean_expected4.desc
@@ -0,0 +1,7 @@
+CORE
+boolean_expected4.smv
+
+^file boolean_expected4\.smv line 6: expected 0 or 1 here, but got 5$
+^EXIT=2$
+^SIGNAL=0$
+--
diff --git a/regression/smv/boolean/boolean_expected4.smv b/regression/smv/boolean/boolean_expected4.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x : 1..10;
+
+ASSIGN x := case
+  5 : 1;
+  1 : 1;
+esac;
+