Merge pull request #7856 from tautschnig/bugfixes/linking-location

Add missing source locations

Author: tautschnig

jbmc/src/java_bytecode/nondet.cpp

@@ -123,7 +123,9 @@ code_blockt generate_nondet_switch(
     this_block.add(switch_case);
     this_block.add(code_breakt());
     code_switch_caset this_case(
-      from_integer(case_number, switch_value.type()), this_block);
+      from_integer(case_number, switch_value.type())
+        .with_source_location(source_location),
+      this_block);
     switch_block.add(std::move(this_case));
     ++case_number;
   }

regression/CMakeLists.txt

@@ -77,6 +77,7 @@ add_subdirectory(k-induction)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-harness-multi-file-project)
 add_subdirectory(goto-cc-file-local)
+add_subdirectory(goto-cc-multi-file)
 add_subdirectory(goto-cc-regression-gh-issue-5380)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)

regression/Makefile

@@ -50,6 +50,7 @@ DIRS = cbmc-shadow-memory \
        goto-harness \
        goto-harness-multi-file-project \
        goto-cc-file-local \
+       goto-cc-multi-file \
        goto-cc-regression-gh-issue-5380 \
        linking-goto-binaries \
        symtab2gb \

regression/cbmc-cover/location3/main.c

@@ -0,0 +1,22 @@
+int main()
+{
+  int b, c;
+
+  if(b)
+  {
+    if(c)
+    {
+      c = 1;
+    }
+    else
+    {
+      c = 2;
+    }
+  }
+  else
+  {
+    b = 0;
+  }
+
+  return 1;
+}

regression/cbmc-cover/location3/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.\d+\] file main.c line 9 function main block \d+ \(lines main.c:main:9,10\): SATISFIED$
+^\[main.coverage.\d+\] file main.c line 15 function main block \d+ \(lines main.c:main:15\): SATISFIED$
+^\*\* 7 of 7 covered \(100.0%\)
+--
+^warning: ignoring
+--
+All gotos must have a source location annotated.

regression/goto-cc-multi-file/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}"
+)

regression/goto-cc-multi-file/maintain-location/main.c

@@ -0,0 +1,11 @@
+int foo()
+{
+  return 0;
+}
+
+int main()
+{
+  int result;
+  result = foo();
+  return result;
+}

regression/goto-cc-multi-file/maintain-location/other.c

@@ -0,0 +1,6 @@
+int foo();
+
+int bar()
+{
+  return foo();
+}

regression/goto-cc-multi-file/maintain-location/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+other.c
+file main.c line 9 function main
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+We previously lost the location attached to the call of `foo` in function main.

src/ansi-c/c_typecheck_expr.cpp

@@ -1044,15 +1044,16 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
     new_expr = size_of_opt.value();
   }
 
+  source_locationt location = expr.source_location();
   new_expr.swap(expr);
-
+  expr.add_source_location() = location;
   expr.add(ID_C_c_sizeof_type)=type;
 
   // The type may contain side-effects.
   if(!clean_code.empty())
   {
     side_effect_exprt side_effect_expr(
-      ID_statement_expression, void_type(), expr.source_location());
+      ID_statement_expression, void_type(), location);
     auto decl_block=code_blockt::from_list(clean_code);
     decl_block.set_statement(ID_decl_block);
     side_effect_expr.copy_to_operands(decl_block);
@@ -1064,8 +1065,9 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
     // It is not obvious whether the type or 'e' should be evaluated
     // first.
 
-    binary_exprt comma_expr{
-      std::move(side_effect_expr), ID_comma, expr, expr.type()};
+    exprt comma_expr =
+      binary_exprt{std::move(side_effect_expr), ID_comma, expr, expr.type()}
+        .with_source_location(location);
     expr.swap(comma_expr);
   }
 }
@@ -4656,6 +4658,8 @@ class is_compile_time_constantt
 
 void c_typecheck_baset::make_constant(exprt &expr)
 {
+  source_locationt location = expr.find_source_location();
+
   // Floating-point expressions may require a rounding mode.
   // ISO 9899:1999 F.7.2 says that the default is "round to nearest".
   // Some compilers have command-line options to override.
@@ -4664,10 +4668,11 @@ void c_typecheck_baset::make_constant(exprt &expr)
   adjust_float_expressions(expr, rounding_mode);
 
   simplify(expr, *this);
+  expr.add_source_location() = location;
 
   if(!is_compile_time_constantt(*this)(expr))
   {
-    error().source_location=expr.find_source_location();
+    error().source_location = location;
     error() << "expected constant expression, but got '" << to_string(expr)
             << "'" << eom;
     throw 0;
@@ -4676,13 +4681,15 @@ void c_typecheck_baset::make_constant(exprt &expr)
 
 void c_typecheck_baset::make_constant_index(exprt &expr)
 {
+  source_locationt location = expr.find_source_location();
   make_constant(expr);
   make_index_type(expr);
   simplify(expr, *this);
+  expr.add_source_location() = location;
 
   if(!is_compile_time_constantt(*this)(expr))
   {
-    error().source_location=expr.find_source_location();
+    error().source_location = location;
     error() << "conversion to integer constant failed" << eom;
     throw 0;
   }