Project

General

Profile

Bug #8981 » error trace.json

Evgeny Novikov, 06/21/2018 10:32 AM

 
1
{
2
    "actions": [
3
        "Initialize rule models.",
4
        "Start environment model scenarios.",
5
        "Declare auxiliary variables.",
6
        "Trigger module initialization.",
7
        "Initialize the module after insmod with 'ldv_init' function. Invoke callback ldv_init from INSMOD."
8
    ],
9
    "callback actions": [
10
        4
11
    ],
12
    "edges": [
13
        {
14
            "assumption": "__ldv_in_interrupt_context == 0;",
15
            "end line": 25,
16
            "file": 0,
17
            "source": "static bool __ldv_in_interrupt_context = 0;",
18
            "source node": 0,
19
            "start line": 25,
20
            "target node": 1,
21
            "thread": 0
22
        },
23
        {
24
            "end line": 166,
25
            "enter": 0,
26
            "entry_point": "Entry point 'main'",
27
            "file": 1,
28
            "line": 166,
29
            "source": "Begin program execution",
30
            "source node": 1,
31
            "start line": 166,
32
            "target node": 2,
33
            "thread": 1
34
        },
35
        {
36
            "end line": 168,
37
            "enter": 1,
38
            "entry_point": "Main entry point function.",
39
            "file": 1,
40
            "source": "ldv_main_3((void *)0);",
41
            "source node": 2,
42
            "start line": 168,
43
            "target node": 3,
44
            "thread": 3
45
        },
46
        {
47
            "action": 0,
48
            "end line": 143,
49
            "file": 1,
50
            "source": "ldv_initialize();",
51
            "source node": 3,
52
            "start line": 143,
53
            "target node": 4,
54
            "thread": 3
55
        },
56
        {
57
            "action": 1,
58
            "end line": 147,
59
            "enter": 2,
60
            "file": 1,
61
            "source": "ldv_dispatch_insmod_register_3_3();",
62
            "source node": 4,
63
            "start line": 147,
64
            "target node": 5,
65
            "thread": 3
66
        },
67
        {
68
            "end line": 77,
69
            "file": 1,
70
            "source": "struct ldv_struct_main_3 *cf_arg_2;",
71
            "source node": 5,
72
            "start line": 77,
73
            "target node": 6,
74
            "thread": 3
75
        },
76
        {
77
            "end line": 77,
78
            "enter": 3,
79
            "file": 1,
80
            "source": "cf_arg_2 = (struct ldv_struct_main_3 *)ldv_xmalloc(4UL);",
81
            "source node": 6,
82
            "start line": 77,
83
            "target node": 7,
84
            "thread": 3
85
        },
86
        {
87
            "assumption": "size == 4UL;",
88
            "assumption scope": 3,
89
            "end line": 69,
90
            "file": 2,
91
            "source": "void *res;",
92
            "source node": 7,
93
            "start line": 69,
94
            "target node": 8,
95
            "thread": 3
96
        },
97
        {
98
            "end line": 69,
99
            "file": 2,
100
            "source": "res = malloc(size);",
101
            "source node": 8,
102
            "start line": 69,
103
            "target node": 9,
104
            "thread": 3
105
        },
106
        {
107
            "end line": 71,
108
            "file": 2,
109
            "source": "[__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));]",
110
            "source node": 9,
111
            "start line": 71,
112
            "target node": 10,
113
            "thread": 3
114
        },
115
        {
116
            "end line": 72,
117
            "enter": 4,
118
            "file": 2,
119
            "source": "[__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);]",
120
            "source node": 10,
121
            "start line": 72,
122
            "target node": 11,
123
            "thread": 3
124
        },
125
        {
126
            "end line": 22,
127
            "file": 3,
128
            "return": 4,
129
            "source": "return (unsigned long)ptr > 4294967295UL;",
130
            "source node": 11,
131
            "start line": 22,
132
            "target node": 12,
133
            "thread": 3
134
        },
135
        {
136
            "end line": 74,
137
            "file": 2,
138
            "return": 3,
139
            "source": "return res;",
140
            "source node": 12,
141
            "start line": 74,
142
            "target node": 13,
143
            "thread": 3
144
        },
145
        {
146
            "end line": 78,
147
            "enter": 5,
148
            "entry_point": "Initialize or exit module.",
149
            "file": 1,
150
            "source": "ldv_insmod_2((void *)cf_arg_2);",
151
            "source node": 13,
152
            "start line": 78,
153
            "target node": 14,
154
            "thread": 2
155
        },
156
        {
157
            "action": 2,
158
            "end line": 85,
159
            "file": 1,
160
            "source": "void (*ldv_2_exit_default)(void);",
161
            "source node": 14,
162
            "start line": 85,
163
            "target node": 15,
164
            "thread": 2
165
        },
166
        {
167
            "action": 2,
168
            "end line": 86,
169
            "file": 1,
170
            "source": "int (*ldv_2_ldv_init_default)(void);",
171
            "source node": 15,
172
            "start line": 86,
173
            "target node": 16,
174
            "thread": 2
175
        },
176
        {
177
            "action": 2,
178
            "end line": 87,
179
            "file": 1,
180
            "source": "int ldv_2_ret_default;",
181
            "source node": 16,
182
            "start line": 87,
183
            "target node": 17,
184
            "thread": 2
185
        },
186
        {
187
            "action": 3,
188
            "end line": 94,
189
            "enter": 6,
190
            "file": 1,
191
            "source": "ldv_free(arg0);",
192
            "source node": 17,
193
            "start line": 94,
194
            "target node": 18,
195
            "thread": 2
196
        },
197
        {
198
            "end line": 64,
199
            "file": 2,
200
            "source": "free(s);",
201
            "source node": 18,
202
            "start line": 64,
203
            "target node": 19,
204
            "thread": 2
205
        },
206
        {
207
            "end line": 65,
208
            "file": 2,
209
            "return": 6,
210
            "source": "return;",
211
            "source node": 19,
212
            "start line": 65,
213
            "target node": 20,
214
            "thread": 2
215
        },
216
        {
217
            "action": 4,
218
            "end line": 99,
219
            "enter": 8,
220
            "file": 4,
221
            "original file": 1,
222
            "original start line": 99,
223
            "source": "ldv_2_ret_default = ldv_init();",
224
            "source node": 20,
225
            "start line": 23,
226
            "target node": 21,
227
            "thread": 2
228
        },
229
        {
230
            "end line": 23,
231
            "file": 4,
232
            "note": "int **buf ;",
233
            "source": "int **buf;",
234
            "source node": 21,
235
            "start line": 23,
236
            "target node": 22,
237
            "thread": 2
238
        },
239
        {
240
            "end line": 24,
241
            "file": 4,
242
            "note": "int i ;",
243
            "source": "int i;",
244
            "source node": 22,
245
            "start line": 24,
246
            "target node": 23,
247
            "thread": 2
248
        },
249
        {
250
            "end line": 25,
251
            "enter": 9,
252
            "file": 4,
253
            "note": "tmp = kzalloc(40UL, 208U);",
254
            "source": "kzalloc(40UL, 208U) = kzalloc(40UL, 208U);",
255
            "source node": 23,
256
            "start line": 25,
257
            "target node": 24,
258
            "thread": 2
259
        },
260
        {
261
            "end line": 280,
262
            "enter": 10,
263
            "file": 1,
264
            "note": "tmp = ldv_kzalloc(size, flags);",
265
            "source": "ldv_kzalloc(size, flags) = ldv_kzalloc(size, flags);",
266
            "source node": 24,
267
            "start line": 280,
268
            "target node": 25,
269
            "thread": 2
270
        },
271
        {
272
            "assumption": "size == 40UL; flags == 208U;",
273
            "assumption scope": 10,
274
            "end line": 23,
275
            "file": 5,
276
            "note": "void *res ;",
277
            "source": "void *res;",
278
            "source node": 25,
279
            "start line": 23,
280
            "target node": 26,
281
            "thread": 2
282
        },
283
        {
284
            "end line": 25,
285
            "file": 5,
286
            "source": "ldv_check_alloc_flags(flags);",
287
            "source node": 26,
288
            "start line": 25,
289
            "target node": 27,
290
            "thread": 2
291
        },
292
        {
293
            "end line": 26,
294
            "enter": 11,
295
            "file": 5,
296
            "note": "res = ldv_zalloc(size);",
297
            "source": "res = ldv_zalloc(size);",
298
            "source node": 27,
299
            "start line": 26,
300
            "target node": 28,
301
            "thread": 2
302
        },
303
        {
304
            "end line": 59,
305
            "enter": 12,
306
            "file": 2,
307
            "note": "tmp = ldv_calloc(1UL, size);",
308
            "source": "ldv_calloc(1UL, size) = ldv_calloc(1UL, size);",
309
            "source node": 28,
310
            "start line": 59,
311
            "target node": 29,
312
            "thread": 2
313
        },
314
        {
315
            "assumption": "nmemb == 1UL; size == 40UL;",
316
            "assumption scope": 12,
317
            "end line": 45,
318
            "file": 2,
319
            "note": "void *res ;",
320
            "source": "void *res;",
321
            "source node": 29,
322
            "start line": 45,
323
            "target node": 30,
324
            "thread": 2
325
        },
326
        {
327
            "condition": true,
328
            "end line": 45,
329
            "enter": 13,
330
            "file": 2,
331
            "source": "ldv_undef_int() != 0",
332
            "source node": 30,
333
            "start line": 45,
334
            "target node": 31,
335
            "thread": 2
336
        },
337
        {
338
            "end line": 43,
339
            "file": 6,
340
            "return": 13,
341
            "source": "return __VERIFIER_nondet_int();",
342
            "source node": 31,
343
            "start line": 43,
344
            "target node": 32,
345
            "thread": 2
346
        },
347
        {
348
            "assumption": "(*((signed long long int *)tmp)) == 0LL;",
349
            "assumption scope": 12,
350
            "end line": 46,
351
            "file": 2,
352
            "note": "res = tmp;",
353
            "source": "res = calloc(nmemb, size);",
354
            "source node": 32,
355
            "start line": 46,
356
            "target node": 33,
357
            "thread": 2
358
        },
359
        {
360
            "end line": 48,
361
            "file": 2,
362
            "source": "[__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));]",
363
            "source node": 33,
364
            "start line": 48,
365
            "target node": 34,
366
            "thread": 2
367
        },
368
        {
369
            "end line": 49,
370
            "enter": 4,
371
            "file": 2,
372
            "source": "[__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);]",
373
            "source node": 34,
374
            "start line": 49,
375
            "target node": 35,
376
            "thread": 2
377
        },
378
        {
379
            "assumption": "(*((signed long long int *)ptr)) == 0LL;",
380
            "assumption scope": 4,
381
            "end line": 22,
382
            "file": 3,
383
            "return": 4,
384
            "source": "return (unsigned long)ptr > 4294967295UL;",
385
            "source node": 35,
386
            "start line": 22,
387
            "target node": 36,
388
            "thread": 2
389
        },
390
        {
391
            "end line": 51,
392
            "file": 2,
393
            "note": "return (res);",
394
            "return": 12,
395
            "source": "return res;",
396
            "source node": 36,
397
            "start line": 51,
398
            "target node": 37,
399
            "thread": 2
400
        },
401
        {
402
            "end line": 59,
403
            "file": 2,
404
            "note": "return (tmp);",
405
            "return": 11,
406
            "source": "return tmp;",
407
            "source node": 37,
408
            "start line": 59,
409
            "target node": 38,
410
            "thread": 2
411
        },
412
        {
413
            "end line": 26,
414
            "file": 5,
415
            "note": "res = ldv_zalloc(size);",
416
            "source": "res = ldv_zalloc(size);",
417
            "source node": 38,
418
            "start line": 26,
419
            "target node": 39,
420
            "thread": 2
421
        },
422
        {
423
            "end line": 27,
424
            "enter": 14,
425
            "file": 5,
426
            "source": "ldv_after_alloc(res);",
427
            "source node": 39,
428
            "start line": 27,
429
            "target node": 40,
430
            "thread": 2
431
        },
432
        {
433
            "assumption": "(*((signed long long int *)res)) == 0LL;",
434
            "assumption scope": 14,
435
            "end line": 20,
436
            "file": 7,
437
            "return": 14,
438
            "source": "return;",
439
            "source node": 40,
440
            "start line": 20,
441
            "target node": 41,
442
            "thread": 2
443
        },
444
        {
445
            "end line": 29,
446
            "file": 5,
447
            "note": "return (res);",
448
            "return": 10,
449
            "source": "return res;",
450
            "source node": 41,
451
            "start line": 29,
452
            "target node": 42,
453
            "thread": 2
454
        },
455
        {
456
            "end line": 280,
457
            "file": 1,
458
            "note": "return (tmp);",
459
            "return": 9,
460
            "source": "return tmp;",
461
            "source node": 42,
462
            "start line": 280,
463
            "target node": 43,
464
            "thread": 2
465
        },
466
        {
467
            "end line": 25,
468
            "file": 4,
469
            "note": "buf = (int **)tmp;",
470
            "source": "buf = (int **)tmp;",
471
            "source node": 43,
472
            "start line": 25,
473
            "target node": 44,
474
            "thread": 2
475
        },
476
        {
477
            "condition": true,
478
            "end line": 26,
479
            "file": 4,
480
            "source": "((unsigned long)buf) != ((unsigned long)((int **)0))",
481
            "source node": 44,
482
            "start line": 26,
483
            "target node": 45,
484
            "thread": 2
485
        },
486
        {
487
            "end line": 29,
488
            "file": 4,
489
            "source": "i = *(*(buf + 9UL));",
490
            "source node": 45,
491
            "start line": 29,
492
            "target node": 46,
493
            "thread": 2,
494
            "warn": "Field with 8 byte size can't be read from offset 72 byte of object 40 byte size"
495
        }
496
    ],
497
    "entry node": 0,
498
    "files": [
499
        "linux/ldv/common.c",
500
        "klever-core-work-dir/0/tests/generic/memory/generic-memory/vtg/ext-modules/generic/memory/zalloc.ko/generic:memory/weaver/.tmp_zalloc.c.aux",
501
        "verifier/memory.c",
502
        "linux/err.c",
503
        "ext-modules/generic/memory/zalloc.c",
504
        "linux/mm/kzalloc.c",
505
        "verifier/nondet.c",
506
        "generic/memory.c"
507
    ],
508
    "funcs": [
509
        "main",
510
        "ldv_main_3",
511
        "ldv_dispatch_insmod_register_3_3",
512
        "ldv_xmalloc",
513
        "ldv_is_err",
514
        "ldv_insmod_2",
515
        "ldv_free",
516
        "ldv_insmod_ldv_init_2_5",
517
        "ldv_init",
518
        "kzalloc",
519
        "ldv_kzalloc",
520
        "ldv_zalloc",
521
        "ldv_calloc",
522
        "ldv_undef_int",
523
        "ldv_after_alloc",
524
        "ldv_switch_to_interrupt_context",
525
        "ldv_switch_to_process_context",
526
        "ldv_dispatch_insmod_deregister_3_2",
527
        "ERR_PTR",
528
        "PTR_ERR",
529
        "IS_ERR",
530
        "IS_ERR_OR_NULL",
531
        "alloc_pages",
532
        "ldv___get_free_pages_6",
533
        "kmalloc",
534
        "kmalloc_node",
535
        "kcalloc",
536
        "ldv_kmalloc_array_10",
537
        "kmem_cache_zalloc",
538
        "ldv_kmem_cache_alloc_12",
539
        "kzalloc_node",
540
        "ldv_kfree_15"
541
    ],
542
    "nodes": [
543
        [
544
            null,
545
            0
546
        ],
547
        [
548
            0,
549
            1
550
        ],
551
        [
552
            1,
553
            2
554
        ],
555
        [
556
            2,
557
            3
558
        ],
559
        [
560
            3,
561
            4
562
        ],
563
        [
564
            4,
565
            5
566
        ],
567
        [
568
            5,
569
            6
570
        ],
571
        [
572
            6,
573
            7
574
        ],
575
        [
576
            7,
577
            8
578
        ],
579
        [
580
            8,
581
            9
582
        ],
583
        [
584
            9,
585
            10
586
        ],
587
        [
588
            10,
589
            11
590
        ],
591
        [
592
            11,
593
            12
594
        ],
595
        [
596
            12,
597
            13
598
        ],
599
        [
600
            13,
601
            14
602
        ],
603
        [
604
            14,
605
            15
606
        ],
607
        [
608
            15,
609
            16
610
        ],
611
        [
612
            16,
613
            17
614
        ],
615
        [
616
            17,
617
            18
618
        ],
619
        [
620
            18,
621
            19
622
        ],
623
        [
624
            19,
625
            20
626
        ],
627
        [
628
            20,
629
            21
630
        ],
631
        [
632
            21,
633
            22
634
        ],
635
        [
636
            22,
637
            23
638
        ],
639
        [
640
            23,
641
            24
642
        ],
643
        [
644
            24,
645
            25
646
        ],
647
        [
648
            25,
649
            26
650
        ],
651
        [
652
            26,
653
            27
654
        ],
655
        [
656
            27,
657
            28
658
        ],
659
        [
660
            28,
661
            29
662
        ],
663
        [
664
            29,
665
            30
666
        ],
667
        [
668
            30,
669
            31
670
        ],
671
        [
672
            31,
673
            32
674
        ],
675
        [
676
            32,
677
            33
678
        ],
679
        [
680
            33,
681
            34
682
        ],
683
        [
684
            34,
685
            35
686
        ],
687
        [
688
            35,
689
            36
690
        ],
691
        [
692
            36,
693
            37
694
        ],
695
        [
696
            37,
697
            38
698
        ],
699
        [
700
            38,
701
            39
702
        ],
703
        [
704
            39,
705
            40
706
        ],
707
        [
708
            40,
709
            41
710
        ],
711
        [
712
            41,
713
            42
714
        ],
715
        [
716
            42,
717
            43
718
        ],
719
        [
720
            43,
721
            44
722
        ],
723
        [
724
            44,
725
            45
726
        ],
727
        [
728
            45,
729
            null
730
        ]
731
    ],
732
    "violation nodes": [
733
        46
734
    ]
735
}
(2-2/3)