Only use source_locationt's get_function() for user output

A source location is a place in a text file, and the function information stored
in there need not coincide with the name we use in the goto model.

Part 2: Wherever we generate fresh symbols or function-specific objects we
should use the actual function name to ensure fewer name collisions (for fresh
symbols) or actually unique objects.

Author: tautschnig

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -206,7 +206,12 @@ symbol_exprt c_nondet_symbol_factory(
   bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
   CHECK_RETURN(!moving_symbol_failed);
 
-  symbol_factoryt state(symbol_table, loc, object_factory_parameters, lifetime);
+  symbol_factoryt state(
+    symbol_table,
+    loc,
+    goto_functionst::entry_point(),
+    object_factory_parameters,
+    lifetime);
 
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);

src/ansi-c/c_nondet_symbol_factory.h

@@ -38,13 +38,14 @@ class symbol_factoryt
   symbol_factoryt(
     symbol_tablet &_symbol_table,
     const source_locationt &loc,
+    const irep_idt &name_prefix,
     const c_object_factory_parameterst &object_factory_params,
     const lifetimet lifetime)
     : symbol_table(_symbol_table),
       loc(loc),
       ns(_symbol_table),
       object_factory_params(object_factory_params),
-      allocate_objects(ID_C, loc, loc.get_function(), symbol_table),
+      allocate_objects(ID_C, loc, name_prefix, symbol_table),
       lifetime(lifetime)
   {
   }

src/goto-instrument/code_contracts.cpp

@@ -61,7 +61,9 @@ class code_contractst
 
   const symbolt &new_tmp_symbol(
     const typet &type,
-    const source_locationt &source_location);
+    const source_locationt &source_location,
+    const irep_idt &function_id,
+    const irep_idt &mode);
 };
 
 static void check_apply_invariants(
@@ -248,14 +250,16 @@ void code_contractst::code_contracts(
 
 const symbolt &code_contractst::new_tmp_symbol(
   const typet &type,
-  const source_locationt &source_location)
+  const source_locationt &source_location,
+  const irep_idt &function_id,
+  const irep_idt &mode)
 {
   return get_fresh_aux_symbol(
     type,
-    id2string(source_location.get_function()),
+    id2string(function_id) + "::tmp_cc",
     "tmp_cc",
     source_location,
-    irep_idt(),
+    mode,
     symbol_table);
 }
 
@@ -301,7 +305,8 @@ void code_contractst::add_contract_check(
   g->source_location=skip->source_location;
 
   // prepare function call including all declarations
-  code_function_callt call(ns.lookup(function).symbol_expr());
+  const symbolt &function_symbol = ns.lookup(function);
+  code_function_callt call(function_symbol.symbol_expr());
   replace_symbolt replace;
 
   // decl ret
@@ -310,9 +315,12 @@ void code_contractst::add_contract_check(
     goto_programt::targett d=check.add_instruction(DECL);
     d->source_location=skip->source_location;
 
-    symbol_exprt r=
-      new_tmp_symbol(gf.type.return_type(),
-                     d->source_location).symbol_expr();
+    symbol_exprt r = new_tmp_symbol(
+                       gf.type.return_type(),
+                       d->source_location,
+                       function,
+                       function_symbol.mode)
+                       .symbol_expr();
     d->code=code_declt(r);
 
     call.lhs()=r;
@@ -330,9 +338,10 @@ void code_contractst::add_contract_check(
     goto_programt::targett d=check.add_instruction(DECL);
     d->source_location=skip->source_location;
 
-    symbol_exprt p=
-      new_tmp_symbol(p_it->type(),
-                     d->source_location).symbol_expr();
+    symbol_exprt p =
+      new_tmp_symbol(
+        p_it->type(), d->source_location, function, function_symbol.mode)
+        .symbol_expr();
     d->code=code_declt(p);
 
     call.arguments().push_back(p);

src/goto-instrument/generate_function_bodies.cpp

@@ -169,12 +169,14 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
     const exprt &lhs,
     const std::size_t initial_depth,
     const source_locationt &source_location,
+    const irep_idt &function_id,
     symbol_tablet &symbol_table,
     goto_programt &dest) const
   {
     symbol_factoryt symbol_factory(
       symbol_table,
       source_location,
+      function_id,
       object_factory_parameters,
       lifetimet::DYNAMIC);
 
@@ -235,6 +237,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
           dereference_expr,
           1, // depth 1 since we pass the dereferenced pointer
           function_symbol.location,
+          function_name,
           symbol_table,
           dest);
 
@@ -260,6 +263,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
         symbol_exprt(global_sym.name, global_sym.type),
         0,
         function_symbol.location,
+        irep_idt(),
         symbol_table,
         dest);
 
@@ -291,6 +295,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
         aux_symbol.symbol_expr(),
         0,
         function_symbol.location,
+        function_name,
         symbol_table,
         dest);
 

src/goto-instrument/wmm/abstract_event.h

@@ -34,6 +34,7 @@ class abstract_eventt:public graph_nodet<empty_edget>
   irep_idt variable;
   unsigned id;
   source_locationt source_location;
+  irep_idt function_id;
   bool local;
 
   // for ASMfence
@@ -61,10 +62,20 @@ class abstract_eventt:public graph_nodet<empty_edget>
   }
 
   abstract_eventt(
-    operationt _op, unsigned _th, irep_idt _var,
-    unsigned _id, source_locationt _loc, bool _local)
-    :operation(_op), thread(_th), variable(_var), id(_id),
-    source_location(_loc), local(_local)
+    operationt _op,
+    unsigned _th,
+    irep_idt _var,
+    unsigned _id,
+    source_locationt _loc,
+    irep_idt _function_id,
+    bool _local)
+    : operation(_op),
+      thread(_th),
+      variable(_var),
+      id(_id),
+      source_location(_loc),
+      function_id(_function_id),
+      local(_local)
   {
   }
 
