From 3a8de7d1d22a49b7a660e0d13828f6feaa39eb7c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 10 Nov 2025 12:39:21 -0800 Subject: [PATCH] SMV: item -> element The NuSMV manual uses the term "module element" for the parts of the module body. This renames the data structure in the SMV parse tree from itemt to elementt. --- src/smvlang/smv_language.cpp | 28 ++--- src/smvlang/smv_parse_tree.cpp | 32 +++--- src/smvlang/smv_parse_tree.h | 121 ++++++++++---------- src/smvlang/smv_typecheck.cpp | 196 +++++++++++++++++---------------- 4 files changed, 197 insertions(+), 180 deletions(-) diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp index e2e0ab4ad..06235bb3f 100644 --- a/src/smvlang/smv_language.cpp +++ b/src/smvlang/smv_language.cpp @@ -69,10 +69,10 @@ void smv_languaget::dependencies( const smv_parse_treet::modulet &smv_module=m_it->second; - for(auto &item : smv_module.items) - if(item.is_var() && item.expr.type().id() == ID_smv_submodule) + for(auto &element : smv_module.elements) + if(element.is_var() && element.expr.type().id() == ID_smv_submodule) module_set.insert( - id2string(to_smv_submodule_type(item.expr.type()).identifier())); + id2string(to_smv_submodule_type(element.expr.type()).identifier())); } /*******************************************************************\ @@ -145,13 +145,13 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &) out << " VARIABLES:" << std::endl; - for(auto &item : module.items) - if(item.is_var() && item.expr.type().id() != ID_smv_submodule) + for(auto &element : module.elements) + if(element.is_var() && element.expr.type().id() != ID_smv_submodule) { symbol_tablet symbol_table; namespacet ns{symbol_table}; - auto identifier = to_smv_identifier_expr(item.expr).identifier(); - auto msg = type2smv(item.expr.type(), ns); + auto identifier = to_smv_identifier_expr(element.expr).identifier(); + auto msg = type2smv(element.expr.type(), ns); out << " " << identifier << ": " << msg << ";\n"; } @@ -159,13 +159,13 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &) out << " SUBMODULES:" << std::endl; - for(auto &item : module.items) - if(item.is_var() && item.expr.type().id() == ID_smv_submodule) + for(auto &element : module.elements) + if(element.is_var() && element.expr.type().id() == ID_smv_submodule) { symbol_tablet symbol_table; namespacet ns(symbol_table); - auto identifier = to_smv_identifier_expr(item.expr).identifier(); - auto msg = type2smv(item.expr.type(), ns); + auto identifier = to_smv_identifier_expr(element.expr).identifier(); + auto msg = type2smv(element.expr.type(), ns); out << " " << identifier << ": " << msg << ";\n"; } @@ -173,10 +173,10 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &) out << " ITEMS:" << std::endl; - forall_item_list(it, module.items) + for(auto &element : module.elements) { - out << " TYPE: " << to_string(it->item_type) << std::endl; - out << " EXPR: " << it->expr.pretty() << std::endl; + out << " TYPE: " << to_string(element.element_type) << '\n'; + out << " EXPR: " << element.expr.pretty() << '\n'; out << std::endl; } } diff --git a/src/smvlang/smv_parse_tree.cpp b/src/smvlang/smv_parse_tree.cpp index 3dea7dcd9..7a663499e 100644 --- a/src/smvlang/smv_parse_tree.cpp +++ b/src/smvlang/smv_parse_tree.cpp @@ -54,31 +54,35 @@ Function: operator << \*******************************************************************/ -std::string to_string(smv_parse_treet::modulet::itemt::item_typet i) +std::string to_string(smv_parse_treet::modulet::elementt::element_typet i) { switch(i) { - case smv_parse_treet::modulet::itemt::ASSIGN_CURRENT: + case smv_parse_treet::modulet::elementt::ASSIGN_CURRENT: return "ASSIGN CURRENT"; - case smv_parse_treet::modulet::itemt::ASSIGN_INIT: + case smv_parse_treet::modulet::elementt::ASSIGN_INIT: return "ASSIGN INIT"; - case smv_parse_treet::modulet::itemt::ASSIGN_NEXT: + case smv_parse_treet::modulet::elementt::ASSIGN_NEXT: return "ASSIGN NEXT"; - case smv_parse_treet::modulet::itemt::INVAR: return "INVAR"; - case smv_parse_treet::modulet::itemt::TRANS: return "TRANS"; - case smv_parse_treet::modulet::itemt::INIT: return "INIT"; - case smv_parse_treet::modulet::itemt::CTLSPEC: + case smv_parse_treet::modulet::elementt::INVAR: + return "INVAR"; + case smv_parse_treet::modulet::elementt::TRANS: + return "TRANS"; + case smv_parse_treet::modulet::elementt::INIT: + return "INIT"; + case smv_parse_treet::modulet::elementt::CTLSPEC: return "SPEC"; - case smv_parse_treet::modulet::itemt::LTLSPEC: + case smv_parse_treet::modulet::elementt::LTLSPEC: return "LTLSPEC"; - case smv_parse_treet::modulet::itemt::FAIRNESS: return "FAIRNESS"; - case smv_parse_treet::modulet::itemt::DEFINE: + case smv_parse_treet::modulet::elementt::FAIRNESS: + return "FAIRNESS"; + case smv_parse_treet::modulet::elementt::DEFINE: return "DEFINE"; - case smv_parse_treet::modulet::itemt::ENUM: + case smv_parse_treet::modulet::elementt::ENUM: return "ENUM"; - case smv_parse_treet::modulet::itemt::IVAR: + case smv_parse_treet::modulet::elementt::IVAR: return "IVAR"; - case smv_parse_treet::modulet::itemt::VAR: + case smv_parse_treet::modulet::elementt::VAR: return "VAR"; default:; diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h index 30d7734f1..bc242cc6e 100644 --- a/src/smvlang/smv_parse_tree.h +++ b/src/smvlang/smv_parse_tree.h @@ -25,9 +25,9 @@ class smv_parse_treet irep_idt name, base_name; std::list parameters; - struct itemt + struct elementt { - enum item_typet + enum element_typet { ASSIGN_CURRENT, ASSIGN_INIT, @@ -44,90 +44,93 @@ class smv_parse_treet VAR }; - itemt(item_typet __item_type, exprt __expr, source_locationt __location) - : item_type(__item_type), + elementt( + element_typet __element_type, + exprt __expr, + source_locationt __location) + : element_type(__element_type), expr(std::move(__expr)), location(std::move(__location)) { } - itemt( - item_typet __item_type, + elementt( + element_typet __element_type, irep_idt __name, exprt __expr, source_locationt __location) - : item_type(__item_type), + : element_type(__element_type), name(__name), expr(std::move(__expr)), location(std::move(__location)) { } - friend std::string to_string(item_typet i); - - item_typet item_type; + friend std::string to_string(element_typet i); + + element_typet element_type; std::optional name; exprt expr; source_locationt location; bool is_assign_current() const { - return item_type == ASSIGN_CURRENT; + return element_type == ASSIGN_CURRENT; } bool is_assign_init() const { - return item_type == ASSIGN_INIT; + return element_type == ASSIGN_INIT; } bool is_assign_next() const { - return item_type == ASSIGN_NEXT; + return element_type == ASSIGN_NEXT; } bool is_ctlspec() const { - return item_type == CTLSPEC; + return element_type == CTLSPEC; } bool is_ltlspec() const { - return item_type == LTLSPEC; + return element_type == LTLSPEC; } bool is_define() const { - return item_type==DEFINE; + return element_type == DEFINE; } bool is_invar() const { - return item_type==INVAR; + return element_type == INVAR; } bool is_trans() const { - return item_type==TRANS; + return element_type == TRANS; } bool is_init() const { - return item_type==INIT; + return element_type == INIT; } bool is_enum() const { - return item_type == ENUM; + return element_type == ENUM; } bool is_ivar() const { - return item_type == IVAR; + return element_type == IVAR; } bool is_var() const { - return item_type == VAR; + return element_type == VAR; } // for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE @@ -147,129 +150,138 @@ class smv_parse_treet return to_equal_expr(expr); } }; - - typedef std::list item_listt; - item_listt items; + + typedef std::list element_listt; + element_listt elements; void add_assign_current(exprt lhs, exprt rhs) { - items.emplace_back( - itemt::ASSIGN_CURRENT, + elements.emplace_back( + elementt::ASSIGN_CURRENT, binary_exprt{std::move(lhs), ID_equal, std::move(rhs)}, source_locationt::nil()); } void add_assign_init(exprt lhs, exprt rhs) { - items.emplace_back( - itemt::ASSIGN_INIT, + elements.emplace_back( + elementt::ASSIGN_INIT, binary_exprt{std::move(lhs), ID_equal, std::move(rhs)}, source_locationt::nil()); } void add_assign_next(exprt lhs, exprt rhs) { - items.emplace_back( - itemt::ASSIGN_NEXT, + elements.emplace_back( + elementt::ASSIGN_NEXT, binary_exprt{std::move(lhs), ID_equal, std::move(rhs)}, source_locationt::nil()); } void add_invar(exprt expr) { - items.emplace_back( - itemt::INVAR, std::move(expr), source_locationt::nil()); + elements.emplace_back( + elementt::INVAR, std::move(expr), source_locationt::nil()); } void add_define(exprt lhs, exprt rhs) { - items.emplace_back( - itemt::DEFINE, + elements.emplace_back( + elementt::DEFINE, binary_exprt{std::move(lhs), ID_equal, std::move(rhs)}, source_locationt::nil()); } void add_fairness(exprt expr) { - items.emplace_back( - itemt::FAIRNESS, std::move(expr), source_locationt::nil()); + elements.emplace_back( + elementt::FAIRNESS, std::move(expr), source_locationt::nil()); } void add_init(exprt expr) { - items.emplace_back(itemt::INIT, std::move(expr), source_locationt::nil()); + elements.emplace_back( + elementt::INIT, std::move(expr), source_locationt::nil()); } void add_trans(exprt expr) { - items.emplace_back( - itemt::TRANS, std::move(expr), source_locationt::nil()); + elements.emplace_back( + elementt::TRANS, std::move(expr), source_locationt::nil()); } void add_invar(exprt expr, source_locationt location) { - items.emplace_back(itemt::INVAR, std::move(expr), location); + elements.emplace_back(elementt::INVAR, std::move(expr), location); } void add_ctlspec(exprt expr, source_locationt location) { - items.emplace_back(itemt::CTLSPEC, std::move(expr), std::move(location)); + elements.emplace_back( + elementt::CTLSPEC, std::move(expr), std::move(location)); } void add_ctlspec(irep_idt name, exprt expr, source_locationt location) { - items.emplace_back( - itemt::CTLSPEC, name, std::move(expr), std::move(location)); + elements.emplace_back( + elementt::CTLSPEC, name, std::move(expr), std::move(location)); } void add_ltlspec(exprt expr, source_locationt location) { - items.emplace_back(itemt::LTLSPEC, std::move(expr), location); + elements.emplace_back(elementt::LTLSPEC, std::move(expr), location); } void add_ltlspec(irep_idt name, exprt expr, source_locationt location) { - items.emplace_back(itemt::LTLSPEC, name, std::move(expr), location); + elements.emplace_back(elementt::LTLSPEC, name, std::move(expr), location); } void add_define(exprt expr, source_locationt location) { - items.emplace_back(itemt::DEFINE, std::move(expr), std::move(location)); + elements.emplace_back( + elementt::DEFINE, std::move(expr), std::move(location)); } void add_fairness(exprt expr, source_locationt location) { - items.emplace_back(itemt::FAIRNESS, std::move(expr), std::move(location)); + elements.emplace_back( + elementt::FAIRNESS, std::move(expr), std::move(location)); } void add_init(exprt expr, source_locationt location) { - items.emplace_back(itemt::INIT, std::move(expr), std::move(location)); + elements.emplace_back( + elementt::INIT, std::move(expr), std::move(location)); } void add_trans(exprt expr, source_locationt location) { - items.emplace_back(itemt::TRANS, std::move(expr), std::move(location)); + elements.emplace_back( + elementt::TRANS, std::move(expr), std::move(location)); } void add_ivar(exprt expr, typet type) { expr.type() = std::move(type); auto location = expr.source_location(); - items.emplace_back(itemt::IVAR, std::move(expr), std::move(location)); + elements.emplace_back( + elementt::IVAR, std::move(expr), std::move(location)); } void add_var(exprt expr, typet type) { expr.type() = std::move(type); auto location = expr.source_location(); - items.emplace_back(itemt::VAR, std::move(expr), std::move(location)); + elements.emplace_back( + elementt::VAR, std::move(expr), std::move(location)); } void add_enum(exprt expr) { auto location = expr.source_location(); - items.emplace_back(itemt::ENUM, std::move(expr), std::move(location)); + elements.emplace_back( + elementt::ENUM, std::move(expr), std::move(location)); } enum_sett enum_set; @@ -283,7 +295,4 @@ class smv_parse_treet void clear(); }; -#define forall_item_list(it, expr) \ - for(smv_parse_treet::modulet::item_listt::const_iterator it=(expr).begin(); \ - it!=(expr).end(); it++) #endif diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index aeec7fa0b..f0b4520f9 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -61,7 +61,7 @@ class smv_typecheckt:public typecheckt void convert(smv_parse_treet::modulet &); void create_var_symbols( - const smv_parse_treet::modulet::item_listt &, + const smv_parse_treet::modulet::element_listt &, const std::list &module_parameters); void collect_define(const equal_exprt &); @@ -88,8 +88,8 @@ class smv_typecheckt:public typecheckt void check_type(typet &); smv_ranget convert_type(const typet &); - void convert(smv_parse_treet::modulet::itemt &); - void typecheck(smv_parse_treet::modulet::itemt &); + void convert(smv_parse_treet::modulet::elementt &); + void typecheck(smv_parse_treet::modulet::elementt &); void typecheck_expr_rec(exprt &, modet); void convert_expr_to(exprt &, const typet &dest); exprt convert_word_constant(const constant_exprt &); @@ -196,17 +196,18 @@ Function: smv_typecheckt::flatten_hierarchy void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module) { - for(auto &item : smv_module.items) + for(auto &element : smv_module.elements) { - if(item.is_var() && item.expr.type().id() == ID_smv_submodule) + if(element.is_var() && element.expr.type().id() == ID_smv_submodule) { exprt &inst = - static_cast(static_cast(item.expr.type())); + static_cast(static_cast(element.expr.type())); for(auto &op : inst.operands()) convert(op); - auto instance_base_name = to_smv_identifier_expr(item.expr).identifier(); + auto instance_base_name = + to_smv_identifier_expr(element.expr).identifier(); instantiate( smv_module, @@ -2036,70 +2037,72 @@ Function: smv_typecheckt::typecheck \*******************************************************************/ -void smv_typecheckt::typecheck( - smv_parse_treet::modulet::itemt &item) +void smv_typecheckt::typecheck(smv_parse_treet::modulet::elementt &element) { - switch(item.item_type) + switch(element.element_type) { - case smv_parse_treet::modulet::itemt::INIT: - typecheck(item.expr, INIT); - convert_expr_to(item.expr, bool_typet{}); + case smv_parse_treet::modulet::elementt::INIT: + typecheck(element.expr, INIT); + convert_expr_to(element.expr, bool_typet{}); return; - case smv_parse_treet::modulet::itemt::TRANS: - typecheck(item.expr, TRANS); - convert_expr_to(item.expr, bool_typet{}); + case smv_parse_treet::modulet::elementt::TRANS: + typecheck(element.expr, TRANS); + convert_expr_to(element.expr, bool_typet{}); return; - case smv_parse_treet::modulet::itemt::CTLSPEC: - typecheck(item.expr, CTL); - convert_expr_to(item.expr, bool_typet{}); + case smv_parse_treet::modulet::elementt::CTLSPEC: + typecheck(element.expr, CTL); + convert_expr_to(element.expr, bool_typet{}); return; - case smv_parse_treet::modulet::itemt::LTLSPEC: - typecheck(item.expr, LTL); - convert_expr_to(item.expr, bool_typet{}); + case smv_parse_treet::modulet::elementt::LTLSPEC: + typecheck(element.expr, LTL); + convert_expr_to(element.expr, bool_typet{}); return; - case smv_parse_treet::modulet::itemt::INVAR: - typecheck(item.expr, INVAR); - convert_expr_to(item.expr, bool_typet{}); + case smv_parse_treet::modulet::elementt::INVAR: + typecheck(element.expr, INVAR); + convert_expr_to(element.expr, bool_typet{}); return; - case smv_parse_treet::modulet::itemt::FAIRNESS: - typecheck(item.expr, OTHER); - convert_expr_to(item.expr, bool_typet{}); + case smv_parse_treet::modulet::elementt::FAIRNESS: + typecheck(element.expr, OTHER); + convert_expr_to(element.expr, bool_typet{}); return; - case smv_parse_treet::modulet::itemt::ASSIGN_CURRENT: - typecheck(item.equal_expr().lhs(), OTHER); - typecheck(item.equal_expr().rhs(), OTHER); - convert_expr_to(item.equal_expr().rhs(), item.equal_expr().lhs().type()); - item.equal_expr().type() = bool_typet{}; + case smv_parse_treet::modulet::elementt::ASSIGN_CURRENT: + typecheck(element.equal_expr().lhs(), OTHER); + typecheck(element.equal_expr().rhs(), OTHER); + convert_expr_to( + element.equal_expr().rhs(), element.equal_expr().lhs().type()); + element.equal_expr().type() = bool_typet{}; return; - case smv_parse_treet::modulet::itemt::ASSIGN_INIT: - typecheck(item.equal_expr().lhs(), INIT); - typecheck(item.equal_expr().rhs(), INIT); - convert_expr_to(item.equal_expr().rhs(), item.equal_expr().lhs().type()); - item.equal_expr().type() = bool_typet{}; + case smv_parse_treet::modulet::elementt::ASSIGN_INIT: + typecheck(element.equal_expr().lhs(), INIT); + typecheck(element.equal_expr().rhs(), INIT); + convert_expr_to( + element.equal_expr().rhs(), element.equal_expr().lhs().type()); + element.equal_expr().type() = bool_typet{}; return; - case smv_parse_treet::modulet::itemt::ASSIGN_NEXT: - typecheck(item.equal_expr().lhs(), TRANS); - typecheck(item.equal_expr().rhs(), TRANS); - convert_expr_to(item.equal_expr().rhs(), item.equal_expr().lhs().type()); - item.equal_expr().type() = bool_typet{}; + case smv_parse_treet::modulet::elementt::ASSIGN_NEXT: + typecheck(element.equal_expr().lhs(), TRANS); + typecheck(element.equal_expr().rhs(), TRANS); + convert_expr_to( + element.equal_expr().rhs(), element.equal_expr().lhs().type()); + element.equal_expr().type() = bool_typet{}; return; - case smv_parse_treet::modulet::itemt::DEFINE: - typecheck(item.expr, OTHER); - item.equal_expr().type() = bool_typet{}; + case smv_parse_treet::modulet::elementt::DEFINE: + typecheck(element.expr, OTHER); + element.equal_expr().type() = bool_typet{}; return; - case smv_parse_treet::modulet::itemt::ENUM: - case smv_parse_treet::modulet::itemt::IVAR: - case smv_parse_treet::modulet::itemt::VAR: + case smv_parse_treet::modulet::elementt::ENUM: + case smv_parse_treet::modulet::elementt::IVAR: + case smv_parse_treet::modulet::elementt::VAR: return; } } @@ -2116,10 +2119,9 @@ Function: smv_typecheckt::convert \*******************************************************************/ -void smv_typecheckt::convert( - smv_parse_treet::modulet::itemt &item) +void smv_typecheckt::convert(smv_parse_treet::modulet::elementt &element) { - convert(item.expr); + convert(element.expr); } /*******************************************************************\ @@ -2135,7 +2137,7 @@ Function: smv_typecheckt::create_var_symbols \*******************************************************************/ void smv_typecheckt::create_var_symbols( - const smv_parse_treet::modulet::item_listt &items, + const smv_parse_treet::modulet::element_listt &elements, const std::list &module_parameters) { const irep_idt mode = "SMV"; @@ -2149,36 +2151,36 @@ void smv_typecheckt::create_var_symbols( for(const auto ¶meter : module_parameters) parameters.insert(parameter); - for(const auto &item : items) + for(const auto &element : elements) { - if(item.is_var() || item.is_ivar()) + if(element.is_var() || element.is_ivar()) { - irep_idt base_name = to_smv_identifier_expr(item.expr).identifier(); + irep_idt base_name = to_smv_identifier_expr(element.expr).identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); // already used as enum? if(enums.find(base_name) != enums.end()) { - throw errort{}.with_location(item.expr.source_location()) + throw errort{}.with_location(element.expr.source_location()) << "identifier " << base_name << " already used as enum"; } // already used as a parameter? if(parameters.find(base_name) != parameters.end()) { - throw errort{}.with_location(item.expr.source_location()) + throw errort{}.with_location(element.expr.source_location()) << "identifier " << base_name << " already used as a parameter"; } auto symbol_ptr = symbol_table.lookup(identifier); if(symbol_ptr != nullptr) { - throw errort{}.with_location(item.expr.source_location()) + throw errort{}.with_location(element.expr.source_location()) << "variable " << base_name << " already declared, at " << symbol_ptr->location; } - typet type = item.expr.type(); + typet type = element.expr.type(); // check the type check_type(type); @@ -2200,14 +2202,14 @@ void smv_typecheckt::create_var_symbols( symbol.is_state_var = false; symbol.value = nil_exprt{}; - symbol.location = item.expr.source_location(); + symbol.location = element.expr.source_location(); symbol_table.insert(std::move(symbol)); } - else if(item.is_define()) + else if(element.is_define()) { const auto &identifier_expr = - to_smv_identifier_expr(to_equal_expr(item.expr).lhs()); + to_smv_identifier_expr(to_equal_expr(element.expr).lhs()); irep_idt base_name = identifier_expr.identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); @@ -2254,22 +2256,22 @@ void smv_typecheckt::create_var_symbols( symbol_table.insert(std::move(symbol)); } - else if(item.is_enum()) + else if(element.is_enum()) { - irep_idt base_name = to_smv_identifier_expr(item.expr).identifier(); + irep_idt base_name = to_smv_identifier_expr(element.expr).identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); // already used as a parameter? if(parameters.find(base_name) != parameters.end()) { - throw errort{}.with_location(item.expr.source_location()) + throw errort{}.with_location(element.expr.source_location()) << "identifier " << base_name << " already used as a parameter"; } auto symbol_ptr = symbol_table.lookup(identifier); if(symbol_ptr != nullptr) { - throw errort{}.with_location(item.expr.source_location()) + throw errort{}.with_location(element.expr.source_location()) << "enum " << base_name << " already declared, at " << symbol_ptr->location; } @@ -2420,7 +2422,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) define_map.clear(); // variables/defines first, can be used before their declaration - create_var_symbols(smv_module.items, smv_module.parameters); + create_var_symbols(smv_module.elements, smv_module.parameters); // transition relation @@ -2438,41 +2440,43 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) convert_ports(smv_module, module_symbol.type); - // non-variable items - for(auto &item : smv_module.items) - if(!item.is_var() && !item.is_ivar()) - convert(item); + // non-variable elements + for(auto &element : smv_module.elements) + if(!element.is_var() && !element.is_ivar()) + convert(element); flatten_hierarchy(smv_module); // we first need to collect all the defines - for (auto &item : smv_module.items) { - if(item.is_define() || item.is_assign_current()) - collect_define(item.equal_expr()); + for(auto &element : smv_module.elements) + { + if(element.is_define() || element.is_assign_current()) + collect_define(element.equal_expr()); } // now turn them into INVARs convert_defines(trans_invar); // do the rest now: typecheck - for (auto &item : smv_module.items) { - if(!item.is_define() && !item.is_assign_current()) - typecheck(item); + for(auto &element : smv_module.elements) + { + if(!element.is_define() && !element.is_assign_current()) + typecheck(element); } // copy to transition system - for(const auto &item : smv_module.items) + for(const auto &element : smv_module.elements) { - if (item.is_invar()) - trans_invar.push_back(item.expr); - else if (item.is_init()) - trans_init.push_back(item.expr); - else if(item.is_assign_init()) - trans_init.push_back(item.expr); - else if(item.is_assign_next()) - trans_trans.push_back(item.expr); - else if (item.is_trans()) - trans_trans.push_back(item.expr); + if(element.is_invar()) + trans_invar.push_back(element.expr); + else if(element.is_init()) + trans_init.push_back(element.expr); + else if(element.is_assign_init()) + trans_init.push_back(element.expr); + else if(element.is_assign_next()) + trans_trans.push_back(element.expr); + else if(element.is_trans()) + trans_trans.push_back(element.expr); } module_symbol.value = @@ -2490,14 +2494,14 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) { unsigned nr=1; - forall_item_list(it, smv_module.items) + for(auto &element : smv_module.elements) { - if(it->is_ctlspec() || it->is_ltlspec()) + if(element.is_ctlspec() || element.is_ltlspec()) { symbolt spec_symbol; - if(it->name.has_value()) - spec_symbol.base_name = it->name.value(); + if(element.name.has_value()) + spec_symbol.base_name = element.name.value(); else spec_symbol.base_name = "spec" + std::to_string(nr++); @@ -2507,9 +2511,9 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) spec_symbol.type = bool_typet(); spec_symbol.is_property = true; spec_symbol.mode = "SMV"; - spec_symbol.value = it->expr; - spec_symbol.location = it->location; - spec_symbol.location.set_comment(to_string(it->expr)); + spec_symbol.value = element.expr; + spec_symbol.location = element.location; + spec_symbol.location.set_comment(to_string(element.expr)); if(smv_module.name == "smv::main") spec_symbol.pretty_name = spec_symbol.base_name;