From c84cfffe25e51b86b60700a5f271638a9c679db3 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 23 Dec 2024 14:21:15 +0000
Subject: [PATCH] SMV: add tests for type checking errors

This adds four tests for cases when a Boolean is expected.
---
 regression/smv/boolean/boolean_expected1.desc | 7 +++++++
 regression/smv/boolean/boolean_expected1.smv  | 3 +++
 regression/smv/boolean/boolean_expected2.desc | 7 +++++++
 regression/smv/boolean/boolean_expected2.smv  | 5 +++++
 regression/smv/boolean/boolean_expected3.desc | 7 +++++++
 regression/smv/boolean/boolean_expected3.smv  | 3 +++
 regression/smv/boolean/boolean_expected4.desc | 7 +++++++
 regression/smv/boolean/boolean_expected4.smv  | 9 +++++++++
 8 files changed, 48 insertions(+)
 create mode 100644 regression/smv/boolean/boolean_expected1.desc
 create mode 100644 regression/smv/boolean/boolean_expected1.smv
 create mode 100644 regression/smv/boolean/boolean_expected2.desc
 create mode 100644 regression/smv/boolean/boolean_expected2.smv
 create mode 100644 regression/smv/boolean/boolean_expected3.desc
 create mode 100644 regression/smv/boolean/boolean_expected3.smv
 create mode 100644 regression/smv/boolean/boolean_expected4.desc
 create mode 100644 regression/smv/boolean/boolean_expected4.smv

diff --git a/regression/smv/boolean/boolean_expected1.desc b/regression/smv/boolean/boolean_expected1.desc
new file mode 100644
index 00000000..7386134a
--- /dev/null
+++ 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
new file mode 100644
index 00000000..eccf774d
--- /dev/null
+++ 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
new file mode 100644
index 00000000..37d6faaf
--- /dev/null
+++ 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
new file mode 100644
index 00000000..fc0dad0c
--- /dev/null
+++ 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
new file mode 100644
index 00000000..b3ff245d
--- /dev/null
+++ 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
new file mode 100644
index 00000000..8fd58c0e
--- /dev/null
+++ 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
new file mode 100644
index 00000000..c598aad3
--- /dev/null
+++ 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
new file mode 100644
index 00000000..a0c42742
--- /dev/null
+++ 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;
+