Skip to content

Commit 029f48a

Browse files
authored
Merge pull request #1408 from diffblue/parameters2
SMV: KNOWNBUG test for module type checking
2 parents b419449 + 5c3c88e commit 029f48a

File tree

2 files changed

+18
-0
lines changed

2 files changed

+18
-0
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
parameters2.smv
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
This yields a type-checking error.
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
MODULE main
2+
3+
MODULE my-module(x)
4+
5+
-- this is tolerated when the module is not instantiated
6+
CTLSPEC x + 1
7+
8+
-- this, too
9+
CTLSPEC something_not_known_at_all

0 commit comments

Comments
 (0)