Change 'pc' to 'progam_counter'

This is likely an acronym that is well-known if you're knowledgable of the subject area, but only in a few places is it referred by it's full name, and it confused me until I found that comment.

Author: JohnDumbell

src/cbmc/all_properties.cpp

@@ -83,7 +83,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
       if(property_id.empty())
         continue;
 
-      if(it->source.pc->is_goto())
+      if(it->source.program_counter->is_goto())
       {
         // goto may yield an unwinding assertion
         goal_map[property_id].description = it->comment;

src/cbmc/bmc_cover.cpp

@@ -224,11 +224,11 @@ bool bmc_covert::operator()()
   {
     if(it->is_assert())
     {
-      PRECONDITION(it->source.pc->is_assert());
+      PRECONDITION(it->source.program_counter->is_assert());
       const and_exprt c(
         literal_exprt(it->guard_literal), literal_exprt(!it->cond_literal));
       literalt l_c=solver.convert(c);
-      goal_map[id(it->source.pc)].add_instance(it, l_c);
+      goal_map[id(it->source.program_counter)].add_instance(it, l_c);
     }
   }
 

src/cbmc/fault_localization.cpp

@@ -55,7 +55,7 @@ void fault_localizationt::collect_guards(lpointst &lpoints)
     {
       if(!it->guard_literal.is_constant())
       {
-        lpoints[it->guard_literal].target=it->source.pc;
+        lpoints[it->guard_literal].target=it->source.program_counter;
         lpoints[it->guard_literal].score=0;
       }
     }
@@ -148,7 +148,7 @@ void fault_localizationt::run(irep_idt goal_id)
   PRECONDITION(failed != bmc.equation.SSA_steps.end());
 
   if(goal_id==ID_nil)
-    goal_id=failed->source.pc->source_location.get_property_id();
+    goal_id=failed->source.program_counter->source_location.get_property_id();
   lpointst &lpoints=lpoints_map[goal_id];
 
   // collect lpoints
@@ -171,7 +171,7 @@ void fault_localizationt::run(irep_idt goal_id)
 void fault_localizationt::report(irep_idt goal_id)
 {
   if(goal_id==ID_nil)
-    goal_id=failed->source.pc->source_location.get_property_id();
+    goal_id=failed->source.program_counter->source_location.get_property_id();
 
   lpointst &lpoints=lpoints_map[goal_id];
 
@@ -203,7 +203,7 @@ xmlt fault_localizationt::report_xml(irep_idt goal_id)
   xml_diagnosis.new_element("method").data="linear fault localization";
 
   if(goal_id==ID_nil)
-    goal_id=failed->source.pc->source_location.get_property_id();
+    goal_id=failed->source.program_counter->source_location.get_property_id();
 
   xml_diagnosis.set_attribute("property", id2string(goal_id));
 

src/goto-checker/bmc_util.cpp

@@ -245,7 +245,8 @@ std::vector<irep_idt> update_properties_status_from_symex_target_equation(
     const auto status = step.cond_expr.is_true() ? property_statust::PASS
                                                  : property_statust::UNKNOWN;
     auto emplace_result = properties.emplace(
-      property_id, property_infot{step.source.pc, step.comment, status});
+      property_id,
+      property_infot{step.source.program_counter, step.comment, status});
 
     if(emplace_result.second)
     {

src/goto-checker/symex_bmc.cpp

@@ -35,7 +35,8 @@ void symex_bmct::symex_step(
   const get_goto_functiont &get_goto_function,
   statet &state)
 {
-  const source_locationt &source_location = state.source.pc->source_location;
+  const source_locationt &source_location =
+    state.source.program_counter->source_location;
 
   if(!source_location.is_nil() && last_source_location != source_location)
   {
@@ -45,18 +46,19 @@ void symex_bmct::symex_step(
     last_source_location = source_location;
   }
 
-  const goto_programt::const_targett cur_pc = state.source.pc;
+  const goto_programt::const_targett cur_pc = state.source.program_counter;
   const guardt cur_guard = state.guard;
 
   if(
-    !state.guard.is_false() && state.source.pc->is_assume() &&
-    simplify_expr(state.source.pc->guard, ns).is_false())
+    !state.guard.is_false() && state.source.program_counter->is_assume() &&
+    simplify_expr(state.source.program_counter->guard, ns).is_false())
   {
     log.statistics() << "aborting path on assume(false) at "
-                     << state.source.pc->source_location << " thread "
-                     << state.source.thread_nr;
+                     << state.source.program_counter->source_location
+                     << " thread " << state.source.thread_nr;
 
-    const irep_idt &c = state.source.pc->source_location.get_comment();
+    const irep_idt &c =
+      state.source.program_counter->source_location.get_comment();
     if(!c.empty())
       log.statistics() << ": " << c;
 
@@ -67,7 +69,7 @@ void symex_bmct::symex_step(
 
   if(
     record_coverage &&
-    // avoid an invalid iterator in state.source.pc
+    // avoid an invalid iterator in state.source.program_counter
     (!cur_pc->is_end_function() ||
      state.source.function_id != goto_functionst::entry_point()))
   {
@@ -78,19 +80,21 @@ void symex_bmct::symex_step(
     // transition from the goto instruction to its target to make
     // sure the goto is considered covered
     if(
-      cur_pc->is_goto() && cur_pc->get_target() != state.source.pc &&
+      cur_pc->is_goto() &&
+      cur_pc->get_target() != state.source.program_counter &&
       cur_pc->guard.is_true())
       symex_coverage.covered(cur_pc, cur_pc->get_target());
     else if(!state.guard.is_false())
-      symex_coverage.covered(cur_pc, state.source.pc);
+      symex_coverage.covered(cur_pc, state.source.program_counter);
   }
 }
 
 void symex_bmct::merge_goto(
   const statet::goto_statet &goto_state,
   statet &state)
 {
-  const goto_programt::const_targett prev_pc = goto_state.source.pc;
+  const goto_programt::const_targett prev_pc =
+    goto_state.source.program_counter;
   const guardt prev_guard = goto_state.guard;
 
   goto_symext::merge_goto(goto_state, state);
@@ -102,23 +106,24 @@ void symex_bmct::merge_goto(
     !prev_guard.is_false() && !state.guard.is_false() &&
     // branches only, no single-successor goto
     !prev_pc->guard.is_true())
-    symex_coverage.covered(prev_pc, state.source.pc);
+    symex_coverage.covered(prev_pc, state.source.program_counter);
 }
 
 bool symex_bmct::should_stop_unwind(
   const symex_targett::sourcet &source,
   const goto_symex_statet::call_stackt &context,
   unsigned unwind)
 {
-  const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc);
+  const irep_idt id =
+    goto_programt::loop_id(source.function_id, *source.program_counter);
 
   tvt abort_unwind_decision;
   unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
 
   for(auto handler : loop_unwind_handlers)
   {
-    abort_unwind_decision =
-      handler(context, source.pc->loop_number, unwind, this_loop_limit);
+    abort_unwind_decision = handler(
+      context, source.program_counter->loop_number, unwind, this_loop_limit);
     if(abort_unwind_decision.is_known())
       break;
   }
@@ -145,8 +150,8 @@ bool symex_bmct::should_stop_unwind(
   if(this_loop_limit != std::numeric_limits<unsigned>::max())
     log.statistics() << " (" << this_loop_limit << " max)";
 
-  log.statistics() << " " << source.pc->source_location << " thread "
-                   << source.thread_nr << log.eom;
+  log.statistics() << " " << source.program_counter->source_location
+                   << " thread " << source.thread_nr << log.eom;
 
   return abort;
 }

src/goto-programs/graphml_witness.cpp

@@ -374,11 +374,12 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
       it!=equation.SSA_steps.end();
       it++, step_nr++) // we cannot replace this by a ranged for
   {
-    const source_locationt &source_location=it->source.pc->source_location;
+    const source_locationt &source_location =
+      it->source.program_counter->source_location;
 
     if(it->hidden ||
        (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
-       (it->is_goto() && it->source.pc->guard.is_true()) ||
+       (it->is_goto() && it->source.program_counter->guard.is_true()) ||
        source_location.is_nil() ||
        source_location.is_built_in() ||
        source_location.get_line().empty())
@@ -391,10 +392,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
     // skip declarations followed by an immediate assignment
     symex_target_equationt::SSA_stepst::const_iterator next=it;
     ++next;
-    if(next!=equation.SSA_steps.end() &&
-       next->is_assignment() &&
-       it->ssa_full_lhs==next->ssa_full_lhs &&
-       it->source.pc->source_location==next->source.pc->source_location)
+    if(
+      next != equation.SSA_steps.end() && next->is_assignment() &&
+      it->ssa_full_lhs == next->ssa_full_lhs &&
+      it->source.program_counter->source_location ==
+        next->source.program_counter->source_location)
     {
       step_to_node[step_nr]=sink;
 
@@ -403,7 +405,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
 
     const graphmlt::node_indext node=graphml.add_node();
     graphml[node].node_name=
-      std::to_string(it->source.pc->location_number)+"."+
+      std::to_string(it->source.program_counter->location_number)+"."+
       std::to_string(step_nr);
     graphml[node].file=source_location.get_file();
     graphml[node].line=source_location.get_line();
@@ -433,8 +435,9 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
     symex_target_equationt::SSA_stepst::const_iterator next=it;
     std::size_t next_step_nr=step_nr;
     for(++next, ++next_step_nr;
-        next!=equation.SSA_steps.end() &&
-        (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
+        next != equation.SSA_steps.end() &&
+        (step_to_node[next_step_nr] == sink ||
+         it->source.program_counter == next->source.program_counter);
         ++next, ++next_step_nr)
     {
       // advance
@@ -475,11 +478,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
           graphml[to].has_invariant=true;
           code_assignt assign(it->ssa_full_lhs, it->ssa_rhs);
           graphml[to].invariant=convert_assign_rec(identifier, assign);
-          graphml[to].invariant_scope=
-            id2string(it->source.pc->source_location.get_function());
+          graphml[to].invariant_scope = id2string(
+            it->source.program_counter->source_location.get_function());
         }
         else if(it->is_goto() &&
-                it->source.pc->is_goto())
+                it->source.program_counter->is_goto())
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");

src/goto-symex/build_goto_trace.cpp

@@ -144,7 +144,7 @@ void update_internal_field(
   // set internal field to CPROVER functions (e.g., __CPROVER_initialize)
   if(SSA_step.is_function_call())
   {
-    if(SSA_step.source.pc->source_location.as_string().empty())
+    if(SSA_step.source.program_counter->source_location.as_string().empty())
       goto_trace_step.internal=true;
   }
 
@@ -161,7 +161,7 @@ void update_internal_field(
     // "__CPROVER_*" function calls in __CPROVER_start are already marked as
     // internal. Don't mark any other function calls (i.e. "main"), function
     // arguments or any other parts of a code_function_callt as internal.
-    if(SSA_step.source.pc->code.get_statement()!=ID_function_call)
+    if(SSA_step.source.program_counter->code.get_statement()!=ID_function_call)
       goto_trace_step.internal=true;
   }
 }
@@ -303,7 +303,7 @@ void build_goto_trace(
       goto_trace_step.step_nr = ++step_nr;
 
       goto_trace_step.thread_nr = SSA_step.source.thread_nr;
-      goto_trace_step.pc = SSA_step.source.pc;
+      goto_trace_step.pc = SSA_step.source.program_counter;
       goto_trace_step.function_id = SSA_step.source.function_id;
       if(SSA_step.is_assert())
       {

src/goto-symex/equation_conversion_exceptions.h

@@ -28,7 +28,8 @@ class equation_conversion_exceptiont : public std::runtime_error
   {
     std::ostringstream error_msg;
     error_msg << runtime_error::what();
-    error_msg << "\nSource GOTO statement: " << format(step.source.pc->code);
+    error_msg << "\nSource GOTO statement: "
+              << format(step.source.program_counter->code);
     error_msg << "\nStep:\n";
     step.output(error_msg);
     error_message = error_msg.str();

src/goto-symex/goto_symex_state.cpp

@@ -817,7 +817,8 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
     return;
   }
 
-  out << source.function_id << " " << source.pc->location_number << "\n";
+  out << source.function_id << " " << source.program_counter->location_number
+      << "\n";
 
   for(auto stackit = threads[source.thread_nr].call_stack.rbegin(),
            stackend = threads[source.thread_nr].call_stack.rend();
@@ -828,7 +829,7 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
     if(frame.calling_location.is_set)
     {
       out << frame.calling_location.function_id << " "
-          << frame.calling_location.pc->location_number << "\n";
+          << frame.calling_location.program_counter->location_number << "\n";
     }
   }
 }

src/goto-symex/memory_model_tso.cpp

@@ -106,7 +106,7 @@ void memory_model_tsot::program_order(
 
         if((*e_it2)->is_memory_barrier())
         {
-          const codet &code = (*e_it2)->source.pc->code;
+          const codet &code = (*e_it2)->source.program_counter->code;
 
           if((*e_it)->is_shared_read() &&
              !code.get_bool(ID_RRfence) &&

src/goto-symex/show_program.cpp

@@ -58,8 +58,9 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation)
 
   for(const auto &step : equation.SSA_steps)
   {
-    std::cout << "// " << step.source.pc->location_number << " ";
-    std::cout << step.source.pc->source_location.as_string() << "\n";
+    std::cout << "// " << step.source.program_counter->location_number << " ";
+    std::cout << step.source.program_counter->source_location.as_string()
+              << "\n";
 
     if(step.is_assignment())
       show_step(ns, step, "", count);

src/goto-symex/show_vcc.cpp

@@ -43,8 +43,8 @@ void show_vcc_plain(
     else
       out << '\n';
 
-    if(s_it->source.pc->source_location.is_not_nil())
-      out << s_it->source.pc->source_location << '\n';
+    if(s_it->source.program_counter->source_location.is_not_nil())
+      out << s_it->source.program_counter->source_location << '\n';
 
     if(s_it->comment != "")
       out << s_it->comment << '\n';
@@ -120,7 +120,8 @@ void show_vcc_json(
     // vcc object
     json_objectt &object = json_vccs.push_back(jsont()).make_object();
 
-    const source_locationt &source_location = s_it->source.pc->source_location;
+    const source_locationt &source_location =
+      s_it->source.program_counter->source_location;
     if(source_location.is_not_nil())
       object["sourceLocation"] = json(source_location);
 

src/goto-symex/symex_assign.cpp

@@ -71,7 +71,7 @@ void goto_symext::symex_assign(
       assignment_type=symex_targett::assignment_typet::HIDDEN;
 
     // We hide if we are executing a hidden instruction.
-    if(state.source.pc->source_location.get_hide())
+    if(state.source.program_counter->source_location.get_hide())
       assignment_type=symex_targett::assignment_typet::HIDDEN;
 
     guardt guard{true_exprt{}}; // NOT the state guard!

src/goto-symex/symex_atomic_section.cpp

@@ -21,7 +21,7 @@ void goto_symext::symex_atomic_begin(statet &state)
   if(state.atomic_section_id != 0)
     throw incorrect_goto_program_exceptiont(
       "we don't support nesting of atomic sections",
-      state.source.pc->source_location);
+      state.source.program_counter->source_location);
 
   state.atomic_section_id=++atomic_section_counter;
   state.read_in_atomic_section.clear();
@@ -40,7 +40,7 @@ void goto_symext::symex_atomic_end(statet &state)
 
   if(state.atomic_section_id == 0)
     throw incorrect_goto_program_exceptiont(
-      "ATOMIC_END unmatched", state.source.pc->source_location);
+      "ATOMIC_END unmatched", state.source.program_counter->source_location);
 
   const unsigned atomic_section_id=state.atomic_section_id;
   state.atomic_section_id=0;

src/goto-symex/symex_catch.cpp

@@ -18,7 +18,7 @@ void goto_symext::symex_catch(statet &)
   // there are two variants: 'push' and 'pop'
 
   #if 0
-  const goto_programt::instructiont &instruction=*state.source.pc;
+  const goto_programt::instructiont &instruction=*state.source.program_counter;
 
   if(instruction.targets.empty()) // pop
   {

src/goto-symex/symex_dead.cpp

@@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
 
 void goto_symext::symex_dead(statet &state)
 {
-  const goto_programt::instructiont &instruction=*state.source.pc;
+  const goto_programt::instructiont &instruction=*state.source.program_counter;
 
   const code_deadt &code = to_code_dead(instruction.code);