Skip to content

Commit 44879df

Browse files
hannes-steffenhagen-diffbluepetr-bauch
hannes-steffenhagen-diffblue
authored and
petr-bauch
committed
Add XSD that describes output of cbmc --trace
Note that this is based on observed outputs from cbmc, there is currently no mechanism in place that enforces CBMC to conform to this. We have discussed adding a regression test pass for checking that at least our own regression tests conform to the spec. In a future PR.
1 parent 7e2ad38 commit 44879df

File tree

1 file changed

+180
-0
lines changed

1 file changed

+180
-0
lines changed

‎doc/assets/xml_spec.xsd

Lines changed: 180 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
<?xml version="1.0" encoding="UTF-8" ?>
2+
<xs:schema xmlns:xs="http://www.w3.org/2001/XMLSchema">
3+
<!-- This is mostly meant for reference purposes.
4+
This schema is descriptive of observed output from
5+
cbmc, not prescriptive (i.e. there currently is
6+
no mechanism in place to ensure that cbmc outputs
7+
will conform to this specification).
8+
-->
9+
10+
<xs:element name="location">
11+
<xs:complexType>
12+
<xs:attribute name="file" type="xs:string" use="optional"/>
13+
<xs:attribute name="line" type="xs:int" use="optional"/>
14+
<xs:attribute name="working-directory" type="xs:string"
15+
use="optional"/>
16+
<xs:attribute name="function" type="xs:string" use="optional"/>
17+
</xs:complexType>
18+
</xs:element>
19+
20+
<xs:attributeGroup name="traceStepAttrs">
21+
<xs:attribute name="hidden" type="xs:string"/>
22+
<xs:attribute name="step_nr" type="xs:int"/>
23+
<xs:attribute name="thread" type="xs:int"/>
24+
</xs:attributeGroup>
25+
26+
<xs:element name="failure">
27+
<xs:complexType>
28+
<xs:all>
29+
<xs:element ref="location" minOccurs="0"/>
30+
</xs:all>
31+
<xs:attributeGroup ref="traceStepAttrs"/>
32+
<xs:attribute name="property" type="xs:string"/>
33+
<xs:attribute name="reason" type="xs:string"/>
34+
</xs:complexType>
35+
</xs:element>
36+
37+
<xs:element name="assignment">
38+
<xs:complexType>
39+
<xs:all>
40+
<xs:element ref="location" minOccurs="0"/>
41+
<xs:element name="type" type="xs:string" minOccurs="0"/>
42+
<xs:element name="full_lhs" type="xs:string"/>
43+
<xs:element name="full_lhs_value" type="xs:string"/>
44+
</xs:all>
45+
<xs:attributeGroup ref="traceStepAttrs"/>
46+
<xs:attribute name="assignment_type" type="xs:string"/>
47+
<xs:attribute name="base_name" type="xs:string"
48+
use="optional"/>
49+
<xs:attribute name="display_name" type="xs:string"
50+
use="optional"/>
51+
<xs:attribute name="identifier" type="xs:string"
52+
use="optional"/>
53+
<xs:attribute name="mode" type="xs:string" use="optional"/>
54+
</xs:complexType>
55+
</xs:element>
56+
57+
<xs:element name="value_expression">
58+
<xs:complexType>
59+
<xs:sequence>
60+
<xs:any processContents="lax" maxOccurs="unbounded" minOccurs="0"/>
61+
</xs:sequence>
62+
</xs:complexType>
63+
</xs:element>
64+
65+
<xs:element name="input">
66+
<xs:complexType>
67+
<xs:sequence>
68+
<xs:element name="input_id" type="xs:string"/>
69+
<xs:sequence minOccurs="0" maxOccurs="unbounded">
70+
<xs:element name="value" type="xs:string"/>
71+
<xs:element ref="value_expression"/>
72+
</xs:sequence>
73+
<xs:element ref="location" minOccurs="0"/>
74+
</xs:sequence>
75+
<xs:attributeGroup ref="traceStepAttrs"/>
76+
</xs:complexType>
77+
</xs:element>
78+
79+
<xs:element name="output">
80+
<xs:complexType>
81+
<xs:sequence>
82+
<xs:element name="text" type="xs:string"/>
83+
<xs:element ref="location" minOccurs="0"/>
84+
<xs:sequence minOccurs="0" maxOccurs="unbounded">
85+
<xs:element name="value" type="xs:string"/>
86+
<xs:element ref="value_expression"/>
87+
</xs:sequence>
88+
</xs:sequence>
89+
<xs:attributeGroup ref="traceStepAttrs"/>
90+
</xs:complexType>
91+
</xs:element>
92+
93+
<xs:element name="function_call">
94+
<xs:complexType>
95+
<xs:all>
96+
<xs:element ref="location" minOccurs="0"/>
97+
<xs:element ref="function"/>
98+
</xs:all>
99+
<xs:attributeGroup ref="traceStepAttrs"/>
100+
</xs:complexType>
101+
</xs:element>
102+
103+
<xs:element name="function">
104+
<xs:complexType>
105+
<xs:all>
106+
<xs:element ref="location" minOccurs="0"/>
107+
</xs:all>
108+
<xs:attribute name="display_name" type="xs:string"/>
109+
<xs:attribute name="identifier" type="xs:string"/>
110+
</xs:complexType>
111+
</xs:element>
112+
113+
<xs:element name="function_return">
114+
<xs:complexType>
115+
<xs:sequence>
116+
<xs:element ref="function"/>
117+
<xs:element ref="location" minOccurs="0"/>
118+
</xs:sequence>
119+
<xs:attributeGroup ref="traceStepAttrs"/>
120+
</xs:complexType>
121+
</xs:element>
122+
123+
124+
<xs:element name="location-only">
125+
<xs:complexType>
126+
<xs:all>
127+
<xs:element ref="location" minOccurs="0"/>
128+
</xs:all>
129+
<xs:attributeGroup ref="traceStepAttrs"/>
130+
</xs:complexType>
131+
</xs:element>
132+
133+
<xs:element name="goto_trace">
134+
<xs:complexType>
135+
<xs:choice minOccurs="0" maxOccurs="unbounded">
136+
<xs:element ref="assignment"></xs:element>
137+
<xs:element ref="failure"></xs:element>
138+
<xs:element ref="function_call"></xs:element>
139+
<xs:element ref="function_return"></xs:element>
140+
<xs:element ref="input"></xs:element>
141+
<xs:element ref="output"></xs:element>
142+
<xs:element ref="location-only"></xs:element>
143+
</xs:choice>
144+
</xs:complexType>
145+
</xs:element>
146+
<xs:element name="result">
147+
<xs:complexType>
148+
<xs:sequence>
149+
<xs:element ref="goto_trace" minOccurs="0"/>
150+
</xs:sequence>
151+
<xs:attribute name="property" type="xs:string"/>
152+
<xs:attribute name="status" type="xs:string"/>
153+
</xs:complexType>
154+
</xs:element>
155+
156+
<xs:element name="message">
157+
<xs:complexType>
158+
<xs:sequence>
159+
<xs:element ref="location" minOccurs="0"/>
160+
<xs:element name="text" type="xs:string"/>
161+
</xs:sequence>
162+
<xs:attribute name="type" type="xs:string"/>
163+
</xs:complexType>
164+
</xs:element>
165+
166+
<xs:element name="program" type="xs:string"/>
167+
<xs:element name="cprover-status" type="xs:string"/>
168+
<xs:element name="cprover">
169+
<xs:complexType>
170+
<xs:sequence>
171+
<xs:element ref="program"/>
172+
<xs:choice minOccurs="0" maxOccurs="unbounded">
173+
<xs:element ref="message"/>
174+
<xs:element ref="result"/>
175+
</xs:choice>
176+
<xs:element ref="cprover-status" minOccurs="0"/>
177+
</xs:sequence>
178+
</xs:complexType>
179+
</xs:element>
180+
</xs:schema>

0 commit comments

Comments
 (0)