Remove function from source_locationt [depends-on: #4131]

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -869,7 +869,7 @@ void jbmc_parse_optionst::process_goto_function(
     if(using_symex_driven_loading)
     {
       // label the assertions
-      label_properties(goto_function.body);
+      label_properties(goto_function.body, function.get_function_id());
 
       goto_function.body.update();
       function.compute_location_numbers();

regression/cbmc/unique_labels1/bar.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+static int foo()
+{
+  assert(1 < 0);
+}
+
+void bar()
+{
+  foo();
+}

regression/cbmc/unique_labels1/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+static int foo()
+{
+  assert(0);
+}
+
+void bar();
+
+int main()
+{
+  foo();
+  bar();
+}

regression/cbmc/unique_labels1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+bar.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+assertion\.2
+--
+Each of the assertions in the two functions named "foo" should have a unique
+prefix, and thus be numbered "<prefix>.assertion.1."

regression/contracts/function_check_04/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 --apply-code-contracts
 ^\[main.assertion.1\] .* assertion x == 0: SUCCESS$
-^\[foo.1\] line 9 .*: FAILURE$
+^\[__CPROVER_initialize.1\] line 9 .*: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

src/ansi-c/ansi_c_declaration.cpp

@@ -131,14 +131,14 @@ void ansi_c_declarationt::to_symbol(
   symbol.value=declarator.value();
   symbol.type=full_type(declarator);
   symbol.name=declarator.get_name();
-  symbol.pretty_name=symbol.name;
-  symbol.base_name=declarator.get_base_name();
+  symbol.display_name=declarator.get_base_name();
   symbol.is_type=get_is_typedef();
   symbol.location=declarator.source_location();
   symbol.is_extern=get_is_extern();
   symbol.is_macro=get_is_typedef() || get_is_enum_constant();
   symbol.is_parameter=get_is_parameter();
   symbol.is_weak=get_is_weak();
+  symbol.has_local_scope = !get_is_global();
 
   // is it a function?
 

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/ansi-c/expr2c.cpp

@@ -160,6 +160,8 @@ void expr2ct::get_shorthands(const exprt &expr)
       irep_idt func;
 
       const symbolt *symbol;
+      // we use the source-level function name as a means to detect collisions,
+      // which is ok, because this is about generating user-visible output
       if(!ns.lookup(symbol_id, symbol))
         func=symbol->location.get_function();
 

src/ansi-c/type2name.cpp

@@ -38,21 +38,27 @@ static std::string type2name_tag(
   if(ns.lookup(identifier, symbol))
     return "SYM#"+id2string(identifier)+"#";
 
+  std::string result;
+
+  // this isn't really a qualifier, but the linker needs to
+  // distinguish these - should likely be fixed in the linker instead
+  if(symbol->has_local_scope)
+    result += 'l';
+
   assert(symbol && symbol->is_type);
 
   if(symbol->type.id()!=ID_struct &&
      symbol->type.id()!=ID_union)
-    return type2name(symbol->type, ns, symbol_number);
+    return result + type2name(symbol->type, ns, symbol_number);
 
   // assign each symbol a number when seen for the first time
   std::pair<symbol_numbert::iterator, bool> entry=
     symbol_number.insert(std::make_pair(
         identifier,
         std::make_pair(symbol_number.size(), true)));
 
-  std::string result = "SYM" +
-                       id2string(to_struct_union_type(symbol->type).get_tag()) +
-                       '#' + std::to_string(entry.first->second.first);
+  result += "SYM" + id2string(to_struct_union_type(symbol->type).get_tag()) +
+            '#' + std::to_string(entry.first->second.first);
 
   // new entry, add definition
   if(entry.second)
@@ -99,11 +105,6 @@ static std::string type2name(
   if(type.get_bool(ID_C_noreturn))
     result+='n';
 
-  // this isn't really a qualifier, but the linker needs to
-  // distinguish these - should likely be fixed in the linker instead
-  if(!type.source_location().get_function().empty())
-    result+='l';
-
   if(type.id().empty())
     throw "empty type encountered";
   else if(type.id()==ID_empty)

src/cpp/cpp_declarator_converter.cpp

@@ -426,6 +426,8 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
   symbol.is_type=is_typedef;
   symbol.is_macro=is_typedef && !is_template_parameter;
   symbol.pretty_name=pretty_name;
+  symbol.has_local_scope =
+    !cpp_typecheck.cpp_scopes.current_scope().is_global_scope();
 
   // Constant? These are propagated.
   if(symbol.type.get_bool(ID_C_constant) &&

src/cpp/cpp_typecheck_compound_type.cpp

@@ -233,6 +233,7 @@ void cpp_typecheckt::typecheck_compound_type(
       cpp_scopes.current_scope().suffix;
     symbol.type.set(
       ID_tag, cpp_scopes.current_scope().prefix+id2string(symbol.base_name));
+    symbol.has_local_scope = !cpp_scopes.current_scope().is_global_scope();
 
     // move early, must be visible before doing body
     symbolt *new_symbol;

src/cpp/cpp_typecheck_enum_type.cpp

@@ -178,6 +178,7 @@ void cpp_typecheckt::typecheck_enum_type(typet &type)
     symbol.is_type=true;
     symbol.is_macro=false;
     symbol.pretty_name=pretty_name;
+    symbol.has_local_scope = !cpp_scopes.current_scope().is_global_scope();
 
     // move early, must be visible before doing body
     symbolt *new_symbol;

src/cpp/cpp_typecheck_template.cpp

@@ -178,6 +178,7 @@ void cpp_typecheckt::typecheck_class_template(
 
   symbol.pretty_name=
     cpp_scopes.current_scope().prefix+id2string(symbol.base_name);
+  symbol.has_local_scope = !cpp_scopes.current_scope().is_global_scope();
 
   symbolt *new_symbol;
   if(symbol_table.move(symbol, new_symbol))

src/goto-instrument/aggressive_slicer.cpp

@@ -92,7 +92,7 @@ void aggressive_slicert::doit()
     auto property_loc = find_property(p, goto_model.goto_functions);
     if(!property_loc.has_value())
       throw "unable to find property in call graph";
-    note_functions_to_keep(property_loc.value().get_function());
+    note_functions_to_keep(property_loc->first);
   }
 
   // Add functions within distance of shortest path functions

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/dump_c.cpp

@@ -168,11 +168,9 @@ void dump_ct::operator()(std::ostream &os)
     const symbolt &symbol=ns.lookup(*it);
     const irep_idt &type_id=symbol.type.id();
 
-    if(symbol.is_type &&
-       symbol.location.get_function().empty() &&
-       (type_id==ID_struct ||
-        type_id==ID_union ||
-        type_id==ID_c_enum))
+    if(
+      symbol.is_type && !symbol.has_local_scope &&
+      (type_id == ID_struct || type_id == ID_union || type_id == ID_c_enum))
     {
       if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers))
       {
@@ -293,7 +291,7 @@ void dump_ct::convert_compound_declaration(
     const symbolt &symbol,
     std::ostream &os_body)
 {
-  if(!symbol.location.get_function().empty())
+  if(symbol.has_local_scope)
     return;
 
   // do compound type body
@@ -737,8 +735,7 @@ void dump_ct::gather_global_typedefs()
   {
     const symbolt &symbol=symbol_entry.second;
 
-    if(symbol.is_macro && symbol.is_type &&
-       symbol.location.get_function().empty())
+    if(symbol.is_macro && symbol.is_type && !symbol.has_local_scope)
     {
       const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
       PRECONDITION(!typedef_str.empty());
@@ -843,9 +840,10 @@ void dump_ct::convert_global_variable(
     std::ostream &os,
     local_static_declst &local_static_decls)
 {
-  const irep_idt &func=symbol.location.get_function();
-  if((func.empty() || symbol.is_extern || symbol.value.is_not_nil()) &&
-      !converted_global.insert(symbol.name).second)
+  const bool global = !symbol.has_local_scope;
+  if(
+    (global || symbol.is_extern || symbol.value.is_not_nil()) &&
+    !converted_global.insert(symbol.name).second)
     return;
 
   code_declt d(symbol.symbol_expr());
@@ -856,8 +854,7 @@ void dump_ct::convert_global_variable(
 
   // add a tentative declaration to cater for symbols in the initializer
   // relying on it this symbol
-  if((func.empty() || symbol.is_extern) &&
-     (symbol.value.is_nil() || !syms.empty()))
+  if((global || symbol.is_extern) && (symbol.value.is_nil() || !syms.empty()))
   {
     os << "// " << symbol.name << '\n';
     os << "// " << symbol.location << '\n';
@@ -889,7 +886,7 @@ void dump_ct::convert_global_variable(
     d.copy_to_operands(symbol.value);
   }
 
-  if(!func.empty() && !symbol.is_extern)
+  if(!global && !symbol.is_extern)
   {
     local_static_decls.emplace(symbol.name, d);
   }

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