Merge pull request #4480 from peterschrammel/byte-extract-lhs-object

Get lhs_object from byte_extract for goto trace

Author: peterschrammel

regression/cbmc/xml-trace/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdint.h>
+
+union myunion {
+  int64_t i;
+  double d;
+};
+
+void test(union myunion u)
+{
+  u.i += 1;
+  double d = u.d;
+  assert(d != 5);
+}

regression/cbmc/xml-trace/test.desc

@@ -0,0 +1,25 @@
+CORE broken-smt-backend
+main.c
+--xml-ui --function test --little-endian
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">
+<location file=".*" function="test" line="\d+" working-directory=".*"/>
+<type>union myunion</type>
+<full_lhs>byte_extract_little_endian\(u, 0ll?, .*int.*\)</full_lhs>
+<full_lhs_value>\d+ll?</full_lhs_value>
+<value>\{ \.i=\d+ll? \}</value>
+<value_expression>
+<union>
+<member member_name="i">
+<integer binary="\d+" c_type=".*int.*" width="\d+">\d+</integer>
+</member>
+</union>
+</value_expression>
+</assignment>
+--
+^warning: ignoring
+--
+Tests whether the assignment XML output contains all the required elements
+such as identifier, full_lhs, full_lhs_value and value.

src/goto-programs/goto_trace.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening
 #include <ostream>
 
 #include <util/arith_tools.h>
+#include <util/byte_operators.h>
 #include <util/format_expr.h>
 #include <util/range.h>
 #include <util/string_utils.h>
@@ -35,6 +36,12 @@ static optionalt<symbol_exprt> get_object_rec(const exprt &src)
     return get_object_rec(to_index_expr(src).array());
   else if(src.id()==ID_typecast)
     return get_object_rec(to_typecast_expr(src).op());
+  else if(
+    src.id() == ID_byte_extract_little_endian ||
+    src.id() == ID_byte_extract_big_endian)
+  {
+    return get_object_rec(to_byte_extract_expr(src).op());
+  }
   else
     return {}; // give up
 }