Merge pull request #1207 from diffblue/smv-missing-declarations

tautschnig · web-flow · commit 090e1cc4c7f9 · 2025-07-18T18:28:35.000+02:00
SMV: grammar for missing declarations
diff --git a/regression/smv/compute/compute1.desc b/regression/smv/compute/compute1.desc
@@ -0,0 +1,8 @@
+CORE
+compute1.smv
+
+^file .* line 3: No support for COMPUTE specifications .*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/compute/compute1.smv b/regression/smv/compute/compute1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+COMPUTE MIN [TRUE, TRUE];
diff --git a/regression/smv/constants/constants1.desc b/regression/smv/constants/constants1.desc
@@ -0,0 +1,8 @@
+CORE
+constants1.smv
+
+^file .* line 3: No support for CONSTANTS declarations .*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/constants/constants1.smv b/regression/smv/constants/constants1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+CONSTANTS some_constant;
diff --git a/regression/smv/frozenvar/frozenvar1.desc b/regression/smv/frozenvar/frozenvar1.desc
@@ -0,0 +1,8 @@
+CORE
+frozenvar1.smv
+
+^file .* line 3: No support for FROZENVAR declarations$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/frozenvar/frozenvar1.smv b/regression/smv/frozenvar/frozenvar1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+FROZENVAR some_var : boolean;
diff --git a/regression/smv/isa/isa1.desc b/regression/smv/isa/isa1.desc
@@ -0,0 +1,8 @@
+CORE
+isa1.smv
+
+^file .* line 3: No support for ISA declarations .*$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/isa/isa1.smv b/regression/smv/isa/isa1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+ISA some_isa
diff --git a/regression/smv/ivar/ivar1.desc b/regression/smv/ivar/ivar1.desc
@@ -0,0 +1,8 @@
+CORE
+ivar1.smv
+
+^file .* line 3: No support for IVAR declarations$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/ivar/ivar1.smv b/regression/smv/ivar/ivar1.smv
@@ -0,0 +1,3 @@
+MODULE main
+
+IVAR some_input : boolean;
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
@@ -369,14 +369,20 @@ semi_opt   :    /* empty */
 
 module_element:
              var_declaration
+           | ivar_declaration
+           | frozenvar_declaration
            | define_declaration
+           | constants_declaration
            | assign_constraint
            | trans_constraint
            | init_constraint
            | invar_constraint
            | fairness_constraint
            | ctl_specification
            | ltl_specification
+           | compute_specification
+           | isa_declaration
+           /* not in the NuSMV manual */
            | EXTERN_Token extern_var semi_opt
            | EXTERN_Token
            ;
@@ -386,11 +392,78 @@ var_declaration:
            | VAR_Token
            ;
 
+ivar_declaration:
+             IVAR_Token simple_var_list
+           {
+             yyerror("No support for IVAR declarations");
+             YYERROR;
+           }
+           ;
+
+frozenvar_declaration:
+             FROZENVAR_Token simple_var_list
+           {
+             yyerror("No support for FROZENVAR declarations");
+             YYERROR;
+           }
+           ;
+
+simple_var_list:
+             identifier ':' simple_type_specifier ';'
+           | simple_var_list identifier ':' simple_type_specifier ';'
+
 define_declaration:
              DEFINE_Token defines
            | DEFINE_Token
            ;
 
+constants_declaration:
+             CONSTANTS_Token constants_body ';'
+           {
+             yyerror("No support for CONSTANTS declarations");
+             YYERROR;
+           }
+           ;
+
+constants_body:
+             complex_identifier
+           | constants_body ',' complex_identifier
+           ;
+
+compute_specification:
+             COMPUTE_Token compute_expr
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           | COMPUTE_Token compute_expr ';'
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           | COMPUTE_Token NAME_Token identifier ":=" compute_expr
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           | COMPUTE_Token NAME_Token identifier ":=" compute_expr ';'
+           {
+             yyerror("No support for COMPUTE specifications");
+             YYERROR;
+           }
+           ;
+
+compute_expr:
+           ;
+
+isa_declaration:
+             ISA_Token identifier
+           {
+             yyerror("No support for ISA declarations");
+             YYERROR;
+           }
+           ;
+
 assign_constraint:
              ASSIGN_Token assignments
            | ASSIGN_Token

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+MODULE main`
	`2`	`+`
	`3`	`+COMPUTE MIN [TRUE, TRUE];`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+MODULE main`
	`2`	`+`
	`3`	`+CONSTANTS some_constant;`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+MODULE main`
	`2`	`+`
	`3`	`+FROZENVAR some_var : boolean;`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+MODULE main`
	`2`	`+`
	`3`	`+IVAR some_input : boolean;`