Skip to content

Commit

Permalink
SMV: rename production rules in grammar
Browse files Browse the repository at this point in the history
This renames some production rules in the SMV grammar to match the NuSMV manual.
https://nusmv.fbk.eu/userman/v27/nusmv.pdf
  • Loading branch information
kroening committed Feb 18, 2025
1 parent 45c1cbf commit 3cb6193
Showing 1 changed file with 10 additions and 4 deletions.
14 changes: 10 additions & 4 deletions src/smvlang/parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -380,7 +380,13 @@ module_argument_list_opt: /* empty */
| module_argument_list
;

type : array_Token NUMBER_Token DOTDOT_Token NUMBER_Token of_Token type
type_specifier:
simple_type_specifier
| module_type_specifier
;

simple_type_specifier:
array_Token NUMBER_Token DOTDOT_Token NUMBER_Token of_Token simple_type_specifier
{
init($$, ID_array);
int start=atoi(stack_expr($2).id().c_str());
Expand All @@ -404,10 +410,10 @@ type : array_Token NUMBER_Token DOTDOT_Token NUMBER_Token of_Token type
stack_type($$).set(ID_from, stack_expr($1));
stack_type($$).set(ID_to, stack_expr($3));
}
| usertype
;

usertype : module_name
module_type_specifier:
module_name
{
init($$, "submodule");
stack_expr($$).set(ID_identifier,
Expand Down Expand Up @@ -441,7 +447,7 @@ enum_element: STRING_Token
}
;

vardecl : variable_name ':' type ';'
vardecl : variable_name ':' type_specifier ';'
{
const irep_idt &identifier=stack_expr($1).get(ID_identifier);
smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
Expand Down

0 comments on commit 3cb6193

Please sign in to comment.