SMV: KNOWNBUG test for bare section headers

Bare TRANS/INIT/INVAR/FAIRNESS/SPEC/CTLSPEC/LTLSPEC headers are accepted
as empty sections (parser.y:447). Truncated or malformed SMV input can
silently weaken the model instead of failing with a parse error.

Author: kroening

regression/smv/syntax-errors/bare_section_headers1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+bare_section_headers1.smv
+--bound 1
+^EXIT=1$
+^SIGNAL=0$
+--
+Bare TRANS/INIT/INVAR/FAIRNESS/SPEC/CTLSPEC/LTLSPEC headers are accepted
+as empty sections (parser.y:447). Truncated or malformed SMV input can
+silently weaken the model instead of failing with a parse error.

regression/smv/syntax-errors/bare_section_headers1.smv

@@ -0,0 +1,14 @@
+-- Bare section headers with no formula should be rejected.
+-- Truncated or malformed input can silently weaken the model.
+
+MODULE main
+
+VAR x : boolean;
+
+TRANS
+INIT
+INVAR
+FAIRNESS
+SPEC
+CTLSPEC
+LTLSPEC