Merge pull request #6869 from tautschnig/bugfixes/6845-part-1-xml

XML counterexample trace: display member types

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;
         }
       }