This repository has been archived by the owner on Oct 14, 2022. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 9
/
multivar_true-unreach-call1.graphml
125 lines (125 loc) · 5.5 KB
/
multivar_true-unreach-call1.graphml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
<key attr.name="originFileName" attr.type="string" for="edge" id="originfile">
<default>/home/dangl/sv-witnesses/multivar_true-unreach-call1.i</default>
</key>
<key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
<key attr.name="invariant.scope" attr.type="string" for="node" id="invariant.scope"/>
<key attr.name="namedValue" attr.type="string" for="node" id="named"/>
<key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
<default>path</default>
</key>
<key attr.name="isFrontierNode" attr.type="boolean" for="node" id="frontier">
<default>false</default>
</key>
<key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
<default>false</default>
</key>
<key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
<default>false</default>
</key>
<key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
<default>false</default>
</key>
<key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
<default>false</default>
</key>
<key attr.name="violatedProperty" attr.type="string" for="node" id="violatedProperty"/>
<key attr.name="threadId" attr.type="string" for="edge" id="threadId"/>
<key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
<key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
<key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>
<key attr.name="specification" attr.type="string" for="graph" id="specification"/>
<key attr.name="architecture" attr.type="string" for="graph" id="architecture"/>
<key attr.name="producer" attr.type="string" for="graph" id="producer"/>
<key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
<key attr.name="startline" attr.type="int" for="edge" id="startline"/>
<key attr.name="startoffset" attr.type="int" for="edge" id="startoffset"/>
<key attr.name="lineColSet" attr.type="string" for="edge" id="lineCols"/>
<key attr.name="control" attr.type="string" for="edge" id="control"/>
<key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
<key attr.name="assumption.resultfunction" attr.type="string" for="edge" id="assumption.resultfunction"/>
<key attr.name="assumption.scope" attr.type="string" for="edge" id="assumption.scope"/>
<key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
<key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
<key attr.name="predecessor" attr.type="string" for="edge" id="predecessor"/>
<key attr.name="successor" attr.type="string" for="edge" id="successor"/>
<key attr.name="witness-type" attr.type="string" for="graph" id="witness-type"/>
<graph edgedefault="directed">
<data key="witness-type">correctness_witness</data>
<data key="sourcecodelang">C</data>
<data key="producer">CPAchecker 1.6.1-svn</data>
<data key="specification">CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )</data>
<data key="programfile">multivar_true-unreach-call1.i</data>
<data key="programhash">a2577bafced442fc9d7239226a9a4234883426ad</data>
<data key="architecture">32bit</data>
<node id="N9">
<data key="entry">true</data>
</node>
<node id="N22">
<data key="invariant">(y == x)</data>
<data key="invariant.scope">main</data>
</node>
<edge source="N9" target="N22">
<data key="enterLoopHead">true</data>
<data key="sourcecode">unsigned int y = x;</data>
<data key="startline">11</data>
<data key="startoffset">276</data>
</edge>
<node id="N15"/>
<edge source="N22" target="N15">
<data key="sourcecode">[x < 1024]</data>
<data key="startline">12</data>
<data key="startoffset">305</data>
<data key="control">condition-true</data>
</edge>
<node id="N16">
<data key="invariant">(y == x) && (x >= 1024U) && (x <= 4294967295U)</data>
<data key="invariant.scope">main</data>
</node>
<edge source="N22" target="N16">
<data key="sourcecode">[!(x < 1024)]</data>
<data key="startline">12</data>
<data key="startoffset">305</data>
<data key="control">condition-false</data>
</edge>
<node id="N1"/>
<edge source="N16" target="N1">
<data key="sourcecode">__VERIFIER_assert(x == y);</data>
<data key="startline">16</data>
<data key="startoffset">341</data>
<data key="enterFunction">__VERIFIER_assert</data>
</edge>
<node id="N4"/>
<edge source="N1" target="N4">
<data key="sourcecode">[cond == 0]</data>
<data key="startline">4</data>
<data key="startoffset">156</data>
<data key="control">condition-true</data>
</edge>
<edge source="N1" target="N4">
<data key="sourcecode">[!(cond == 0)]</data>
<data key="startline">4</data>
<data key="startoffset">156</data>
<data key="control">condition-false</data>
</edge>
<node id="N0"/>
<edge source="N4" target="N0">
<data key="sourcecode">return;</data>
<data key="startline">7</data>
<data key="startoffset">202</data>
<data key="returnFrom">__VERIFIER_assert</data>
</edge>
<node id="N23"/>
<edge source="N0" target="N23">
<data key="startline">16</data>
<data key="startoffset">341</data>
</edge>
<edge source="N15" target="N22">
<data key="enterLoopHead">true</data>
<data key="sourcecode">y++;</data>
<data key="startline">14</data>
<data key="startoffset">330</data>
</edge>
</graph>
</graphml>