Report for test/programs/benchmarks/loops/bubble_sort_false-unreach-call.i (Counterexample 1)

Generated on 2018-10-15 15:16:14 by CPAchecker 1.7-svn

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

-V-
{{line.desc}}
1
extern void __VERIFIER_error() __attribute__ ((__noreturn__));  
2
  
3
  
4
extern void __assert_fail (__const char *__assertion, __const char *__file,  
5
      unsigned int __line, __const char *__function)  
6
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
7
extern void __assert_perror_fail (int __errnum, __const char *__file,  
8
      unsigned int __line,  
9
      __const char *__function)  
10
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
11
extern void __assert (const char *__assertion, const char *__file, int __line)  
12
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
13
  
14
typedef unsigned int size_t;  
15
  
16
  
17
  
18
  
19
struct list_head {  
20
   struct list_head *next ;  
21
   struct list_head *prev ;  
22
};  
23
struct node {  
24
   int value ;  
25
   struct list_head linkage ;  
26
   struct list_head nested ;  
27
};  
28
extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;  
29
extern __attribute__((__nothrow__)) void free(void *__ptr ) ;  
30
extern __attribute__((__nothrow__, __noreturn__)) void abort(void) ;  
31
extern int __VERIFIER_nondet_int(void);  
32
static void fail(void)  
33
{  
34
  {  
35
  ERROR: __VERIFIER_error();((0) ? (void) (0) : __assert_fail ("0", "test-0180.c", 11, __PRETTY_FUNCTION__));  
36
  goto ERROR;  
37
}  
38
}  
39
  
40
  
41
struct list_head gl_list = {& gl_list, & gl_list};  
42
  
