From 2ceda01aeb87a82fe19ed3d3e62e91227ee50aa3 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 17 Jul 2025 10:41:16 -0700 Subject: [PATCH] SMV: grammar for missing declarations 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. --- regression/smv/compute/compute1.desc | 8 +++ regression/smv/compute/compute1.smv | 3 + regression/smv/constants/constants1.desc | 8 +++ regression/smv/constants/constants1.smv | 3 + regression/smv/frozenvar/frozenvar1.desc | 8 +++ regression/smv/frozenvar/frozenvar1.smv | 3 + regression/smv/isa/isa1.desc | 8 +++ regression/smv/isa/isa1.smv | 3 + regression/smv/ivar/ivar1.desc | 8 +++ regression/smv/ivar/ivar1.smv | 3 + src/smvlang/parser.y | 73 ++++++++++++++++++++++++ 11 files changed, 128 insertions(+) create mode 100644 regression/smv/compute/compute1.desc create mode 100644 regression/smv/compute/compute1.smv create mode 100644 regression/smv/constants/constants1.desc create mode 100644 regression/smv/constants/constants1.smv create mode 100644 regression/smv/frozenvar/frozenvar1.desc create mode 100644 regression/smv/frozenvar/frozenvar1.smv create mode 100644 regression/smv/isa/isa1.desc create mode 100644 regression/smv/isa/isa1.smv create mode 100644 regression/smv/ivar/ivar1.desc create mode 100644 regression/smv/ivar/ivar1.smv diff --git a/regression/smv/compute/compute1.desc b/regression/smv/compute/compute1.desc new file mode 100644 index 000000000..30eae8a28 --- /dev/null +++ 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 new file mode 100644 index 000000000..06607abef --- /dev/null +++ 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 new file mode 100644 index 000000000..a7fa5e356 --- /dev/null +++ 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 new file mode 100644 index 000000000..e81428c71 --- /dev/null +++ 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 new file mode 100644 index 000000000..67e201925 --- /dev/null +++ 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 new file mode 100644 index 000000000..542fddc59 --- /dev/null +++ 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 new file mode 100644 index 000000000..9b62e2f26 --- /dev/null +++ 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 new file mode 100644 index 000000000..b29aeae52 --- /dev/null +++ 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 new file mode 100644 index 000000000..e6cb0032c --- /dev/null +++ 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 new file mode 100644 index 000000000..eb9ff90a8 --- /dev/null +++ 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 index b4819ba20..b3b68e9f4 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -369,7 +369,10 @@ semi_opt : /* empty */ module_element: var_declaration + | ivar_declaration + | frozenvar_declaration | define_declaration + | constants_declaration | assign_constraint | trans_constraint | init_constraint @@ -377,6 +380,9 @@ module_element: | 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