Skip to content

Commit

Permalink
SMV: add tests for type checking errors
Browse files Browse the repository at this point in the history
This adds four tests for cases when a Boolean is expected.
  • Loading branch information
kroening committed Dec 23, 2024
1 parent 11397bf commit c84cfff
Show file tree
Hide file tree
Showing 8 changed files with 48 additions and 0 deletions.
7 changes: 7 additions & 0 deletions regression/smv/boolean/boolean_expected1.desc
Original file line number Diff line number Diff line change
@@ -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$
--
3 changes: 3 additions & 0 deletions regression/smv/boolean/boolean_expected1.smv
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
MODULE main

SPEC 10
7 changes: 7 additions & 0 deletions regression/smv/boolean/boolean_expected2.desc
Original file line number Diff line number Diff line change
@@ -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$
--
5 changes: 5 additions & 0 deletions regression/smv/boolean/boolean_expected2.smv
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
MODULE main

VAR x : 1..10;

ASSIGN x := 5 ? 1 : 2;
7 changes: 7 additions & 0 deletions regression/smv/boolean/boolean_expected3.desc
Original file line number Diff line number Diff line change
@@ -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$
--
3 changes: 3 additions & 0 deletions regression/smv/boolean/boolean_expected3.smv
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
MODULE main

SPEC 1 & 3
7 changes: 7 additions & 0 deletions regression/smv/boolean/boolean_expected4.desc
Original file line number Diff line number Diff line change
@@ -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$
--
9 changes: 9 additions & 0 deletions regression/smv/boolean/boolean_expected4.smv
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
MODULE main

VAR x : 1..10;

ASSIGN x := case
5 : 1;
1 : 1;
esac;

0 comments on commit c84cfff

Please sign in to comment.