diff --git a/regression/cbmc/xml-trace/main.c b/regression/cbmc/xml-trace/main.c new file mode 100644 index 00000000000..3bba32cbcf6 --- /dev/null +++ b/regression/cbmc/xml-trace/main.c @@ -0,0 +1,14 @@ +#include +#include + +union myunion { + int64_t i; + double d; +}; + +void test(union myunion u) +{ + u.i += 1; + double d = u.d; + assert(d != 5); +} diff --git a/regression/cbmc/xml-trace/test.desc b/regression/cbmc/xml-trace/test.desc new file mode 100644 index 00000000000..0fc03ee356c --- /dev/null +++ b/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 + +-- +^warning: ignoring +-- +Tests whether the assignment XML output contains all the required elements +such as identifier, full_lhs, full_lhs_value and value. diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 81705da4515..9c5ada4d48e 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening #include #include +#include #include #include #include @@ -35,6 +36,12 @@ static optionalt 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 }