SMV: rename smv_submodule to smv_module_instance

The NuSMV 2.7 manual uses the term "module instance" -- hence, this renames
the ID used.

Author: kroening

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)

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())
     {

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());
            }

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()));
 }
 
 /*******************************************************************\

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);

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<exprt &>(static_cast<irept &>(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;

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<const smv_submodule_typet &>(type);
+  PRECONDITION(type.id() == ID_smv_module_instance);
+  return static_cast<const smv_module_instance_typet &>(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<smv_submodule_typet &>(type);
+  PRECONDITION(type.id() == ID_smv_module_instance);
+  return static_cast<smv_module_instance_typet &>(type);
 }
 
 #endif // CPROVER_SMV_TYPES_H