Skip to content

Commit 14d0d33

Browse files
committed
SMV: variable definitions are now parse tree items
1 parent 955c752 commit 14d0d33

File tree

4 files changed

+29
-8
lines changed

4 files changed

+29
-8
lines changed

src/smvlang/parser.y

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -594,7 +594,7 @@ vardecl : variable_identifier ':' type_specifier ';'
594594
switch(var.var_class)
595595
{
596596
case smv_parse_treet::mc_vart::UNKNOWN:
597-
var.type=(typet &)stack_expr($3);
597+
var.type=stack_type($3);
598598
var.var_class=smv_parse_treet::mc_vart::DECLARED;
599599
break;
600600

@@ -616,6 +616,8 @@ vardecl : variable_identifier ':' type_specifier ';'
616616
default:
617617
DATA_INVARIANT(false, "unexpected variable class");
618618
}
619+
620+
PARSER.module->add_var(stack_expr($1), stack_type($3));
619621
}
620622
;
621623

src/smvlang/smv_parse_tree.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,7 @@ std::string to_string(smv_parse_treet::modulet::itemt::item_typet i)
7373
return "LTLSPEC";
7474
case smv_parse_treet::modulet::itemt::FAIRNESS: return "FAIRNESS";
7575
case smv_parse_treet::modulet::itemt::DEFINE: return "DEFINE";
76+
case smv_parse_treet::modulet::itemt::VAR: return "VAR";
7677

7778
default:;
7879
}

src/smvlang/smv_parse_tree.h

Lines changed: 17 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -46,12 +46,13 @@ class smv_parse_treet
4646
ASSIGN_INIT,
4747
ASSIGN_NEXT,
4848
CTLSPEC,
49-
LTLSPEC,
50-
INIT,
51-
TRANS,
5249
DEFINE,
50+
FAIRNESS,
51+
INIT,
5352
INVAR,
54-
FAIRNESS
53+
LTLSPEC,
54+
TRANS,
55+
VAR
5556
};
5657

5758
itemt(item_typet __item_type, exprt __expr, source_locationt __location)
@@ -124,6 +125,11 @@ class smv_parse_treet
124125
{
125126
return item_type==INIT;
126127
}
128+
129+
bool is_var() const
130+
{
131+
return item_type == VAR;
132+
}
127133

128134
// for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE
129135
const equal_exprt &equal_expr() const
@@ -247,6 +253,13 @@ class smv_parse_treet
247253
items.emplace_back(itemt::TRANS, std::move(expr), std::move(location));
248254
}
249255

256+
void add_var(exprt expr, typet type)
257+
{
258+
expr.type() = std::move(type);
259+
auto location = expr.source_location();
260+
items.emplace_back(itemt::VAR, std::move(expr), std::move(location));
261+
}
262+
250263
mc_varst vars;
251264
enum_sett enum_set;
252265

src/smvlang/smv_typecheck.cpp

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1893,6 +1893,9 @@ void smv_typecheckt::typecheck(
18931893
typecheck(item.expr, OTHER);
18941894
item.equal_expr().type() = bool_typet{};
18951895
return;
1896+
1897+
case smv_parse_treet::modulet::itemt::VAR:
1898+
return;
18961899
}
18971900
}
18981901

@@ -2104,6 +2107,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
21042107

21052108
define_map.clear();
21062109

2110+
// variables first, need to be visible before declaration
21072111
convert(smv_module.vars);
21082112

21092113
// transition relation
@@ -2122,9 +2126,10 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
21222126

21232127
convert_ports(smv_module, module_symbol.type);
21242128

2125-
for (auto &item : smv_module.items) {
2126-
convert(item);
2127-
}
2129+
// non-variable items
2130+
for(auto &item : smv_module.items)
2131+
if(!item.is_var())
2132+
convert(item);
21282133

21292134
flatten_hierarchy(smv_module);
21302135

0 commit comments

Comments
 (0)