Ticket #93: malloc.report

File malloc.report, 7.5 KB (added by Lukáš Zaoral, 5 years ago)

Line
1	states per second: 468.75
2	state count: 15
3	mips: 0.556219
4
5	version: 4.3.6+b8f657ddf59e
6	architecture: Intel(R) Core(TM) i7-6820HQ CPU @ 2.70GHz
7	memory used: 734124
8	physical memory used: 242996
9	user time: 1.617197
10	system time: 0.076497
11	wall time: 1.525529
12
13	fragment memory:
14	total: { items: 176, used: 1739411, held: 2652496 }
15	1: { items: 6, used: 6, held: 12264 }
16	2: { items: 1, used: 2, held: 4088 }
17	4: { items: 3, used: 12, held: 12264 }
18	5: { items: 0, used: 0, held: 4088 }
19	6: { items: 1, used: 6, held: 4088 }
20	8: { items: 10, used: 80, held: 16352 }
21	9: { items: 1, used: 9, held: 4080 }
22	16: { items: 13, used: 208, held: 12240 }
23	20: { items: 2, used: 40, held: 8160 }
24	24: { items: 8, used: 192, held: 20400 }
25	25: { items: 0, used: 0, held: 4064 }
26	32: { items: 18, used: 576, held: 20320 }
27	33: { items: 0, used: 0, held: 8160 }
28	36: { items: 1, used: 36, held: 12240 }
29	37: { items: 1, used: 37, held: 8160 }
30	40: { items: 4, used: 160, held: 12240 }
31	41: { items: 1, used: 41, held: 8160 }
32	44: { items: 3, used: 132, held: 16320 }
33	48: { items: 0, used: 0, held: 12240 }
34	49: { items: 1, used: 49, held: 12264 }
35	50: { items: 1, used: 50, held: 12264 }
36	52: { items: 1, used: 52, held: 4088 }
37	53: { items: 1, used: 53, held: 20440 }
38	56: { items: 4, used: 224, held: 16352 }
39	57: { items: 0, used: 0, held: 4032 }
40	58: { items: 1, used: 58, held: 8064 }
41	60: { items: 2, used: 120, held: 8064 }
42	64: { items: 3, used: 192, held: 12096 }
43	65: { items: 1, used: 65, held: 8064 }
44	67: { items: 0, used: 0, held: 4032 }
45	68: { items: 1, used: 68, held: 4032 }
46	69: { items: 1, used: 69, held: 16128 }
47	70: { items: 1, used: 70, held: 12096 }
48	72: { items: 5, used: 360, held: 16128 }
49	73: { items: 3, used: 219, held: 12240 }
50	74: { items: 0, used: 0, held: 4080 }
51	77: { items: 1, used: 77, held: 16320 }
52	78: { items: 1, used: 78, held: 16320 }
53	79: { items: 0, used: 0, held: 4080 }
54	80: { items: 12, used: 960, held: 20400 }
55	81: { items: 1, used: 81, held: 8096 }
56	82: { items: 0, used: 0, held: 16192 }
57	84: { items: 0, used: 0, held: 12144 }
58	86: { items: 0, used: 0, held: 4048 }
59	87: { items: 0, used: 0, held: 4048 }
60	88: { items: 2, used: 176, held: 8096 }
61	89: { items: 0, used: 0, held: 4032 }
62	90: { items: 1, used: 90, held: 4032 }
63	91: { items: 1, used: 91, held: 20160 }
64	93: { items: 0, used: 0, held: 4032 }
65	94: { items: 0, used: 0, held: 4032 }
66	96: { items: 5, used: 480, held: 16128 }
67	97: { items: 0, used: 0, held: 16224 }
68	99: { items: 0, used: 0, held: 4056 }
69	104: { items: 1, used: 104, held: 4056 }
70	105: { items: 1, used: 105, held: 12096 }
71	108: { items: 2, used: 216, held: 4032 }
72	109: { items: 1, used: 109, held: 4032 }
73	110: { items: 0, used: 0, held: 4032 }
74	112: { items: 1, used: 112, held: 4032 }
75	114: { items: 1, used: 114, held: 4080 }
76	117: { items: 1, used: 117, held: 12240 }
77	119: { items: 0, used: 0, held: 4080 }
78	120: { items: 1, used: 120, held: 4080 }
79	124: { items: 0, used: 0, held: 3968 }
80	125: { items: 1, used: 125, held: 3968 }
81	129: { items: 1, used: 129, held: 4080 }
82	130: { items: 0, used: 0, held: 12240 }
83	131: { items: 1, used: 131, held: 4080 }
84	133: { items: 1, used: 133, held: 8160 }
85	134: { items: 1, used: 134, held: 4080 }
86	138: { items: 0, used: 0, held: 4032 }
87	141: { items: 0, used: 0, held: 12096 }
88	148: { items: 0, used: 0, held: 3952 }
89	150: { items: 0, used: 0, held: 3952 }
90	152: { items: 2, used: 304, held: 7904 }
91	154: { items: 0, used: 0, held: 4000 }
92	156: { items: 3, used: 468, held: 16000 }
93	158: { items: 2, used: 316, held: 8000 }
94	161: { items: 1, used: 161, held: 4032 }
95	162: { items: 2, used: 324, held: 20160 }
96	167: { items: 0, used: 0, held: 4032 }
97	177: { items: 0, used: 0, held: 4048 }
98	181: { items: 0, used: 0, held: 4048 }
99	183: { items: 0, used: 0, held: 12144 }
100	194: { items: 1, used: 194, held: 4000 }
101	210: { items: 0, used: 0, held: 3888 }
102	219: { items: 0, used: 0, held: 4032 }
103	222: { items: 0, used: 0, held: 12096 }
104	232: { items: 0, used: 0, held: 3944 }
105	239: { items: 0, used: 0, held: 4080 }
106	245: { items: 0, used: 0, held: 3968 }
107	251: { items: 0, used: 0, held: 3840 }
108	255: { items: 1, used: 255, held: 3840 }
109	256: { items: 1, used: 256, held: 3840 }
110	272: { items: 4, used: 1088, held: 12240 }
111	276: { items: 1, used: 276, held: 3920 }
112	291: { items: 1, used: 291, held: 3848 }
113	296: { items: 1, used: 296, held: 3848 }
114	304: { items: 0, used: 0, held: 3952 }
115	307: { items: 0, used: 0, held: 4056 }
116	316: { items: 0, used: 0, held: 11520 }
117	319: { items: 1, used: 319, held: 3840 }
118	331: { items: 1, used: 331, held: 4032 }
119	344: { items: 0, used: 0, held: 11352 }
120	361: { items: 0, used: 0, held: 8096 }
121	362: { items: 0, used: 0, held: 4048 }
122	370: { items: 1, used: 370, held: 3760 }
123	433: { items: 1, used: 433, held: 3960 }
124	440: { items: 1, used: 440, held: 3960 }
125	502: { items: 1, used: 502, held: 4032 }
126	587: { items: 0, used: 0, held: 3552 }
127	679: { items: 2, used: 1358, held: 4080 }
128	1197: { items: 1, used: 1197, held: 3600 }
129	1320: { items: 6, used: 7920, held: 15840 }
130	1338: { items: 2, used: 2676, held: 12096 }
131	666752: { items: 1, used: 666752, held: 666752 }
132	1046016: { items: 1, used: 1046016, held: 1046016 }
133	snapshot memory:
134	total: { items: 15, used: 5496, held: 43304 }
135	60: { items: 1, used: 60, held: 4032 }
136	72: { items: 0, used: 0, held: 4032 }
137	120: { items: 0, used: 0, held: 4080 }
138	228: { items: 1, used: 228, held: 3944 }
139	288: { items: 1, used: 288, held: 4032 }
140	360: { items: 2, used: 720, held: 7920 }
141	420: { items: 10, used: 4200, held: 15264 }
142	fragment table: { used: 80, capacity: 256 }
143	snapshot table: { used: 15, capacity: 256 }
144	input file: malloc.c
145	compile options:
146	- malloc.c
147	input options:
148	divine.bcname: "malloc.c"
149	dios config:
150	leak check: [ "exit" ]
151	smt solver: stp
152	property type: safety
153
154	timers:
155	lart: 0.512
156	loader: 0.572
157	boot: 0.053
158	search: 0.032
159	ce: 0.088
160	error found: yes
161	error trace: \|
162	[0] malloc: Success
163	LEAK: weak* fbe0520f 0
164	FAULT:
165	[0] FATAL: memory leak in userspace
166
167	machine trace:
168	- choices: 0/1 0/2
169	interrupts: C/1877/276:28
170	- choices: 0/1
171	interrupts: C/86/276:28
172	- choices: 0/1
173	interrupts: C/86/276:28
174	- choices: 0/1
175	interrupts: C/86/276:28
176	- choices: 0/1
177	interrupts: C/86/276:28
178	- choices: 0/1
179	interrupts: C/521/184:45
180	- choices: 0/1
181	interrupts: C/908/276:28
182	- choices: 0/1
183	interrupts: C/86/276:28
184	- choices: 0/1
185	interrupts: C/86/276:28
186	- choices: 0/1
187	interrupts: C/86/276:28
188	- choices: 0/1
189	interrupts: C/86/276:28
190	- choices: 0/1
191	interrupts: C/842/184:98
192	- choices: 0/1
193	interrupts: ""
194
195	active stack:
196	- symbol: void __dios::FaultBase::handler<__dios::Upcall<__dios::fs::VFS<__dios::ProcessManager<__dios::Fault<__dios::Scheduler<__dios::Base> > > > > >(_VM_Fault, _VM_Frame, void ()())
197	location: /dios/include/dios/sys/fault.hpp:118
198	pc: code* 802bf 4
199	address: heap* 825e109a 0+0
200
201	- symbol: __dios_fault
202	location: /dios/src/arch/divm/fault.c:12
203	pc: code* 80544 1b
204	address: heap* 6abe8348 0+0
205
206	- symbol: _exit
207	location: /dios/src/libc/sys/start.cpp:61
208	pc: code* 80123 a
209	address: heap* b72b8e24 0+0
210
211	- symbol: _Exit
212	location: /dios/src/libc/stdlib/_Exit.c:19
213	pc: code* 80113 7
214	address: heap* 1160628d 0+0
215
216	- symbol: exit
217	location: /dios/src/libc/stdlib/exit.c:6
218	pc: code* 800da 6
219	address: heap* c169917c 0+0
220
221	- symbol: __dios_start
222	location: /dios/src/libc/sys/start.cpp:108
223	pc: code* 80126 35h
224	address: heap* 47fc22b9 0+0
225