diff --git a/regression/smv/modules/trace1.desc b/regression/smv/modules/trace1.desc index dc6c74754..70d04346d 100644 --- a/regression/smv/modules/trace1.desc +++ b/regression/smv/modules/trace1.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE trace1.smv --numbered-trace ^\[.*\] AG \!a\.c\.d: REFUTED$ @@ -16,6 +16,4 @@ trace1.smv ^a@1 = .*$ ^b@1 = .*$ ^a.c@1 = .*$ -^b.d@1 = .*$ -- -The trace contains entries for the module instances. diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 0d4509bfd..3478822e9 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -38,7 +38,7 @@ IREP_ID_ONE(smv_setin) IREP_ID_ONE(smv_setnotin) IREP_ID_ONE(smv_signed_cast) IREP_ID_ONE(smv_sizeof) -IREP_ID_ONE(smv_submodule) +IREP_ID_ONE(smv_module_instance) IREP_ID_ONE(smv_swconst) IREP_ID_ONE(smv_union) IREP_ID_ONE(smv_unsigned_cast) diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp index 4039d552a..a45ee3f9f 100644 --- a/src/smvlang/expr2smv.cpp +++ b/src/smvlang/expr2smv.cpp @@ -1058,9 +1058,9 @@ std::string type2smv(const typet &type, const namespacet &ns) { return "set"; } - else if(type.id() == ID_smv_submodule) + else if(type.id() == ID_smv_module_instance) { - auto code = id2string(to_smv_submodule_type(type).identifier()); + auto code = id2string(to_smv_module_instance_type(type).identifier()); const exprt &e=(exprt &)type; if(e.has_operands()) { diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index 6ab873594..443a32a2d 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -631,14 +631,14 @@ simple_type_specifier: module_type_specifier: module_name { - init($$, ID_smv_submodule); - to_smv_submodule_type(stack_type($$)).identifier( + init($$, ID_smv_module_instance); + to_smv_module_instance_type(stack_type($$)).identifier( smv_module_symbol(stack_expr($1).id_string())); } | module_name '(' parameter_list ')' { - init($$, ID_smv_submodule); - to_smv_submodule_type(stack_type($$)).identifier( + init($$, ID_smv_module_instance); + to_smv_module_instance_type(stack_type($$)).identifier( smv_module_symbol(stack_expr($1).id_string())); stack_expr($$).operands().swap(stack_expr($3).operands()); } diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp index a9b23f8c6..4ba5f722f 100644 --- a/src/smvlang/smv_language.cpp +++ b/src/smvlang/smv_language.cpp @@ -70,9 +70,9 @@ void smv_languaget::dependencies( const smv_parse_treet::modulet &smv_module = *m_it->second; 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(element.expr.type()).identifier())); + if(element.is_var() && element.expr.type().id() == ID_smv_module_instance) + module_set.insert(id2string( + to_smv_module_instance_type(element.expr.type()).identifier())); } /*******************************************************************\ diff --git a/src/smvlang/smv_parse_tree.cpp b/src/smvlang/smv_parse_tree.cpp index 2b6747311..c2de28e46 100644 --- a/src/smvlang/smv_parse_tree.cpp +++ b/src/smvlang/smv_parse_tree.cpp @@ -122,7 +122,7 @@ void smv_parse_treet::show(std::ostream &out) const out << " VARIABLES:" << std::endl; for(auto &element : module.elements) - if(element.is_var() && element.expr.type().id() != ID_smv_submodule) + if(element.is_var() && element.expr.type().id() != ID_smv_module_instance) { symbol_tablet symbol_table; namespacet ns{symbol_table}; @@ -136,7 +136,7 @@ void smv_parse_treet::show(std::ostream &out) const out << " SUBMODULES:" << std::endl; for(auto &element : module.elements) - if(element.is_var() && element.expr.type().id() == ID_smv_submodule) + if(element.is_var() && element.expr.type().id() == ID_smv_module_instance) { symbol_tablet symbol_table; namespacet ns(symbol_table); diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 5bb2166ff..d996f3f37 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -203,7 +203,7 @@ void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module) { auto &element = *element_it; - if(element.is_var() && element.expr.type().id() == ID_smv_submodule) + if(element.is_var() && element.expr.type().id() == ID_smv_module_instance) { exprt &inst = static_cast(static_cast(element.expr.type())); @@ -2181,7 +2181,7 @@ void smv_typecheckt::create_var_symbols( else symbol.pretty_name = strip_smv_prefix(symbol.name); - if(symbol.type.id() == ID_smv_submodule) + if(symbol.type.id() == ID_smv_module_instance) symbol.is_input = false; else symbol.is_input = true; diff --git a/src/smvlang/smv_types.h b/src/smvlang/smv_types.h index 594d68e24..8b7574823 100644 --- a/src/smvlang/smv_types.h +++ b/src/smvlang/smv_types.h @@ -72,10 +72,11 @@ inline smv_enumeration_typet &to_smv_enumeration_type(typet &type) } /// The type used for VAR declarations that are in fact module instantiations -class smv_submodule_typet : public typet +class smv_module_instance_typet : public typet { public: - explicit smv_submodule_typet(irep_idt _identifier) : typet{ID_smv_submodule} + explicit smv_module_instance_typet(irep_idt _identifier) + : typet{ID_smv_module_instance} { identifier(_identifier); } @@ -91,26 +92,27 @@ class smv_submodule_typet : public typet } }; -/*! \brief Cast a generic typet to a \ref smv_submodule_typet +/*! \brief Cast a generic typet to a \ref smv_module_instance_typet * * This is an unchecked conversion. \a type must be known to be \ref - * smv_submodule_typet. + * smv_module_instance_typet. * * \param type Source type - * \return Object of type \ref smv_submodule_typet + * \return Object of type \ref smv_module_instance_typet * * \ingroup gr_std_types */ -inline const smv_submodule_typet &to_smv_submodule_type(const typet &type) +inline const smv_module_instance_typet & +to_smv_module_instance_type(const typet &type) { - PRECONDITION(type.id() == ID_smv_submodule); - return static_cast(type); + PRECONDITION(type.id() == ID_smv_module_instance); + return static_cast(type); } -inline smv_submodule_typet &to_smv_submodule_type(typet &type) +inline smv_module_instance_typet &to_smv_module_instance_type(typet &type) { - PRECONDITION(type.id() == ID_smv_submodule); - return static_cast(type); + PRECONDITION(type.id() == ID_smv_module_instance); + return static_cast(type); } #endif // CPROVER_SMV_TYPES_H diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp index c7b1c3901..48f2246b0 100644 --- a/src/trans-netlist/trans_to_netlist.cpp +++ b/src/trans-netlist/trans_to_netlist.cpp @@ -225,7 +225,8 @@ void convert_trans_to_netlistt::map_vars( } else if( symbol.type.id() == ID_module || symbol.type.id() == ID_module_instance || - symbol.type.id() == ID_primitive_module_instance) + symbol.type.id() == ID_primitive_module_instance || + symbol.type.id() == ID_smv_module_instance) { return; // ignore modules } diff --git a/src/trans-word-level/trans_trace_word_level.cpp b/src/trans-word-level/trans_trace_word_level.cpp index 57fb2a0fc..14280657a 100644 --- a/src/trans-word-level/trans_trace_word_level.cpp +++ b/src/trans-word-level/trans_trace_word_level.cpp @@ -53,10 +53,11 @@ trans_tracet compute_trans_trace( { const symbolt &symbol=ns.lookup(it->second); - if(!symbol.is_type && - !symbol.is_property && - symbol.type.id()!=ID_module && - symbol.type.id()!=ID_module_instance) + if( + !symbol.is_type && !symbol.is_property && + symbol.type.id() != ID_module && + symbol.type.id() != ID_module_instance && + symbol.type.id() != ID_smv_module_instance) { if(symbol.is_macro) {