43
static void inspect(struct list_head const *head )  
44
{ struct node const *node ;  
45
  unsigned int __cil_tmp3 ;  
46
  struct list_head *__cil_tmp4 ;  
47
  unsigned int __cil_tmp5 ;  
48
  int __cil_tmp6 ;  
49
  unsigned int __cil_tmp7 ;  
50
  unsigned int __cil_tmp8 ;  
51
  unsigned int __cil_tmp9 ;  
52
  struct list_head *__cil_tmp10 ;  
53
  unsigned int __cil_tmp11 ;  
54
  int __cil_tmp12 ;  
55
  unsigned int __cil_tmp13 ;  
56
  unsigned int __cil_tmp14 ;  
57
  struct list_head *__cil_tmp15 ;  
58
  unsigned int __cil_tmp16 ;  
59
  struct list_head *__cil_tmp17 ;  
60
  unsigned int __cil_tmp18 ;  
61
  int __cil_tmp19 ;  
62
  unsigned int __cil_tmp20 ;  
63
  unsigned int __cil_tmp21 ;  
64
  unsigned int __cil_tmp22 ;  
65
  struct list_head *__cil_tmp23 ;  
66
  unsigned int __cil_tmp24 ;  
67
  int __cil_tmp25 ;  
68
  struct node *__cil_tmp26 ;  
69
  unsigned int __cil_tmp27 ;  
70
  unsigned int __cil_tmp28 ;  
71
  struct list_head *__cil_tmp29 ;  
72
  unsigned long __cil_tmp30 ;  
73
  char *__cil_tmp31 ;  
74
  char *__cil_tmp32 ;  
75
  struct node *__cil_tmp33 ;  
76
  unsigned int __cil_tmp34 ;  
77
  unsigned int __cil_tmp35 ;  
78
  struct list_head const *__cil_tmp36 ;  
79
  unsigned int __cil_tmp37 ;  
80
  unsigned int __cil_tmp38 ;  
81
  unsigned int __cil_tmp39 ;  
82
  struct list_head *__cil_tmp40 ;  
83
  unsigned int __cil_tmp41 ;  
84
  int __cil_tmp42 ;  
85
  unsigned int __cil_tmp43 ;  
86
  unsigned int __cil_tmp44 ;  
87
  struct list_head const *__cil_tmp45 ;  
88
  unsigned int __cil_tmp46 ;  
89
  unsigned int __cil_tmp47 ;  
90
  unsigned int __cil_tmp48 ;  
91
  unsigned int __cil_tmp49 ;  
92
  struct list_head *__cil_tmp50 ;  
93
  unsigned int __cil_tmp51 ;  
94
  int __cil_tmp52 ;  
95
  unsigned int __cil_tmp53 ;  
96
  unsigned int __cil_tmp54 ;  
97
  struct list_head const *__cil_tmp55 ;  
98
  unsigned int __cil_tmp56 ;  
99
  unsigned int __cil_tmp57 ;  
100
  unsigned int __cil_tmp58 ;  
101
  struct list_head *__cil_tmp59 ;  
102
  unsigned int __cil_tmp60 ;  
103
  int __cil_tmp61 ;  
104
  unsigned int __cil_tmp62 ;  
105
  unsigned int __cil_tmp63 ;  
106
  struct list_head const *__cil_tmp64 ;  
107
  unsigned int __cil_tmp65 ;  
108
  unsigned int __cil_tmp66 ;  
109
  unsigned int __cil_tmp67 ;  
110
  unsigned int __cil_tmp68 ;  
111
  struct list_head *__cil_tmp69 ;  
112
  unsigned int __cil_tmp70 ;  
113
  int __cil_tmp71 ;  
114
  struct node const *__cil_tmp72 ;  
115
  unsigned int __cil_tmp73 ;  
116
  unsigned int __cil_tmp74 ;  
117
  int __cil_tmp75 ;  
118
  unsigned int __cil_tmp76 ;  
119
  unsigned int __cil_tmp77 ;  
120
  struct list_head const *__cil_tmp78 ;  
121
  struct node const *__cil_tmp79 ;  
122
  unsigned int __cil_tmp80 ;  
123
  unsigned int __cil_tmp81 ;  
124
  int __cil_tmp82 ;  
125
  int const *__cil_tmp83 ;  
126
  struct node const *__cil_tmp84 ;  
127
  unsigned int __cil_tmp85 ;  
128
  unsigned int __cil_tmp86 ;  
129
  int __cil_tmp87 ;  
130
  unsigned int __cil_tmp88 ;  
131
  unsigned int __cil_tmp89 ;  
132
  struct list_head *__cil_tmp90 ;  
133
  unsigned int __cil_tmp91 ;  
134
  unsigned int __cil_tmp92 ;  
135
  struct list_head *__cil_tmp93 ;  
136
  unsigned int __cil_tmp94 ;  
137
  unsigned int __cil_tmp95 ;  
138
  int __cil_tmp96 ;  
139
  unsigned int __cil_tmp97 ;  
140
  unsigned int __cil_tmp98 ;  
141
  unsigned int __cil_tmp99 ;  
142
  struct list_head *__cil_tmp100 ;  
143
  struct list_head *__cil_tmp101 ;  
144
  unsigned int __cil_tmp102 ;  
145
  unsigned int __cil_tmp103 ;  
146
  int __cil_tmp104 ;  
147
  struct list_head *__cil_tmp105 ;  
148
  unsigned int __cil_tmp106 ;  
149
  unsigned int __cil_tmp107 ;  
150
  unsigned int __cil_tmp108 ;  
151
  struct list_head const *__cil_tmp109 ;  
152
  unsigned int __cil_tmp110 ;  
153
  struct list_head *__cil_tmp111 ;  
154
  unsigned int __cil_tmp112 ;  
155
  struct node *__cil_tmp113 ;  
156
  unsigned int __cil_tmp114 ;  
157
  unsigned int __cil_tmp115 ;  
158
  struct list_head *__cil_tmp116 ;  
159
  unsigned long __cil_tmp117 ;  
160
  char *__cil_tmp118 ;  
161
  char *__cil_tmp119 ;  
162
  struct node *__cil_tmp120 ;  
163
  unsigned int __cil_tmp121 ;  
164
  int __cil_tmp122 ;  
165
  
166
  {  
167
  {  
168
  while (1) {  
169
    while_0_continue: ;  
170
    if (! head) {  
171
      {  
172
      fail();  
173
      }  
174
    } else {  
175
    }  
176
    goto while_0_break;  
177
  }  
178
  while_0_break: ;  
179
  }  
180
  {  
181
  while (1) {  
182
    while_1_continue: ;  
183
    {  
184
    __cil_tmp3 = (unsigned int )head;  
185
    __cil_tmp4 = *((struct list_head * const *)head);  
186
    __cil_tmp5 = (unsigned int )__cil_tmp4;  
187
    __cil_tmp6 = __cil_tmp5 != __cil_tmp3;  
188
    if (! __cil_tmp6) {  
189
      {  
190
      fail();  
191
      }  
192
    } else {  
193
    }  
194
    }  
195
    goto while_1_break;  
196
  }  
197
  while_1_break: ;  
198
  }  
199
  {  
200
  while (1) {  
201
    while_2_continue: ;  
202
    {  
203
    __cil_tmp7 = (unsigned int )head;  
204
    __cil_tmp8 = (unsigned int )head;  
205
    __cil_tmp9 = __cil_tmp8 + 4;  
206
    __cil_tmp10 = *((struct list_head * const *)__cil_tmp9);  
207
    __cil_tmp11 = (unsigned int )__cil_tmp10;  
208
    __cil_tmp12 = __cil_tmp11 != __cil_tmp7;  
209
    if (! __cil_tmp12) {  
210
      {  
211
      fail();  
212
      }  
213
    } else {  
214
    }  
215
    }  
216
    goto while_2_break;  
217
  }  
218
  while_2_break: ;  
219
  }  
220
  __cil_tmp13 = (unsigned int )head;  
221
  __cil_tmp14 = __cil_tmp13 + 4;  
222
  __cil_tmp15 = *((struct list_head * const *)__cil_tmp14);  
223
  head = (struct list_head const *)__cil_tmp15;  
224
  {  
225
  while (1) {  
226
    while_3_continue: ;  
227
    if (! head) {  
228
      {  
229
      fail();  
230
      }  
231
    } else {  
232
    }  
233
    goto while_3_break;  
234
  }  
235
  while_3_break: ;  
236
  }  
237
  {  
238
  while (1) {  
239
    while_4_continue: ;  
240
    {  
241
    __cil_tmp16 = (unsigned int )head;  
242
    __cil_tmp17 = *((struct list_head * const *)head);  
243
    __cil_tmp18 = (unsigned int )__cil_tmp17;  
244
    __cil_tmp19 = __cil_tmp18 != __cil_tmp16;  
245
    if (! __cil_tmp19) {  
246
      {  
247
      fail();  
248
      }  
249
    } else {  
250
    }  
251
    }  
252
    goto while_4_break;  
253
  }  
254
  while_4_break: ;  
255
  }  
256
  {  
257
  while (1) {  
258
    while_5_continue: ;  
259
    {  
260
    __cil_tmp20 = (unsigned int )head;  
261
    __cil_tmp21 = (unsigned int )head;  
262
    __cil_tmp22 = __cil_tmp21 + 4;  
263
    __cil_tmp23 = *((struct list_head * const *)__cil_tmp22);  
264
    __cil_tmp24 = (unsigned int )__cil_tmp23;  
265
    __cil_tmp25 = __cil_tmp24 != __cil_tmp20;  
266
    if (! __cil_tmp25) {  
267
      {  
268
      fail();  
269
      }  
270
    } else {  
271
    }  
272
    }  
273
    goto while_5_break;  
274
  }  
275
  while_5_break: ;  
276
  }  
277
  __cil_tmp26 = (struct node *)0;  
278
  __cil_tmp27 = (unsigned int )__cil_tmp26;  
279
  __cil_tmp28 = __cil_tmp27 + 4;  
280
  __cil_tmp29 = (struct list_head *)__cil_tmp28;  
281
  __cil_tmp30 = (unsigned long )__cil_tmp29;  
282
  __cil_tmp31 = (char *)head;  
283
  __cil_tmp32 = __cil_tmp31 - __cil_tmp30;  
284
  __cil_tmp33 = (struct node *)__cil_tmp32;  
285
  node = (struct node const *)__cil_tmp33;  
286
  {  
287
  while (1) {  
288
    while_6_continue: ;  
289
    if (! node) {  
290
      {  
291
      fail();  
292
      }  
293
    } else {  
294
    }  
295
    goto while_6_break;  
296
  }  
297
  while_6_break: ;  
298
  }  
299
  {  
300
  while (1) {  
301
    while_7_continue: ;  
302
    {  
303
    __cil_tmp34 = (unsigned int )node;  
304
    __cil_tmp35 = __cil_tmp34 + 12;  
305
    __cil_tmp36 = (struct list_head const *)__cil_tmp35;  
306
    __cil_tmp37 = (unsigned int )__cil_tmp36;  
307
    __cil_tmp38 = (unsigned int )node;  
308
    __cil_tmp39 = __cil_tmp38 + 12;  
309
    __cil_tmp40 = *((struct list_head * const *)__cil_tmp39);  
310
    __cil_tmp41 = (unsigned int )__cil_tmp40;  
311
    __cil_tmp42 = __cil_tmp41 == __cil_tmp37;  
312
    if (! __cil_tmp42) {  
313
      {  
314
      fail();  
315
      }  
316
    } else {  
317
    }  
318
    }  
319
    goto while_7_break;  
320
  }  
321
  while_7_break: ;  
322
  }  
323
  {  
324
  while (1) {  
325
    while_8_continue: ;  
326
    {  
327
    __cil_tmp43 = (unsigned int )node;  
328
    __cil_tmp44 = __cil_tmp43 + 12;  
329
    __cil_tmp45 = (struct list_head const *)__cil_tmp44;  
330
    __cil_tmp46 = (unsigned int )__cil_tmp45;  
331
    __cil_tmp47 = 12 + 4;  
332
    __cil_tmp48 = (unsigned int )node;  
333
    __cil_tmp49 = __cil_tmp48 + __cil_tmp47;  
334
    __cil_tmp50 = *((struct list_head * const *)__cil_tmp49);  
335
    __cil_tmp51 = (unsigned int )__cil_tmp50;  
336
    __cil_tmp52 = __cil_tmp51 == __cil_tmp46;  
337
    if (! __cil_tmp52) {  
338
      {  
339
      fail();  
340
      }  
341
    } else {  
342
    }  
343
    }  
344
    goto while_8_break;  
345
  }  
346
  while_8_break: ;  
347
  }  
348
  {  
349
  while (1) {  
350
    while_9_continue: ;  
351
    {  
352
    __cil_tmp53 = (unsigned int )node;  
353
    __cil_tmp54 = __cil_tmp53 + 4;  
354
    __cil_tmp55 = (struct list_head const *)__cil_tmp54;  
355
    __cil_tmp56 = (unsigned int )__cil_tmp55;  
356
    __cil_tmp57 = (unsigned int )node;  
357
    __cil_tmp58 = __cil_tmp57 + 12;  
358
    __cil_tmp59 = *((struct list_head * const *)__cil_tmp58);  
359
    __cil_tmp60 = (unsigned int )__cil_tmp59;  
360
    __cil_tmp61 = __cil_tmp60 != __cil_tmp56;  
361
    if (! __cil_tmp61) {  
362
      {  
363
      fail();  
364
      }  
365
    } else {  
366
    }  
367
    }  
368
    goto while_9_break;  
369
  }  
370
  while_9_break: ;  
371
  }  
372
  {  
373
  while (1) {  
374
    while_10_continue: ;  
375
    {  
376
    __cil_tmp62 = (unsigned int )node;  
377
    __cil_tmp63 = __cil_tmp62 + 4;  
378
    __cil_tmp64 = (struct list_head const *)__cil_tmp63;  
379
    __cil_tmp65 = (unsigned int )__cil_tmp64;  
380
    __cil_tmp66 = 12 + 4;  
381
    __cil_tmp67 = (unsigned int )node;  
382
    __cil_tmp68 = __cil_tmp67 + __cil_tmp66;  
383
    __cil_tmp69 = *((struct list_head * const *)__cil_tmp68);  
384
    __cil_tmp70 = (unsigned int )__cil_tmp69;  
385
    __cil_tmp71 = __cil_tmp70 != __cil_tmp65;  
386
    if (! __cil_tmp71) {  
387
      {  
388
      fail();  
389
      }  
390
    } else {  
391
    }  
392
    }  
393
    goto while_10_break;  
394
  }  
395
  while_10_break: ;  
396
  }  
397
  {  
398
  while (1) {  
399
    while_11_continue: ;  
400
    {  
401
    __cil_tmp72 = (struct node const *)head;  
402
    __cil_tmp73 = (unsigned int )__cil_tmp72;  
403
    __cil_tmp74 = (unsigned int )node;  
404
    __cil_tmp75 = __cil_tmp74 != __cil_tmp73;  
405
    if (! __cil_tmp75) {  
406
      {  
407
      fail();  
408
      }  
409
    } else {  
410
    }  
411
    }  
412
    goto while_11_break;  
413
  }  
414
  while_11_break: ;  
415
  }  
416
  {  
417
  while (1) {  
418
    while_12_continue: ;  
419
    {  
420
    __cil_tmp76 = (unsigned int )node;  
421
    __cil_tmp77 = __cil_tmp76 + 4;  
422
    __cil_tmp78 = (struct list_head const *)__cil_tmp77;  
423
    __cil_tmp79 = (struct node const *)__cil_tmp78;  
424
    __cil_tmp80 = (unsigned int )__cil_tmp79;  
425
    __cil_tmp81 = (unsigned int )node;  
426
    __cil_tmp82 = __cil_tmp81 != __cil_tmp80;  
427
    if (! __cil_tmp82) {  
428
      {  
429
      fail();  
430
      }  
431
    } else {  
432
    }  
433
    }  
434
    goto while_12_break;  
435
  }  
436
  while_12_break: ;  
437
  }  
438
  {  
439
  while (1) {  
440
    while_13_continue: ;  
441
    {  
442
    __cil_tmp83 = (int const *)node;  
443
    __cil_tmp84 = (struct node const *)__cil_tmp83;  
444
    __cil_tmp85 = (unsigned int )__cil_tmp84;  
445
    __cil_tmp86 = (unsigned int )node;  
446
    __cil_tmp87 = __cil_tmp86 == __cil_tmp85;  
447
    if (! __cil_tmp87) {  
448
      {  
449
      fail();  
450
      }  
451
    } else {  
452
    }  
453
    }  
454
    goto while_13_break;  
455
  }  
456
  while_13_break: ;  
457
  }  
458
  {  
459
  while (1) {  
460
    while_14_continue: ;  
461
    {  
462
    __cil_tmp88 = (unsigned int )node;  
463
    __cil_tmp89 = __cil_tmp88 + 4;  
464
    __cil_tmp90 = *((struct list_head * const *)__cil_tmp89);  
465
    __cil_tmp91 = (unsigned int )__cil_tmp90;  
466
    __cil_tmp92 = __cil_tmp91 + 4;  
467
    __cil_tmp93 = *((struct list_head **)__cil_tmp92);  
468
    __cil_tmp94 = (unsigned int )__cil_tmp93;  
469
    __cil_tmp95 = (unsigned int )head;  
470
    __cil_tmp96 = __cil_tmp95 == __cil_tmp94;  
471
    if (! __cil_tmp96) {  
472
      {  
473
      fail();  
474
      }  
475
    } else {  
476
    }  
477
    }  
478
    goto while_14_break;  
479
  }  
480
  while_14_break: ;  
481
  }  
482
  {  
483
  while (1) {  
484
    while_15_continue: ;  
485
    {  
486
    __cil_tmp97 = 4 + 4;  
487
    __cil_tmp98 = (unsigned int )node;  
488
    __cil_tmp99 = __cil_tmp98 + __cil_tmp97;  
489
    __cil_tmp100 = *((struct list_head * const *)__cil_tmp99);  
490
    __cil_tmp101 = *((struct list_head **)__cil_tmp100);  
491
    __cil_tmp102 = (unsigned int )__cil_tmp101;  
492
    __cil_tmp103 = (unsigned int )head;  
493
    __cil_tmp104 = __cil_tmp103 == __cil_tmp102;  
494
    if (! __cil_tmp104) {  
495
      {  
496
      fail();  
497
      }  
498
    } else {  
499
    }  
500
    }  
501
    goto while_15_break;  
502
  }  
503
  while_15_break: ;  
504
  }  
505
  __cil_tmp105 = *((struct list_head * const *)head);  
506
  head = (struct list_head const *)__cil_tmp105;  
507
  {  
508
  while (1) {  
509
    while_16_continue: ;  
510
    {  
511
    __cil_tmp106 = (unsigned int )head;  
512
    __cil_tmp107 = (unsigned int )node;  
513
    __cil_tmp108 = __cil_tmp107 + 4;  
514
    __cil_tmp109 = (struct list_head const *)__cil_tmp108;  
515
    __cil_tmp110 = (unsigned int )__cil_tmp109;  
516
    if (__cil_tmp110 != __cil_tmp106) {  
517
    } else {  
518
      goto while_16_break;  
519
    }  
520
    }  
521
    __cil_tmp111 = *((struct list_head * const *)head);  
522
    head = (struct list_head const *)__cil_tmp111;  
523
  }  
524
  while_16_break: ;  
525
  }  
526
  {  
527
  while (1) {  
528
    while_17_continue: ;  
529
    {  
530
    __cil_tmp112 = (unsigned int )node;  
531
    __cil_tmp113 = (struct node *)0;  
532
    __cil_tmp114 = (unsigned int )__cil_tmp113;  
533
    __cil_tmp115 = __cil_tmp114 + 4;  
534
    __cil_tmp116 = (struct list_head *)__cil_tmp115;  
535
    __cil_tmp117 = (unsigned long )__cil_tmp116;  
536
    __cil_tmp118 = (char *)head;  
537
    __cil_tmp119 = __cil_tmp118 - __cil_tmp117;  
538
    __cil_tmp120 = (struct node *)__cil_tmp119;  
539
    __cil_tmp121 = (unsigned int )__cil_tmp120;  
540
    __cil_tmp122 = __cil_tmp121 == __cil_tmp112;  
541
    if (! __cil_tmp122) {  
542
      {  
543
      fail();  
544
      }  
545
    } else {  
546
    }  
547
    }  
548
    goto while_17_break;  
549
  }  
550
  while_17_break: ;  
551
  }  
552
  return;  
553
}  
554
}  
555
__inline static void __list_add(struct list_head *new , struct list_head *prev , struct list_head *next )  
556
{ unsigned int __cil_tmp4 ;  
557
  unsigned int __cil_tmp5 ;  
558
  unsigned int __cil_tmp6 ;  
559
  unsigned int __cil_tmp7 ;  
560
  {  
561
  __cil_tmp4 = (unsigned int )next;  
562
  __cil_tmp5 = __cil_tmp4 + 4;  
563
  *((struct list_head **)__cil_tmp5) = new;  
564
  *((struct list_head **)new) = next;  
565
  __cil_tmp6 = (unsigned int )new;  
566
  __cil_tmp7 = __cil_tmp6 + 4;  
567
  *((struct list_head **)__cil_tmp7) = prev;  
568
  *((struct list_head **)prev) = new;  
569
  return;  
570
}  
571
}  
572
__inline static void __list_del(struct list_head *prev , struct list_head *next )  
573
{ unsigned int __cil_tmp3 ;  
574
  unsigned int __cil_tmp4 ;  
575
  {  
576
  __cil_tmp3 = (unsigned int )next;  
577
  __cil_tmp4 = __cil_tmp3 + 4;  
578
  *((struct list_head **)__cil_tmp4) = prev;  
579
  *((struct list_head **)prev) = next;  
580
  return;  
581
}  
582
}  
583
__inline static void list_add(struct list_head *new , struct list_head *head )  
584
{ struct list_head *__cil_tmp3 ;  
585
  {  
586
  {  
587
  __cil_tmp3 = *((struct list_head **)head);  
588
  __list_add(new, head, __cil_tmp3);  
589
  }  
590
  return;  
591
}  
592
}  
593
__inline static void list_move(struct list_head *list , struct list_head *head )  
594
{ unsigned int __cil_tmp3 ;  
595
  unsigned int __cil_tmp4 ;  
596
  struct list_head *__cil_tmp5 ;  
597
  struct list_head *__cil_tmp6 ;  
598
  {  
599
  {  
600
  __cil_tmp3 = (unsigned int )list;  
601
  __cil_tmp4 = __cil_tmp3 + 4;  
602
  __cil_tmp5 = *((struct list_head **)__cil_tmp4);  
603
  __cil_tmp6 = *((struct list_head **)list);  
604
  __list_del(__cil_tmp5, __cil_tmp6);  
605
  list_add(list, head);  
606
  }  
607
  return;  
608
}  
609
}  
610
static void gl_insert(int value )  
611
{ struct node *node ;  
612
  void *tmp ;  
613
  unsigned int __cil_tmp4 ;  
614
  unsigned int __cil_tmp5 ;  
615
  unsigned int __cil_tmp6 ;  
616
  struct list_head *__cil_tmp7 ;  
617
  unsigned int __cil_tmp8 ;  
618
  unsigned int __cil_tmp9 ;  
619
  unsigned int __cil_tmp10 ;  
620
  unsigned int __cil_tmp11 ;  
621
  unsigned int __cil_tmp12 ;  
622
  unsigned int __cil_tmp13 ;  
623
  unsigned int __cil_tmp14 ;  
624
  unsigned int __cil_tmp15 ;  
625
  {  
626
  {  
627
  __cil_tmp4 = (unsigned int )20UL;  
628
  tmp = malloc(__cil_tmp4);  
629
  node = (struct node *)tmp;  
630
  }  
631
  if (! node) {  
632
    {  
633
    abort();  
634
    }  
635
  } else {  
636
  }  
637
  {  
638
  *((int *)node) = value;  
639
  __cil_tmp5 = (unsigned int )node;  
640
  __cil_tmp6 = __cil_tmp5 + 4;  
641
  __cil_tmp7 = (struct list_head *)__cil_tmp6;  
642
  list_add(__cil_tmp7, & gl_list);  
643
  }  
644
  {  
645
  while (1) {  
646
    while_18_continue: ;  
647
    __cil_tmp8 = (unsigned int )node;  
648
    __cil_tmp9 = __cil_tmp8 + 12;  
649
    __cil_tmp10 = (unsigned int )node;  
650
    __cil_tmp11 = __cil_tmp10 + 12;  
651
    *((struct list_head **)__cil_tmp9) = (struct list_head *)__cil_tmp11;  
652
    __cil_tmp12 = (unsigned int )node;  
653
    __cil_tmp13 = __cil_tmp12 + 12;  
654
    __cil_tmp14 = (unsigned int )node;  
655
    __cil_tmp15 = __cil_tmp14 + 12;  
656
    *((struct list_head **)__cil_tmp13) = (struct list_head *)__cil_tmp15;  
657
    goto while_18_break;  
658
  }  
659
  while_18_break: ;  
660
  }  
661
  return;  
662
}  
663
}  
664
static void gl_read(void)  
665
{ int tmp ;  
666
  int tmp___0 ;  
667
  {  
668
  {  
669
  while (1) {  
670
    while_19_continue: ;  
671
    {  
672
    tmp = __VERIFIER_nondet_int();  
673
    gl_insert(tmp);  
674
    tmp___0 = __VERIFIER_nondet_int();  
675
    }  
676
    if (tmp___0) {  
677
    } else {  
678
      goto while_19_break;  
679
    }  
680
  }  
681
  while_19_break: ;  
682
  }  
683
  return;  
684
}  
685
}  
686
static void gl_destroy(void)  
687
{ struct list_head *next ;  
688
  struct list_head *__cil_tmp2 ;  
689
  unsigned int __cil_tmp3 ;  
690
  unsigned int __cil_tmp4 ;  
691
  struct list_head *__cil_tmp5 ;  
692
  struct node *__cil_tmp6 ;  
693
  unsigned int __cil_tmp7 ;  
694
  unsigned int __cil_tmp8 ;  
695
  struct list_head *__cil_tmp9 ;  
696
  unsigned long __cil_tmp10 ;  
697
  char *__cil_tmp11 ;  
698
  char *__cil_tmp12 ;  
699
  struct node *__cil_tmp13 ;  
700
  void *__cil_tmp14 ;  
701
  {  
702
  {  
703
  while (1) {  
704
    while_20_continue: ;  
705
    __cil_tmp2 = & gl_list;  
706
    next = *((struct list_head **)__cil_tmp2);  
707
    {  
708
    __cil_tmp3 = (unsigned int )next;  
709
    __cil_tmp4 = (unsigned int )(& gl_list);  
710
    if (__cil_tmp4 != __cil_tmp3) {  
711
    } else {  
712
      goto while_20_break;  
713
    }  
714
    }  
715
    {  
716
    __cil_tmp5 = & gl_list;  
717
    *((struct list_head **)__cil_tmp5) = *((struct list_head **)next);  
718
    __cil_tmp6 = (struct node *)0;  
719
    __cil_tmp7 = (unsigned int )__cil_tmp6;  
720
    __cil_tmp8 = __cil_tmp7 + 4;  
721
    __cil_tmp9 = (struct list_head *)__cil_tmp8;  
722
    __cil_tmp10 = (unsigned long )__cil_tmp9;  
723
    __cil_tmp11 = (char *)next;  
724
    __cil_tmp12 = __cil_tmp11 - __cil_tmp10;  
725
    __cil_tmp13 = (struct node *)__cil_tmp12;  
726
    __cil_tmp14 = (void *)__cil_tmp13;  
727
    free(__cil_tmp14);  
728
    }  
729
  }  
730
  while_20_break: ;  
731
  }  
732
  return;  
733
}  
734
}  
735
static int val_from_node(struct list_head *head )  
736
{ struct node *entry ;  
737
  struct node *__cil_tmp3 ;  
738
  unsigned int __cil_tmp4 ;  
739
  unsigned int __cil_tmp5 ;  
740
  struct list_head *__cil_tmp6 ;  
741
  unsigned long __cil_tmp7 ;  
742
  char *__cil_tmp8 ;  
743
  char *__cil_tmp9 ;  
744
  {  
745
  __cil_tmp3 = (struct node *)0;  
746
  __cil_tmp4 = (unsigned int )__cil_tmp3;  
747
  __cil_tmp5 = __cil_tmp4 + 4;  
748
  __cil_tmp6 = (struct list_head *)__cil_tmp5;  
749
  __cil_tmp7 = (unsigned long )__cil_tmp6;  
750
  __cil_tmp8 = (char *)head;  
751
  __cil_tmp9 = __cil_tmp8 - __cil_tmp7;  
752
  entry = (struct node *)__cil_tmp9;  
753
  return (*((int *)entry));  
754
}  
755
}  
756
static _Bool gl_sort_pass(void)  
757
{ _Bool any_change ;  
758
  struct list_head *pos0 ;  
759
  struct list_head *pos1 ;  
760
  int val0 ;  
761
  int tmp ;  
762
  int val1 ;  
763
  int tmp___0 ;  
764
  struct list_head *__cil_tmp8 ;  
765
  unsigned int __cil_tmp9 ;  
766
  unsigned int __cil_tmp10 ;  
767
  {  
768
  any_change = (_Bool)0;  
769
  __cil_tmp8 = & gl_list;  
770
  pos0 = *((struct list_head **)__cil_tmp8);  
771
  {  
772
  while (1) {  
773
    while_21_continue: ;  
774
    pos1 = *((struct list_head **)pos0);  
775
    {  
776
    __cil_tmp9 = (unsigned int )pos1;  
777
    __cil_tmp10 = (unsigned int )(& gl_list);  
778
    if (__cil_tmp10 != __cil_tmp9) {  
779
    } else {  
780
      goto while_21_break;  
781
    }  
782
    }  
783
    {  
784
    tmp = val_from_node(pos0);  
785
    val0 = tmp;  
786
    tmp___0 = val_from_node(pos1);  
787
    val1 = tmp___0;  
788
    }  
789
    if (val0 <= val1) {  
790
      pos0 = pos1;  
791
      goto while_21_continue;  
792
    } else {  
793
    }  
794
    {  
795
    any_change = (_Bool)1;  
796
    list_move(pos0, pos1);  
797
    }  
798
  }  
799
  while_21_break: ;  
800
  }  
801
  return (any_change);  
802
}  
803
}  
804
static void gl_sort(void)  
805
{ _Bool tmp ;  
806
  {  
807
  {  
808
  while (1) {  
809
    while_22_continue: ;  
810
    {  
811
    tmp = gl_sort_pass();  
812
    }  
813
    if (tmp) {  
814
    } else {  
815
      goto while_22_break;  
816
    }  
817
  }  
818
  while_22_break: ;  
819
  }  
820
  return;  
821
}  
822
}  
823
int main(void)  
824
{ struct list_head const *__cil_tmp1 ;  
825
  struct list_head const *__cil_tmp2 ;  
826
  {  
827
  {  
828
  gl_read();  
829
  __cil_tmp1 = (struct list_head const *)(& gl_list);  
830
  inspect(__cil_tmp1);  
831
  gl_sort();  
832
  __cil_tmp2 = (struct list_head const *)(& gl_list);  
833
  inspect(__cil_tmp2);  
834
  gl_destroy();  
835
  }  
836
  return (0);  
837
}  
838
}  
DateTimeLog LevelLog InfoLog Message
2018-10-1515:16:12:697INFOResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 900s
2018-10-1515:16:12:729INFOCPAchecker.runCPAchecker 1.7-svn (OpenJDK 64-Bit Server VM 1.8.0_181) started
2018-10-1515:16:13:791WARNINGPredicateCPA:JavaSMT:Mathsat5SolverContext.<init>MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-10-1515:16:13:853INFOPredicateCPA:PredicateCPA.<init>Using predicate analysis with MathSAT5 version 5.5.2 (850e644d5107) (May 22 2018 13:53:37, gmp 6.1.0, gcc 4.8.5, 64-bit, reentrant) and JFactory 1.21.
2018-10-1515:16:13:912WARNINGARGCPA:JavaSMT:Mathsat5SolverContext.<init>MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-10-1515:16:13:917WARNINGARGCPA:JavaSMT:Mathsat5SolverContext.<init>MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-10-1515:16:13:983INFOPredicateCPA:PredicateCPARefiner.<init>Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2018-10-1515:16:13:996INFOCPAchecker.runAlgorithmStarting analysis ...
2018-10-1515:16:14:524INFOCPAchecker.runAlgorithmStopping analysis ...
Statistics NameStatistics ValueAdditional Value
PredicateCPA statistics
Number of abstractions 14 2% of all post computations
Times abstraction was reused 0
Because of function entry/exit 0 0%
Because of loop head 11 79%
Because of join nodes 0 0%
Because of threshold 0 0%
Because of target state 3 21%
Times precision was empty 9 64%
Times precision was {false} 3 21%
Times result was cached 0 0%
Times cartesian abs was used 0 0%
Times boolean abs was used 2 14%
Times result was 'false' 2 14%
Number of strengthen sat checks 0
Number of coverage checks 3
BDD entailment checks 3
Number of SMT sat checks 0
trivial 0
cached 0
Max ABE block size 188
Number of predicates discovered 18
Number of abstraction locations 2
Max number of predicates per location 1
Avg number of predicates per location 1
Total predicates per abstraction 5
Max number of predicates per abstraction 1
Avg number of predicates per abstraction 1.00
Number of irrelevant predicates 3 60%
Number of preds handled by boolean abs 2 40%
Total number of models for allsat 2
Max number of models for allsat 1
Avg number of models for allsat 1.00
Time for post operator 0.126s
Time for path formula creation 0.104s
Time for strengthen operator 0.005s
Time for prec operator 0.061s
Time for abstraction 0.055s Max: 0.034s, Count: 14
Boolean abstraction 0.006s
Solving time 0.043s Max: 0.031s
Model enumeration time 0.000s
Time for BDD construction 0.000s Max: 0.000s
Time for coverage check 0.004s
Time for BDD entailment checks 0.004s
Total time for SMT solver (w/o itp) 0.043s
Number of path formula cache hits 498 49%
Inside post operator
Inside path formula creation
Time for path formula computation 0.120s
Total number of created targets for pointer analysis 0
Number of BDD nodes 202
Size of BDD node table 55949
Size of BDD cache 5623
Size of BDD node cleanup queue 0.00 sum: 0, count: 111, min: 0, max: 0
Time for BDD node cleanup 0.000s
Time for BDD garbage collection 0.000s in 0 runs
KeyValue statistics
Init. function predicates 0
Init. global predicates 0
Init. location predicates 0
Invariant Generation statistics
AutomatonAnalysis (SVCOMP) statistics
Number of states 1
Total time for successor computation 0.014s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 734, count: 737, min: 0, max: 1 [0 x 3, 1 x 734]
CPA algorithm statistics
Number of iterations 155
Max size of waitlist 2
Average size of waitlist 1
ReversePostorderSortedWaitlist 0.00 sum: 0, count: 430, min: 0, max: 0
CallstackSortedWaitlist 13.33 sum: 40, count: 3, min: 6, max: 22
Number of computed successors 163
Max successors for one state 2
Number of times merged 0
Number of times stopped 3
Number of times breaked 3
Total time for CPA algorithm 0.288s Max: 0.144s
Time for choose from waitlist 0.005s
Time for precision adjustment 0.074s
Time for transfer relation 0.191s
Time for merge operator 0.001s
Time for stop operator 0.006s
Time for adding to reached set 0.004s
Static Predicate Refiner statistics
Number of predicates found statically 16 count: 1, min: 16, max: 16, avg: 16.00
Total time for static refinement 0.062s
Time for path feasibility check 0.021s
Time for predicate extraction from CFA 0.027s
Time for ARG update 0.005s
PredicateCPARefiner statistics
Number of predicate refinements 2
Avg. length of target path (in blocks) 3.00 sum: 6, count: 2, min: 3, max: 3
Number of infeasible sliced prefixes 0 count: 0, min: 0, max: 0, avg: 0.00
Time for refinement 0.156s
Counterexample analysis 0.075s Max: 0.034s, Calls: 3
Refinement sat check 0.042s
Interpolant computation 0.000s
Path-formulas extraction 0.000s
Error path post-processing 0.094s
Predicate-Abstraction Refiner statistics
Predicate creation 0.000s
Precision update 0.001s
ARG update 0.001s
Length of refined path (in blocks) 2.00 sum: 2, count: 1, min: 2, max: 2
Number of affected states 1 count: 1, min: 1, max: 1, avg: 1.00
Length (states) of path with itp 'true' 0 count: 1, min: 0, max: 0, avg: 0.00
Length (states) of path with itp non-trivial itp 1 count: 1, min: 1, max: 1, avg: 1.00
Length (states) of path with itp 'false' 1 count: 1, min: 1, max: 1, avg: 1.00
Different non-trivial interpolants along paths 0 count: 1, min: 0, max: 0, avg: 0.00
Equal non-trivial interpolants along paths 0 count: 1, min: 0, max: 0, avg: 0.00
Number of refs with location-based cutoff 0
CEGAR algorithm statistics
Number of refinements 3
Number of successful refinements 2
Number of failed refinements 0
Max. size of reached set before ref. 67
Max. size of reached set after ref. 5
Avg. size of reached set before ref. 55.00
Avg. size of reached set after ref. 3.00
Total time for CEGAR algorithm 0.527s
Time for refinements 0.238s
Average time for refinement 0.079s
Max time for refinement 0.130s
Code Coverage
Function coverage 0.538
Visited lines 230
Total lines 553
Line coverage 0.416
Visited conditions 10
Total conditions 48
Condition coverage 0.208
CPAchecker general statistics
Number of program locations 665
Number of CFA edges (per node) 674 count: 665, min: 0, max: 2, avg: 1.01
Number of relevant variables 189
Number of functions 13
Number of loops (and loop nodes) 6 sum: 68, min: 3, max: 21, avg: 11.33
Size of reached set 67
Number of reached locations 63 9%
Avg states per location 1
Max states per location 3 at node N1
Number of reached functions 7 54%
Number of partitions 67
Avg size of partitions 1
Max size of partitions 1
Number of target states 1
Size of final wait list 2
Time for analysis setup 1.258s
Time for loading CPAs 0.451s
Time for loading parser 0.195s
Time for CFA construction 0.530s
Time for parsing file(s) 0.241s
Time for AST to CFA 0.127s
Time for CFA sanity check 0.013s
Time for post-processing 0.120s
Time for CFA export 0.892s
Time for function pointers resolving 0.003s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for var class. 0.073s
Time for collecting variables 0.032s
Time for solving dependencies 0.001s
Time for building hierarchy 0.000s
Time for building classification 0.031s
Time for exporting data 0.009s
Time for Analysis 0.527s
CPU time for analysis 1.620s
Time for analyzing result 0.000s
Total time for CPAchecker 1.786s
Total CPU time for CPAchecker 4.980s
Time for statistics 0.281s
Time for Garbage Collector 0.075s in 3 runs
Garbage Collector(s) used PS MarkSweep, PS Scavenge
Used heap memory 126MB ( 120 MiB) max; 70MB ( 67 MiB) avg; 165MB ( 157 MiB) peak
Used non-heap memory 42MB ( 40 MiB) max; 29MB ( 28 MiB) avg; 49MB ( 46 MiB) peak
Used in PS Old Gen pool 15MB ( 14 MiB) max; 6MB ( 6 MiB) avg; 15MB ( 14 MiB) peak
Allocated heap memory 504MB ( 481 MiB) max; 493MB ( 470 MiB) avg
Allocated non-heap memory 44MB ( 42 MiB) max; 30MB ( 29 MiB) avg
Total process virtual memory 4084MB ( 3895 MiB) max; 3939MB ( 3756 MiB) avg
#Configuration NameConfiguration Value
1analysis.algorithm.CEGAR true
2analysis.entryFunction main
3analysis.programNames test/programs/benchmarks/loops/bubble_sort_false-unreach-call.i
4analysis.traversal.order bfs
5analysis.traversal.useCallstack true
6analysis.traversal.useReversePostorder true
7ARGCPA.cpa cpa.composite.CompositeCPA
8cegar.refiner cpa.predicate.PredicateRefiner
9CompositeCPA.cpas cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.functionpointer.FunctionPointerCPA, cpa.predicate.PredicateCPA
10cpa cpa.arg.ARGCPA
11cpa.composite.aggregateBasicBlocks true
12cpa.predicate.blk.alwaysAtFunctions false
13cpa.predicate.blk.alwaysAtLoops true
14cpa.predicate.refinement.performInitialStaticRefinement true
15limits.time.cpu 900s
16log.level INFO
17specification config/specification/sv-comp-reachability.spc