@@ -74,27 +85,29 @@ class abstract_eventt:public graph_nodet<empty_edget>
     irep_idt _var,
     unsigned _id,
     source_locationt _loc,
+    irep_idt _function_id,
     bool _local,
     bool WRf,
     bool WWf,
     bool RRf,
     bool RWf,
     bool WWc,
     bool RWc,
-    bool RRc):
-    operation(_op),
-    thread(_th),
-    variable(_var),
-    id(_id),
-    source_location(_loc),
-    local(_local),
-    WRfence(RWf),
-    WWfence(WWf),
-    RRfence(RRf),
-    RWfence(WRf),
-    WWcumul(WWc),
-    RWcumul(RWc),
-    RRcumul(RRc)
+    bool RRc)
+    : operation(_op),
+      thread(_th),
+      variable(_var),
+      id(_id),
+      source_location(_loc),
+      function_id(_function_id),
+      local(_local),
+      WRfence(RWf),
+      WWfence(WWf),
+      RRfence(RRf),
+      RWfence(WRf),
+      WWcumul(WWc),
+      RWcumul(RWc),
+      RRcumul(RRc)
   {
   }
 
@@ -106,6 +119,7 @@ class abstract_eventt:public graph_nodet<empty_edget>
     variable=other.variable;
     id=other.id;
     source_location=other.source_location;
+    function_id = other.function_id;
     local=other.local;
   }
 

src/goto-instrument/wmm/event_graph.cpp

@@ -94,10 +94,10 @@ event_idt event_grapht::copy_segment(event_idt begin, event_idt end)
   const abstract_eventt &end_event=operator[](end);
 
   /* not sure -- we should allow cross function cycles */
-  if(begin_event.source_location.get_file()!=end_event.source_location
-    .get_file()
-    || begin_event.source_location.get_function()!=end_event.source_location
-    .get_function())
+  if(
+    begin_event.source_location.get_file() !=
+      end_event.source_location.get_file() ||
+    begin_event.function_id != end_event.function_id)
     return end;
 
   if(duplicated_bodies.find(std::make_pair(begin_event, end_event))