Removed redundant get_pc() (there is pc())

Author: tautschnig

src/path-symex/path_symex_state.cpp

@@ -41,12 +41,6 @@ path_symex_statet initial_state(
   return s;
 }
 
-loc_reft path_symex_statet::get_pc() const
-{
-  assert(current_thread<threads.size());
-  return threads[current_thread].pc;
-}
-
 void path_symex_statet::output(const threadt &thread, std::ostream &out) const
 {
   out << "  PC: " << thread.pc << '\n';

src/path-symex/path_symex_state.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
 #define CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
 
+#include <util/invariant.h>
+
 #include "locs.h"
 #include "var_map.h"
 #include "path_symex_history.h"
@@ -111,11 +113,9 @@ struct path_symex_statet
     current_thread=_thread;
   }
 
-  loc_reft get_pc() const;
-
   goto_programt::const_targett get_instruction() const
   {
-    return locs[get_pc()].target;
+    return locs[pc()].target;
   }
 
   bool is_executable() const
@@ -145,6 +145,7 @@ struct path_symex_statet
 
   loc_reft pc() const
   {
+    PRECONDITION(current_thread<threads.size());
     return threads[current_thread].pc;
   }
 

src/symex/path_search.cpp

@@ -68,9 +68,9 @@ path_searcht::resultt path_searcht::operator()(
       statet &state=tmp_queue.front();
 
       // record we have seen it
-      loc_data[state.get_pc().loc_number].visited=true;
+      loc_data[state.pc().loc_number].visited=true;
 
-      debug() << "Loc: #" << state.get_pc().loc_number
+      debug() << "Loc: #" << state.pc().loc_number
               << ", queue: " << queue.size()
               << ", depth: " << state.get_depth();
       for(const auto &s : queue)