Skip to content

Commit

Permalink
Merge pull request #997 from diffblue/smv-grammar
Browse files Browse the repository at this point in the history
SMV: rename production rules in grammar
  • Loading branch information
kroening authored Feb 18, 2025
2 parents 45c1cbf + 3cb6193 commit aeb8c12
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 aeb8c12

Please sign in to comment.