Merge pull request #6995 from tautschnig/bugfixes/6994-to_array_expr-source-loc

string_constantt::to_array_expr must maintain the source location

Author: tautschnig

regression/cbmc/String_Literal1/main.c

@@ -52,4 +52,6 @@ int main()
 
   // generic wide string, OS-dependent
   assert(sizeof(L""[0])==sizeof(wchar_t));
+
+  assert(0);
 }

regression/cbmc/String_Literal1/test.desc

@@ -1,8 +1,15 @@
 CORE
 main.c
-
-^EXIT=0$
+--trace
+^State \d+ file main.c function main line 20 thread 0$
+^State \d+ file main.c function main line 36 thread 0$
+^State \d+ file main.c function main line 44 thread 0$
+^\*\* 1 of \d+ failed \(\d+ iterations\)$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+^State \d+ (function main )?thread 0$
+--
+Each step in the trace must have a full source location, including line numbers.

src/util/expr.h

@@ -98,6 +98,30 @@ class exprt:public irept
   const operandst &operands() const
   { return (const operandst &)get_sub(); }
 
+  /// Add the source location from \p other, if it has any.
+  template <typename T>
+  T &with_source_location(const exprt &other) &
+  {
+    static_assert(
+      std::is_base_of<exprt, T>::value,
+      "The template argument T must be derived from exprt.");
+    if(other.source_location().is_not_nil())
+      add_source_location() = other.source_location();
+    return *static_cast<T *>(this);
+  }
+
+  /// Add the source location from \p other, if it has any.
+  template <typename T>
+  T &&with_source_location(const exprt &other) &&
+  {
+    static_assert(
+      std::is_base_of<exprt, T>::value,
+      "The template argument T must be derived from exprt.");
+    if(other.source_location().is_not_nil())
+      add_source_location() = other.source_location();
+    return std::move(*static_cast<T *>(this));
+  }
+
 protected:
   exprt &op0()
   { return operands().front(); }

src/util/std_expr.h

@@ -1571,6 +1571,16 @@ class array_exprt : public multi_ary_exprt
   {
     return static_cast<array_typet &>(multi_ary_exprt::type());
   }
+
+  array_exprt &with_source_location(const exprt &other) &
+  {
+    return exprt::with_source_location<array_exprt>(other);
+  }
+
+  array_exprt &&with_source_location(const exprt &other) &&
+  {
+    return std::move(*this).exprt::with_source_location<array_exprt>(other);
+  }
 };
 
 template <>

src/util/string_constant.cpp

@@ -53,5 +53,5 @@ array_exprt string_constantt::to_array_expr() const
     *it = from_integer(ch, char_type);
   }
 
-  return dest;
+  return std::move(dest).with_source_location(*this);
 }

src/util/string_constant.h

@@ -24,7 +24,6 @@ class string_constantt : public nullary_exprt
   }
 
   array_exprt to_array_expr() const;
-  bool from_array_expr(const array_exprt &);
 };
 
 template <>