SMV: grammar for missing declarations

kroening · kroening · commit 2ceda01aeb87 · 2025-07-17T10:53:31.000-07:00
This adds the grammar for IVAR, FROZENVAR, CONSTANTS, COMPUTE, and ISA
declarations to the SMV parser.  Usage of these constructs yields an error
message that the feature is not supported.
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;`