XML counterexample trace: display member types

Field-sensitive SSA yields assignments at member/element level. The XML
counterexamples, however, appeared to (continue to) assume that all
assignments take place at object level. Adjust the type (which is only
included in XML output, not in JSON nor plain output) to match that of
the element being assigned.

Author: tautschnig

Diff for: doc/assets/xml_spec.xsd

@@ -39,7 +39,7 @@
   <xs:complexType>
     <xs:all>
       <xs:element ref="location" minOccurs="0"/>
-      <xs:element name="type" type="xs:string" minOccurs="0"/>
+      <xs:element name="full_lhs_type" type="xs:string" minOccurs="0"/>
       <xs:element name="full_lhs" type="xs:string"/>
       <xs:element name="full_lhs_value">
         <xs:complexType>

Diff for: regression/cbmc/xml-trace/test.desc

@@ -1,23 +1,13 @@
 CORE broken-smt-backend
 main.c
 --xml-ui --function test --little-endian
+activate-multi-line-match
 ^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 binary="[01]+">\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>
+<assignment assignment_type="actual_parameter" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>union myunion</full_lhs_type>\n\s*<full_lhs>u</full_lhs>
+<value>\{ \.i=\d+ll? \}</value>\n\s*<value_expression>\n\s*<union>\n\s*<member member_name="i">\n\s*<integer binary="\d+" c_type=".*int.*" width="\d+">\d+</integer>\n\s*</member>\n\s*</union>\n\s*</value_expression>
+<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>signed long( long)? int</full_lhs_type>\n\s*<full_lhs>byte_extract_little_endian\(u, 0ll?, .*int.*\)</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
 --
 ^warning: ignoring
 --

Diff for: src/goto-programs/xml_goto_trace.cpp

@@ -140,15 +140,16 @@ void convert(
           lhs_object.has_value() &&
           !ns.lookup(lhs_object->get_identifier(), symbol))
         {
-          std::string type_string = from_type(ns, symbol->name, symbol->type);
+          std::string type_string =
+            from_type(ns, symbol->name, step.full_lhs.type());
 
           xml_assignment.set_attribute("mode", id2string(symbol->mode));
           xml_assignment.set_attribute("identifier", id2string(symbol->name));
           xml_assignment.set_attribute(
             "base_name", id2string(symbol->base_name));
           xml_assignment.set_attribute(
             "display_name", id2string(symbol->display_name()));
-          xml_assignment.new_element("type").data = type_string;
+          xml_assignment.new_element("full_lhs_type").data = type_string;
         }
       }