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

SMV: add tests for type checking errors

Author: tautschnig

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$
+--

regression/smv/boolean/boolean_expected1.smv

@@ -0,0 +1,3 @@
+MODULE main
+
+SPEC 10

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$
+--

regression/smv/boolean/boolean_expected2.smv

@@ -0,0 +1,5 @@
+MODULE main
+
+VAR x : 1..10;
+
+ASSIGN x := 5 ? 1 : 2;

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$
+--

regression/smv/boolean/boolean_expected3.smv

@@ -0,0 +1,3 @@
+MODULE main
+
+SPEC 1 & 3

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$
+--

regression/smv/boolean/boolean_expected4.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x : 1..10;
+
+ASSIGN x := case
+  5 : 1;
+  1 : 1;
+esac;
+