Make index in renamings be of std::size_t type

This avoids some conversions, in particular when assigning from the
return value of fresh_l2_name_provider.

Author: romainbrenguier

src/goto-symex/goto_state.cpp

@@ -35,8 +35,8 @@ std::size_t goto_statet::increase_generation(
 
   if(const auto r_opt = level2.current_names.find(l1_identifier))
   {
-    std::pair<ssa_exprt, unsigned> copy = r_opt->get();
-    copy.second = narrow<unsigned>(n);
+    std::pair<ssa_exprt, std::size_t> copy = r_opt->get();
+    copy.second = n;
     level2.current_names.replace(l1_identifier, std::move(copy));
   }
   else

src/goto-symex/renamed.h

@@ -50,7 +50,7 @@ class renamedt : private underlyingt
   };
 
   friend renamedt<ssa_exprt, L0>
-  symex_level0(ssa_exprt, const namespacet &, unsigned);
+  symex_level0(ssa_exprt, const namespacet &, std::size_t);
   friend struct symex_level1t;
   friend struct symex_level2t;
   friend class goto_symex_statet;

src/goto-symex/renaming_level.cpp

@@ -31,7 +31,7 @@ void get_variables(
 }
 
 renamedt<ssa_exprt, L0>
-symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr)
+symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
 {
   // already renamed?
   if(!ssa_expr.get_level_0().empty())
@@ -56,21 +56,21 @@ symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr)
   return renamedt<ssa_exprt, L0>{ssa_expr};
 }
 
-void symex_level1t::insert(const renamedt<ssa_exprt, L0> &ssa, unsigned index)
+void symex_level1t::insert(const renamedt<ssa_exprt, L0> &ssa, std::size_t index)
 {
   current_names.insert(
     ssa.get().get_identifier(), std::make_pair(ssa.get(), index));
 }
 
-optionalt<std::pair<ssa_exprt, unsigned>> symex_level1t::insert_or_replace(
+optionalt<std::pair<ssa_exprt, std::size_t>> symex_level1t::insert_or_replace(
   const renamedt<ssa_exprt, L0> &ssa,
-  unsigned index)
+  std::size_t index)
 {
   const irep_idt &identifier = ssa.get().get_identifier();
   const auto old_value = current_names.find(identifier);
   if(old_value)
   {
-    std::pair<ssa_exprt, unsigned> result = *old_value;
+    std::pair<ssa_exprt, std::size_t> result = *old_value;
     current_names.replace(identifier, std::make_pair(ssa.get(), index));
     return result;
   }

src/goto-symex/renaming_level.h

@@ -29,7 +29,7 @@ Author: Romain Brenguier, [email protected]
 /// This is extended by the different symex_level structures which are used
 /// during symex to ensure static single assignment (SSA) form.
 using symex_renaming_levelt =
-  sharing_mapt<irep_idt, std::pair<ssa_exprt, unsigned>>;
+  sharing_mapt<irep_idt, std::pair<ssa_exprt, std::size_t>>;
 
 /// Add the \c ssa_exprt of current_names to vars
 DEPRECATED(SINCE(2019, 6, 5, "Unused"))
@@ -44,21 +44,21 @@ void get_variables(
 /// a guard, a shared variable or a function. \p ns is queried to decide
 /// whether we are in one of these cases.
 renamedt<ssa_exprt, L0>
-symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr);
+symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr);
 
 /// Functor to set the level 1 renaming of SSA expressions.
 /// Level 1 corresponds to function frames.
 /// This is to preserve locality in case of recursion
 struct symex_level1t
 {
   /// Assume \p ssa is not already known
-  void insert(const renamedt<ssa_exprt, L0> &ssa, unsigned index);
+  void insert(const renamedt<ssa_exprt, L0> &ssa, std::size_t index);
 
   /// Set the index for \p ssa to index.
   /// \return if an index for \p ssa was already know, returns it's previous
   ///   value.
-  optionalt<std::pair<ssa_exprt, unsigned>>
-  insert_or_replace(const renamedt<ssa_exprt, L0> &ssa, unsigned index);
+  optionalt<std::pair<ssa_exprt, std::size_t>>
+  insert_or_replace(const renamedt<ssa_exprt, L0> &ssa, std::size_t index);
 
   /// \return true if \p ssa has an associated index
   bool has(const renamedt<ssa_exprt, L0> &ssa) const;

src/util/ssa_expr.cpp

@@ -178,19 +178,19 @@ const irep_idt ssa_exprt::get_l1_object_identifier() const
 #endif
 }
 
-void ssa_exprt::set_level_0(unsigned i)
+void ssa_exprt::set_level_0(std::size_t i)
 {
   set(ID_L0, i);
   ::update_identifier(*this);
 }
 
-void ssa_exprt::set_level_1(unsigned i)
+void ssa_exprt::set_level_1(std::size_t i)
 {
   set(ID_L1, i);
   ::update_identifier(*this);
 }
 
-void ssa_exprt::set_level_2(unsigned i)
+void ssa_exprt::set_level_2(std::size_t i)
 {
   set(ID_L2, i);
   ::update_identifier(*this);

src/util/ssa_expr.h

@@ -52,11 +52,11 @@ class ssa_exprt:public symbol_exprt
     return o.get_identifier();
   }
 
-  void set_level_0(unsigned i);
+  void set_level_0(std::size_t i);
 
-  void set_level_1(unsigned i);
+  void set_level_1(std::size_t i);
 
-  void set_level_2(unsigned i);
+  void set_level_2(std::size_t i);
 
   void remove_level_2();