SMV: KNOWNBUG test for module type checking

NuSMV defers module type checking until the module is instantiated.  Hence,
errors are tolerated if the module is not instantiated.

Author: kroening

regression/smv/modules/parameters2.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+parameters2.smv
+
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This yields a type-checking error.

regression/smv/modules/parameters2.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+MODULE my-module(x)
+
+-- this is tolerated when the module is not instantiated
+CTLSPEC x + 1
+
+-- this, too
+CTLSPEC something_not_known_at_all