switch-case conversion: ensure case selection has source location

The expression operand was at times lacking a source location when it
had been subject to expression simplification. Fixes the root cause in
the C front-end, and makes sure the invariant is maintained during goto
conversion.

Author: tautschnig

src/ansi-c/c_typecheck_expr.cpp

@@ -4656,6 +4656,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 +4666,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 +4679,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;
   }

src/goto-programs/goto_convert.cpp

@@ -526,6 +526,13 @@ void goto_convertt::convert_switch_case(
 
     exprt::operandst &case_op_dest=cases_entry->second->second;
     case_op_dest.push_back(code.case_op());
+    // make sure we have a source location in the case operand as otherwise we
+    // end up with a GOTO instruction without a source location
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      case_op_dest.back().source_location().is_not_nil(),
+      "case operand should have a source location",
+      case_op_dest.back().pretty(),
+      code.pretty());
   }
 }