⚲
Project
General
Profile
Sign in
Home
Projects
Help
Search
:
Klever
All Projects
Klever
Overview
Activity
Roadmap
Issues
News
Documents
Wiki
Files
Repository
Download (181 KB)
Bug #8043
» error-trace.json
Evgeny Novikov
, 03/21/2017 03:02 PM
{
"actions"
:
[
"Initialize rule models."
,
"Start environment model scenarios."
,
"Declare auxiliary variables."
,
"Trigger module initialization."
,
"Initialize the module after insmod with 'mm_init' function. Invoke callback mm_init from INSMOD."
,
"Get 'pci' callbacks to register."
,
"Register PCI callbacks."
,
"Begin PCI callbacks invocating."
,
"Allocate memory for pci_dev structure."
,
"Allocate memory for adhoc callback parameters."
,
"Probe new PCI driver. Invoke callback probe from pci_driver."
,
"Failed to allocate an interrupt line for a managed device."
],
"callback actions"
:
[
4
,
10
],
"edges"
:
[
{
"file"
:
1
,
"source"
:
"extern struct module __this_module;"
,
"source node"
:
0
,
"start line"
:
33
,
"target node"
:
1
,
"thread"
:
0
},
{
"file"
:
2
,
"source"
:
"extern struct pv_irq_ops pv_irq_ops;"
,
"source node"
:
1
,
"start line"
:
358
,
"target node"
:
2
,
"thread"
:
0
},
{
"file"
:
3
,
"source"
:
"extern unsigned long volatile jiffies;"
,
"source node"
:
2
,
"start line"
:
77
,
"target node"
:
3
,
"thread"
:
0
},
{
"file"
:
4
,
"source"
:
"extern struct device x86_dma_fallback_dev;"
,
"source node"
:
3
,
"start line"
:
27
,
"target node"
:
4
,
"thread"
:
0
},
{
"file"
:
4
,
"source"
:
"extern struct dma_map_ops *dma_ops;"
,
"source node"
:
4
,
"start line"
:
30
,
"target node"
:
5
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static int debug;"
,
"source node"
:
5
,
"start line"
:
75
,
"target node"
:
6
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static int pci_read_cmd = 12;"
,
"source node"
:
6
,
"start line"
:
85
,
"target node"
:
7
,
"thread"
:
0
},
{
"assumption"
:
"pci_write_cmd == 15;"
,
"file"
:
5
,
"source"
:
"static int pci_write_cmd = 15;"
,
"source node"
:
7
,
"start line"
:
89
,
"target node"
:
8
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static int pci_cmds;"
,
"source node"
:
8
,
"start line"
:
93
,
"target node"
:
9
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static int major_nr;"
,
"source node"
:
9
,
"start line"
:
95
,
"target node"
:
10
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static struct cardinfo cards[4U];"
,
"source node"
:
10
,
"start line"
:
141
,
"target node"
:
11
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static struct timer_list battery_timer;"
,
"source node"
:
11
,
"start line"
:
142
,
"target node"
:
12
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static int num_cards;"
,
"source node"
:
12
,
"start line"
:
144
,
"target node"
:
13
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static struct gendisk *mm_gendisk[4U];"
,
"source node"
:
13
,
"start line"
:
146
,
"target node"
:
14
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static struct block_device_operations const mm_fops = #line 783 {0, 0, 0, 0, 0, 0, 0, 0, &mm_revalidate, &mm_getgeo, 0, &__this_module};"
,
"source node"
:
14
,
"start line"
:
783
,
"target node"
:
15
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static struct pci_device_id const mm_pci_ids[5U] = { {4914U, 21525U, 4294967295U, 4294967295U, 0U, 0U, 0UL}, {4914U, 21541U, 4294967295U, 4294967295U, 0U, 0U, 0UL}, {4914U, 24917U, 4294967295U, 4294967295U, 0U, 0U, 0UL}, {32902U, 46421U, 4914U, 21600U, 327680U, 0U, 0UL}};"
,
"source node"
:
15
,
"start line"
:
1045
,
"target node"
:
16
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"struct pci_device_id const __mod_pci_device_table;"
,
"source node"
:
16
,
"start line"
:
1059
,
"target node"
:
17
,
"thread"
:
0
},
{
"file"
:
5
,
"source"
:
"static struct pci_driver mm_pci_driver = #line 1061 {{0, 0},
\"
umem
\"
, (struct pci_device_id const *)(&mm_pci_ids), &mm_pci_probe, &mm_pci_remove, 0, 0, 0, 0, 0, 0, 0, {0, 0, 0, 0, (_Bool)0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}, {{{{{{0U}}, 0U, 0U, 0, {0, {0, 0}, 0, 0, 0UL}}}}, {0, 0}}};"
,
"source node"
:
17
,
"start line"
:
1061
,
"target node"
:
18
,
"thread"
:
0
},
{
"file"
:
0
,
"source"
:
"struct ldv_thread ldv_thread_1;"
,
"source node"
:
18
,
"start line"
:
122
,
"target node"
:
19
,
"thread"
:
0
},
{
"file"
:
0
,
"source"
:
"struct ldv_thread ldv_thread_14;"
,
"source node"
:
19
,
"start line"
:
123
,
"target node"
:
20
,
"thread"
:
0
},
{
"file"
:
0
,
"source"
:
"struct ldv_thread ldv_thread_2;"
,
"source node"
:
20
,
"start line"
:
124
,
"target node"
:
21
,
"thread"
:
0
},
{
"file"
:
0
,
"source"
:
"struct ldv_thread ldv_thread_3;"
,
"source node"
:
21
,
"start line"
:
125
,
"target node"
:
22
,
"thread"
:
0
},
{
"file"
:
0
,
"source"
:
"struct ldv_thread ldv_thread_4;"
,
"source node"
:
22
,
"start line"
:
126
,
"target node"
:
23
,
"thread"
:
0
},
{
"file"
:
0
,
"source"
:
"struct ldv_thread ldv_thread_5;"
,
"source node"
:
23
,
"start line"
:
127
,
"target node"
:
24
,
"thread"
:
0
},
{
"file"
:
0
,
"source"
:
"struct ldv_thread ldv_thread_6;"
,
"source node"
:
24
,
"start line"
:
128
,
"target node"
:
25
,
"thread"
:
0
},
{
"assumption"
:
"ldv_queue_state == 0;"
,
"file"
:
6
,
"source"
:
"static int ldv_queue_state = 0;"
,
"source node"
:
25
,
"start line"
:
30
,
"target node"
:
26
,
"thread"
:
0
},
{
"enter"
:
0
,
"file"
:
0
,
"source"
:
"ldv_main_14((void *)0);"
,
"source node"
:
26
,
"start line"
:
1073
,
"target node"
:
27
,
"thread"
:
14
},
{
"action"
:
0
,
"file"
:
0
,
"source"
:
"ldv_initialize();"
,
"source node"
:
27
,
"start line"
:
790
,
"target node"
:
28
,
"thread"
:
14
},
{
"action"
:
1
,
"enter"
:
1
,
"file"
:
0
,
"source"
:
"ldv_dispatch_insmod_register_14_3();"
,
"source node"
:
28
,
"start line"
:
794
,
"target node"
:
29
,
"thread"
:
14
},
{
"file"
:
0
,
"source"
:
"struct ldv_struct_insmod_6 *cf_arg_6;"
,
"source node"
:
29
,
"start line"
:
320
,
"target node"
:
30
,
"thread"
:
14
},
{
"enter"
:
2
,
"file"
:
0
,
"source"
:
"cf_arg_6 = (struct ldv_struct_insmod_6 *)ldv_xmalloc(4UL);"
,
"source node"
:
30
,
"start line"
:
320
,
"target node"
:
31
,
"thread"
:
14
},
{
"file"
:
7
,
"source"
:
"void *res;"
,
"source node"
:
31
,
"start line"
:
68
,
"target node"
:
32
,
"thread"
:
14
},
{
"file"
:
7
,
"source"
:
"res = malloc(size);"
,
"source node"
:
32
,
"start line"
:
68
,
"target node"
:
33
,
"thread"
:
14
},
{
"condition"
:
true
,
"file"
:
7
,
"source"
:
"__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));"
,
"source node"
:
33
,
"start line"
:
69
,
"target node"
:
34
,
"thread"
:
14
},
{
"condition"
:
true
,
"enter"
:
3
,
"file"
:
7
,
"source"
:
"__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);"
,
"source node"
:
34
,
"start line"
:
70
,
"target node"
:
35
,
"thread"
:
14
},
{
"file"
:
8
,
"return"
:
3
,
"source"
:
"return (unsigned long)ptr > 4294967295UL;"
,
"source node"
:
35
,
"start line"
:
22
,
"target node"
:
36
,
"thread"
:
14
},
{
"file"
:
7
,
"return"
:
2
,
"source"
:
"return res;"
,
"source node"
:
36
,
"start line"
:
71
,
"target node"
:
37
,
"thread"
:
14
},
{
"enter"
:
4
,
"file"
:
0
,
"source"
:
"ldv_insmod_6((void *)cf_arg_6);"
,
"source node"
:
37
,
"start line"
:
321
,
"target node"
:
38
,
"thread"
:
6
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"void (*ldv_6_mm_cleanup_default)(void);"
,
"source node"
:
38
,
"start line"
:
602
,
"target node"
:
39
,
"thread"
:
6
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"int (*ldv_6_mm_init_default)(void);"
,
"source node"
:
39
,
"start line"
:
603
,
"target node"
:
40
,
"thread"
:
6
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"int ldv_6_reg_guard_12_default;"
,
"source node"
:
40
,
"start line"
:
604
,
"target node"
:
41
,
"thread"
:
6
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"int ldv_6_ret_default;"
,
"source node"
:
41
,
"start line"
:
605
,
"target node"
:
42
,
"thread"
:
6
},
{
"action"
:
3
,
"enter"
:
5
,
"file"
:
0
,
"source"
:
"ldv_free(arg0);"
,
"source node"
:
42
,
"start line"
:
609
,
"target node"
:
43
,
"thread"
:
6
},
{
"file"
:
7
,
"source"
:
"free(s);"
,
"source node"
:
43
,
"start line"
:
63
,
"target node"
:
44
,
"thread"
:
6
},
{
"file"
:
7
,
"return"
:
5
,
"source"
:
"return;"
,
"source node"
:
44
,
"start line"
:
64
,
"target node"
:
45
,
"thread"
:
6
},
{
"action"
:
4
,
"enter"
:
8
,
"file"
:
5
,
"original file"
:
0
,
"original start line"
:
624
,
"source"
:
"ldv_6_ret_default = mm_init();"
,
"source node"
:
45
,
"start line"
:
1070
,
"target node"
:
46
,
"thread"
:
6
},
{
"file"
:
5
,
"source"
:
"int retval;"
,
"source node"
:
46
,
"start line"
:
1070
,
"target node"
:
47
,
"thread"
:
6
},
{
"file"
:
5
,
"source"
:
"int i;"
,
"source node"
:
47
,
"start line"
:
1071
,
"target node"
:
48
,
"thread"
:
6
},
{
"file"
:
5
,
"source"
:
"int err;"
,
"source node"
:
48
,
"start line"
:
1072
,
"target node"
:
49
,
"thread"
:
6
},
{
"file"
:
5
,
"source"
:
"struct gendisk *disk;"
,
"source node"
:
49
,
"start line"
:
1073
,
"target node"
:
50
,
"thread"
:
6
},
{
"file"
:
5
,
"source"
:
"struct lock_class_key __key;"
,
"source node"
:
50
,
"start line"
:
1074
,
"target node"
:
51
,
"thread"
:
6
},
{
"enter"
:
10
,
"file"
:
5
,
"source"
:
"retval = ldv_emg___pci_register_driver(&mm_pci_driver, &__this_module,
\"
umem
\"
);"
,
"source node"
:
51
,
"start line"
:
1073
,
"target node"
:
52
,
"thread"
:
6
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"struct pci_driver *ldv_13_pci_driver_pci_driver;"
,
"source node"
:
52
,
"start line"
:
383
,
"target node"
:
53
,
"thread"
:
6
},
{
"action"
:
5
,
"file"
:
0
,
"source"
:
"ldv_13_pci_driver_pci_driver = arg0;"
,
"source node"
:
53
,
"start line"
:
389
,
"target node"
:
54
,
"thread"
:
6
},
{
"action"
:
6
,
"enter"
:
11
,
"file"
:
0
,
"source"
:
"ldv_dispatch_register_13_3(ldv_13_pci_driver_pci_driver);"
,
"source node"
:
54
,
"start line"
:
393
,
"target node"
:
55
,
"thread"
:
6
},
{
"file"
:
0
,
"source"
:
"struct ldv_struct_pci_scenario_3 *cf_arg_3;"
,
"source node"
:
55
,
"start line"
:
363
,
"target node"
:
56
,
"thread"
:
6
},
{
"enter"
:
2
,
"file"
:
0
,
"source"
:
"cf_arg_3 = (struct ldv_struct_pci_scenario_3 *)ldv_xmalloc(16UL);"
,
"source node"
:
56
,
"start line"
:
363
,
"target node"
:
57
,
"thread"
:
6
},
{
"file"
:
7
,
"source"
:
"void *res;"
,
"source node"
:
57
,
"start line"
:
68
,
"target node"
:
58
,
"thread"
:
6
},
{
"file"
:
7
,
"source"
:
"res = malloc(size);"
,
"source node"
:
58
,
"start line"
:
68
,
"target node"
:
59
,
"thread"
:
6
},
{
"condition"
:
true
,
"file"
:
7
,
"source"
:
"__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));"
,
"source node"
:
59
,
"start line"
:
69
,
"target node"
:
60
,
"thread"
:
6
},
{
"condition"
:
true
,
"enter"
:
3
,
"file"
:
7
,
"source"
:
"__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);"
,
"source node"
:
60
,
"start line"
:
70
,
"target node"
:
61
,
"thread"
:
6
},
{
"file"
:
8
,
"return"
:
3
,
"source"
:
"return (unsigned long)ptr > 4294967295UL;"
,
"source node"
:
61
,
"start line"
:
22
,
"target node"
:
62
,
"thread"
:
6
},
{
"file"
:
7
,
"return"
:
2
,
"source"
:
"return res;"
,
"source node"
:
62
,
"start line"
:
71
,
"target node"
:
63
,
"thread"
:
6
},
{
"file"
:
0
,
"source"
:
"cf_arg_3->arg0 = arg0;"
,
"source node"
:
63
,
"start line"
:
364
,
"target node"
:
64
,
"thread"
:
6
},
{
"enter"
:
12
,
"file"
:
0
,
"source"
:
"ldv_pci_scenario_3((void *)cf_arg_3);"
,
"source node"
:
64
,
"start line"
:
365
,
"target node"
:
65
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"struct pci_driver *ldv_3_container_pci_driver;"
,
"source node"
:
65
,
"start line"
:
816
,
"target node"
:
66
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"struct pci_device_id *ldv_3_ldv_param_17_1_default;"
,
"source node"
:
66
,
"start line"
:
817
,
"target node"
:
67
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"struct pci_dev *ldv_3_resource_dev;"
,
"source node"
:
67
,
"start line"
:
818
,
"target node"
:
68
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"pm_message_t ldv_3_resource_pm_message;"
,
"source node"
:
68
,
"start line"
:
819
,
"target node"
:
69
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"int ldv_3_ret_default;"
,
"source node"
:
69
,
"start line"
:
820
,
"target node"
:
70
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"struct ldv_struct_pci_scenario_3 *data;"
,
"source node"
:
70
,
"start line"
:
821
,
"target node"
:
71
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"data = (struct ldv_struct_pci_scenario_3 *)arg0;"
,
"source node"
:
71
,
"start line"
:
823
,
"target node"
:
72
,
"thread"
:
3
},
{
"action"
:
7
,
"condition"
:
true
,
"file"
:
0
,
"source"
:
"((unsigned long)data) != ((unsigned long)((struct ldv_struct_pci_scenario_3 *)0))"
,
"source node"
:
72
,
"start line"
:
830
,
"target node"
:
73
,
"thread"
:
3
},
{
"action"
:
7
,
"file"
:
0
,
"source"
:
"ldv_3_container_pci_driver = data->arg0;"
,
"source node"
:
73
,
"start line"
:
831
,
"target node"
:
74
,
"thread"
:
3
},
{
"action"
:
7
,
"enter"
:
5
,
"file"
:
0
,
"source"
:
"ldv_free((void *)data);"
,
"source node"
:
74
,
"start line"
:
832
,
"target node"
:
75
,
"thread"
:
3
},
{
"file"
:
7
,
"source"
:
"free(s);"
,
"source node"
:
75
,
"start line"
:
63
,
"target node"
:
76
,
"thread"
:
3
},
{
"file"
:
7
,
"return"
:
5
,
"source"
:
"return;"
,
"source node"
:
76
,
"start line"
:
64
,
"target node"
:
77
,
"thread"
:
3
},
{
"action"
:
8
,
"enter"
:
2
,
"file"
:
0
,
"source"
:
"ldv_3_resource_dev = (struct pci_dev *)ldv_xmalloc(2936UL);"
,
"source node"
:
77
,
"start line"
:
837
,
"target node"
:
78
,
"thread"
:
3
},
{
"file"
:
7
,
"source"
:
"void *res;"
,
"source node"
:
78
,
"start line"
:
68
,
"target node"
:
79
,
"thread"
:
3
},
{
"file"
:
7
,
"source"
:
"res = malloc(size);"
,
"source node"
:
79
,
"start line"
:
68
,
"target node"
:
80
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
7
,
"source"
:
"__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));"
,
"source node"
:
80
,
"start line"
:
69
,
"target node"
:
81
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
3
,
"file"
:
7
,
"source"
:
"__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);"
,
"source node"
:
81
,
"start line"
:
70
,
"target node"
:
82
,
"thread"
:
3
},
{
"file"
:
8
,
"return"
:
3
,
"source"
:
"return (unsigned long)ptr > 4294967295UL;"
,
"source node"
:
82
,
"start line"
:
22
,
"target node"
:
83
,
"thread"
:
3
},
{
"file"
:
7
,
"return"
:
2
,
"source"
:
"return res;"
,
"source node"
:
83
,
"start line"
:
71
,
"target node"
:
84
,
"thread"
:
3
},
{
"action"
:
9
,
"enter"
:
13
,
"file"
:
0
,
"source"
:
"ldv_3_ldv_param_17_1_default = (struct pci_device_id *)ldv_xmalloc_unknown_size(0UL);"
,
"source node"
:
84
,
"start line"
:
854
,
"target node"
:
85
,
"thread"
:
3
},
{
"file"
:
7
,
"source"
:
"void *res;"
,
"source node"
:
85
,
"start line"
:
116
,
"target node"
:
86
,
"thread"
:
3
},
{
"file"
:
7
,
"source"
:
"res = external_allocated_data();"
,
"source node"
:
86
,
"start line"
:
116
,
"target node"
:
87
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
7
,
"source"
:
"__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));"
,
"source node"
:
87
,
"start line"
:
117
,
"target node"
:
88
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
3
,
"file"
:
7
,
"source"
:
"__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);"
,
"source node"
:
88
,
"start line"
:
118
,
"target node"
:
89
,
"thread"
:
3
},
{
"file"
:
8
,
"return"
:
3
,
"source"
:
"return (unsigned long)ptr > 4294967295UL;"
,
"source node"
:
89
,
"start line"
:
22
,
"target node"
:
90
,
"thread"
:
3
},
{
"file"
:
7
,
"return"
:
13
,
"source"
:
"return res;"
,
"source node"
:
90
,
"start line"
:
119
,
"target node"
:
91
,
"thread"
:
3
},
{
"action"
:
10
,
"file"
:
0
,
"source"
:
"ldv_pre_probe();"
,
"source node"
:
91
,
"start line"
:
859
,
"target node"
:
92
,
"thread"
:
3
},
{
"action"
:
10
,
"enter"
:
15
,
"file"
:
5
,
"original file"
:
0
,
"original start line"
:
861
,
"source"
:
"ldv_3_ret_default = mm_pci_probe(ldv_3_resource_dev, ldv_3_ldv_param_17_1_default);"
,
"source node"
:
92
,
"start line"
:
791
,
"target node"
:
93
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"int ret;"
,
"source node"
:
93
,
"start line"
:
791
,
"target node"
:
94
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"struct cardinfo *card;"
,
"source node"
:
94
,
"start line"
:
792
,
"target node"
:
95
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned char mem_present;"
,
"source node"
:
95
,
"start line"
:
793
,
"target node"
:
96
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned char batt_status;"
,
"source node"
:
96
,
"start line"
:
794
,
"target node"
:
97
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned int saved_bar;"
,
"source node"
:
97
,
"start line"
:
795
,
"target node"
:
98
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned int data;"
,
"source node"
:
98
,
"start line"
:
796
,
"target node"
:
99
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned long csr_base;"
,
"source node"
:
99
,
"start line"
:
797
,
"target node"
:
100
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned long csr_len;"
,
"source node"
:
100
,
"start line"
:
798
,
"target node"
:
101
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"int magic_number;"
,
"source node"
:
101
,
"start line"
:
799
,
"target node"
:
102
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"int printed_version;"
,
"source node"
:
102
,
"start line"
:
800
,
"target node"
:
103
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"struct lock_class_key __key;"
,
"source node"
:
103
,
"start line"
:
810
,
"target node"
:
104
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned short cfg_command;"
,
"source node"
:
104
,
"start line"
:
811
,
"target node"
:
105
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"ret = -19;"
,
"source node"
:
105
,
"start line"
:
791
,
"target node"
:
106
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card = (struct cardinfo *)(&cards) + (unsigned long)num_cards;"
,
"source node"
:
106
,
"start line"
:
792
,
"target node"
:
107
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"tmp = printed_version;"
,
"source node"
:
107
,
"start line"
:
801
,
"target node"
:
108
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"printed_version = printed_version + 1;"
,
"source node"
:
108
,
"start line"
:
801
,
"target node"
:
109
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"tmp == 0"
,
"source node"
:
109
,
"start line"
:
801
,
"target node"
:
110
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"printk(
\"\\
016v2.3 : Micro Memory(tm) PCI memory board block driver
\\
n
\"
);"
,
"source node"
:
110
,
"start line"
:
802
,
"target node"
:
111
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"ret = pci_enable_device(dev);"
,
"source node"
:
111
,
"start line"
:
804
,
"target node"
:
112
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"ret == 0"
,
"source node"
:
112
,
"start line"
:
805
,
"target node"
:
113
,
"thread"
:
3
},
{
"enter"
:
16
,
"file"
:
5
,
"source"
:
"pci_write_config_byte((struct pci_dev const *)dev, 13, 248);"
,
"source node"
:
113
,
"start line"
:
808
,
"target node"
:
114
,
"thread"
:
3
},
{
"file"
:
10
,
"return"
:
16
,
"source"
:
"return pci_bus_write_config_byte(dev->bus, dev->devfn, where, (int)val);"
,
"source node"
:
114
,
"start line"
:
849
,
"target node"
:
115
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"pci_set_master(dev);"
,
"source node"
:
115
,
"start line"
:
809
,
"target node"
:
116
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->dev = dev;"
,
"source node"
:
116
,
"start line"
:
811
,
"target node"
:
117
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"csr_base = (unsigned long)dev->resource[0].start;"
,
"source node"
:
117
,
"start line"
:
813
,
"target node"
:
118
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((dev->resource)[0]).start) == 0ULL"
,
"source node"
:
118
,
"start line"
:
814
,
"target node"
:
119
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((dev->resource)[0]).end) != (((dev->resource)[0]).start)"
,
"source node"
:
119
,
"start line"
:
814
,
"target node"
:
120
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"(unsigned long)((dev->resource[0].end - dev->resource[0].start) + 1ULL)"
,
"source node"
:
120
,
"start line"
:
814
,
"target node"
:
121
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"csr_len = dev->resource[0].start != 0ULL || dev->resource[0].end != dev->resource[0].start ? (unsigned long)((dev->resource[0].end - dev->resource[0].start) + 1ULL) : 0UL;"
,
"source node"
:
121
,
"start line"
:
814
,
"target node"
:
122
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"csr_base != 0UL"
,
"source node"
:
122
,
"start line"
:
815
,
"target node"
:
123
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"csr_len != 0UL"
,
"source node"
:
123
,
"start line"
:
815
,
"target node"
:
124
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"dev_printk(
\"\\
016
\"
, (struct device const *)(&dev->dev),
\"
Micro Memory(tm) controller found (PCI Mem Module (Battery Backup))
\\
n
\"
);"
,
"source node"
:
124
,
"start line"
:
818
,
"target node"
:
125
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
17
,
"file"
:
5
,
"source"
:
"pci_set_dma_mask(dev, 0xffffffffffffffffULL) == 0"
,
"source node"
:
125
,
"start line"
:
821
,
"target node"
:
126
,
"thread"
:
3
},
{
"file"
:
11
,
"return"
:
17
,
"source"
:
"return dma_set_mask(&dev->dev, mask);"
,
"source node"
:
126
,
"start line"
:
107
,
"target node"
:
127
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"ret = pci_request_regions(dev,
\"
umem
\"
);"
,
"source node"
:
127
,
"start line"
:
827
,
"target node"
:
128
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"ret == 0"
,
"source node"
:
128
,
"start line"
:
828
,
"target node"
:
129
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->csr_remap = (unsigned char *)ioremap_nocache((resource_size_t)csr_base, csr_len);"
,
"source node"
:
129
,
"start line"
:
834
,
"target node"
:
130
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"__CPAchecker_TMP_1 != ((unsigned long)((unsigned char *)0U))"
,
"source node"
:
130
,
"start line"
:
835
,
"target node"
:
131
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"dev_printk(
\"\\
016
\"
, (struct device const *)(&(card->dev)->dev),
\"
CSR 0x%08lx -> 0x%p (0x%lx)
\\
n
\"
, csr_base, card->csr_remap, csr_len);"
,
"source node"
:
131
,
"start line"
:
843
,
"target node"
:
132
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"__CPAchecker_TMP_2 == 21525"
,
"source node"
:
132
,
"start line"
:
848
,
"target node"
:
133
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->flags = card->flags | 6;"
,
"source node"
:
133
,
"start line"
:
849
,
"target node"
:
134
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"magic_number = 89;"
,
"source node"
:
134
,
"start line"
:
850
,
"target node"
:
135
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
18
,
"file"
:
5
,
"source"
:
"((int)readb((void const volatile *)card->csr_remap)) == magic_number"
,
"source node"
:
135
,
"start line"
:
869
,
"target node"
:
136
,
"thread"
:
3
},
{
"file"
:
12
,
"source"
:
"unsigned char ret;"
,
"source node"
:
136
,
"start line"
:
55
,
"target node"
:
137
,
"thread"
:
3
},
{
"file"
:
12
,
"return"
:
18
,
"source"
:
"return ret;"
,
"source node"
:
137
,
"start line"
:
53
,
"target node"
:
138
,
"thread"
:
3
},
{
"enter"
:
19
,
"file"
:
5
,
"source"
:
"card->mm_pages[0].desc = (struct mm_dma_desc *)pci_alloc_consistent(card->dev, 8192UL, &card->mm_pages[0].page_dma);"
,
"source node"
:
138
,
"start line"
:
875
,
"target node"
:
139
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
11
,
"source"
:
"((unsigned long)hwdev) != ((unsigned long)((struct pci_dev *)0))"
,
"source node"
:
139
,
"start line"
:
19
,
"target node"
:
140
,
"thread"
:
3
},
{
"file"
:
11
,
"source"
:
"&hwdev->dev"
,
"source node"
:
140
,
"start line"
:
19
,
"target node"
:
141
,
"thread"
:
3
},
{
"enter"
:
20
,
"file"
:
11
,
"return"
:
19
,
"source"
:
"return dma_alloc_attrs((unsigned long)hwdev != (unsigned long)((struct pci_dev *)0) ? &hwdev->dev : (struct device *)0, size, dma_handle, 32U, (struct dma_attrs *)0);"
,
"source node"
:
141
,
"start line"
:
19
,
"target node"
:
142
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
20
,
"file"
:
4
,
"source"
:
"struct dma_map_ops *ops;"
,
"source node"
:
142
,
"start line"
:
134
,
"target node"
:
143
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"void *memory;"
,
"source node"
:
143
,
"start line"
:
136
,
"target node"
:
144
,
"thread"
:
3
},
{
"enter"
:
21
,
"file"
:
4
,
"source"
:
"ops = get_dma_ops(dev);"
,
"source node"
:
144
,
"start line"
:
134
,
"target node"
:
145
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
22
,
"file"
:
4
,
"source"
:
"__builtin_expect((unsigned long)dev == (unsigned long)((struct device *)0), 0L) == 0L"
,
"source node"
:
145
,
"start line"
:
37
,
"target node"
:
146
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
146
,
"start line"
:
26
,
"target node"
:
147
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long)(dev->archdata.dma_ops)) != ((unsigned long)((struct dma_map_ops *)0))"
,
"source node"
:
147
,
"start line"
:
37
,
"target node"
:
148
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
21
,
"source"
:
"return dev->archdata.dma_ops;"
,
"source node"
:
148
,
"start line"
:
40
,
"target node"
:
149
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
20
,
"file"
:
4
,
"source"
:
"gfp = gfp &4294967288U;"
,
"source node"
:
149
,
"start line"
:
137
,
"target node"
:
150
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long)dev) == ((unsigned long)((struct device *)0))"
,
"source node"
:
150
,
"start line"
:
142
,
"target node"
:
151
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"dev = &x86_dma_fallback_dev;"
,
"source node"
:
151
,
"start line"
:
143
,
"target node"
:
152
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
23
,
"file"
:
4
,
"source"
:
"is_device_dma_capable(dev) != 0"
,
"source node"
:
152
,
"start line"
:
145
,
"target node"
:
153
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
14
,
"source"
:
"__CPAchecker_TMP_1 != ((unsigned long)((u64 *)0ULL))"
,
"source node"
:
153
,
"start line"
:
72
,
"target node"
:
154
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
14
,
"source"
:
"(*(dev->dma_mask)) != 0ULL"
,
"source node"
:
154
,
"start line"
:
72
,
"target node"
:
155
,
"thread"
:
3
},
{
"file"
:
14
,
"source"
:
"(unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL"
,
"source node"
:
155
,
"start line"
:
72
,
"target node"
:
156
,
"thread"
:
3
},
{
"file"
:
14
,
"return"
:
23
,
"source"
:
"return (unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL;"
,
"source node"
:
156
,
"start line"
:
72
,
"target node"
:
157
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"__CPAchecker_TMP_0 != ((unsigned long)((void *(*)(struct device *, size_t, dma_addr_t *, gfp_t, struct dma_attrs *))0))"
,
"source node"
:
157
,
"start line"
:
148
,
"target node"
:
158
,
"thread"
:
3
},
{
"enter"
:
24
,
"file"
:
4
,
"source"
:
"memory = (*(ops->alloc))(dev, size, dma_handle, dma_alloc_coherent_gfp_flags(dev, gfp), attrs);"
,
"source node"
:
158
,
"start line"
:
151
,
"target node"
:
159
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
24
,
"file"
:
4
,
"source"
:
"unsigned long dma_mask;"
,
"source node"
:
159
,
"start line"
:
117
,
"target node"
:
160
,
"thread"
:
3
},
{
"enter"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = dma_alloc_coherent_mask(dev, gfp);"
,
"source node"
:
160
,
"start line"
:
117
,
"target node"
:
161
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"unsigned long dma_mask;"
,
"source node"
:
161
,
"start line"
:
105
,
"target node"
:
162
,
"thread"
:
3
},
{
"assumption"
:
"dma_mask == 0UL;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = 0UL;"
,
"source node"
:
162
,
"start line"
:
106
,
"target node"
:
163
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"dma_mask = (unsigned long)dev->coherent_dma_mask;"
,
"source node"
:
163
,
"start line"
:
108
,
"target node"
:
164
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"dma_mask == 0UL"
,
"source node"
:
164
,
"start line"
:
109
,
"target node"
:
165
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"(((int)gfp) &1) == 0"
,
"source node"
:
165
,
"start line"
:
110
,
"target node"
:
166
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"4294967295UL"
,
"source node"
:
166
,
"start line"
:
110
,
"target node"
:
167
,
"thread"
:
3
},
{
"assumption"
:
"dma_mask == 4294967295UL;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = (int)gfp &1 ? 16777215UL : 4294967295UL;"
,
"source node"
:
167
,
"start line"
:
110
,
"target node"
:
168
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
25
,
"source"
:
"return dma_mask;"
,
"source node"
:
168
,
"start line"
:
112
,
"target node"
:
169
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long long)dma_mask) > 16777215ULL"
,
"source node"
:
169
,
"start line"
:
119
,
"target node"
:
170
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long long)dma_mask) > 4294967295ULL"
,
"source node"
:
170
,
"start line"
:
122
,
"target node"
:
171
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
24
,
"source"
:
"return gfp;"
,
"source node"
:
171
,
"start line"
:
125
,
"target node"
:
172
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"debug_dma_alloc_coherent(dev, size, *dma_handle, memory);"
,
"source node"
:
172
,
"start line"
:
153
,
"target node"
:
173
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
20
,
"source"
:
"return memory;"
,
"source node"
:
173
,
"start line"
:
155
,
"target node"
:
174
,
"thread"
:
3
},
{
"enter"
:
19
,
"file"
:
5
,
"source"
:
"card->mm_pages[1].desc = (struct mm_dma_desc *)pci_alloc_consistent(card->dev, 8192UL, &card->mm_pages[1].page_dma);"
,
"source node"
:
174
,
"start line"
:
878
,
"target node"
:
175
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
11
,
"source"
:
"((unsigned long)hwdev) != ((unsigned long)((struct pci_dev *)0))"
,
"source node"
:
175
,
"start line"
:
19
,
"target node"
:
176
,
"thread"
:
3
},
{
"file"
:
11
,
"source"
:
"&hwdev->dev"
,
"source node"
:
176
,
"start line"
:
19
,
"target node"
:
177
,
"thread"
:
3
},
{
"enter"
:
20
,
"file"
:
11
,
"return"
:
19
,
"source"
:
"return dma_alloc_attrs((unsigned long)hwdev != (unsigned long)((struct pci_dev *)0) ? &hwdev->dev : (struct device *)0, size, dma_handle, 32U, (struct dma_attrs *)0);"
,
"source node"
:
177
,
"start line"
:
19
,
"target node"
:
178
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
20
,
"file"
:
4
,
"source"
:
"struct dma_map_ops *ops;"
,
"source node"
:
178
,
"start line"
:
134
,
"target node"
:
179
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"void *memory;"
,
"source node"
:
179
,
"start line"
:
136
,
"target node"
:
180
,
"thread"
:
3
},
{
"enter"
:
21
,
"file"
:
4
,
"source"
:
"ops = get_dma_ops(dev);"
,
"source node"
:
180
,
"start line"
:
134
,
"target node"
:
181
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
22
,
"file"
:
4
,
"source"
:
"__builtin_expect((unsigned long)dev == (unsigned long)((struct device *)0), 0L) == 0L"
,
"source node"
:
181
,
"start line"
:
37
,
"target node"
:
182
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
182
,
"start line"
:
26
,
"target node"
:
183
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long)(dev->archdata.dma_ops)) != ((unsigned long)((struct dma_map_ops *)0))"
,
"source node"
:
183
,
"start line"
:
37
,
"target node"
:
184
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
21
,
"source"
:
"return dev->archdata.dma_ops;"
,
"source node"
:
184
,
"start line"
:
40
,
"target node"
:
185
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
20
,
"file"
:
4
,
"source"
:
"gfp = gfp &4294967288U;"
,
"source node"
:
185
,
"start line"
:
137
,
"target node"
:
186
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long)dev) == ((unsigned long)((struct device *)0))"
,
"source node"
:
186
,
"start line"
:
142
,
"target node"
:
187
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"dev = &x86_dma_fallback_dev;"
,
"source node"
:
187
,
"start line"
:
143
,
"target node"
:
188
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
23
,
"file"
:
4
,
"source"
:
"is_device_dma_capable(dev) != 0"
,
"source node"
:
188
,
"start line"
:
145
,
"target node"
:
189
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
14
,
"source"
:
"__CPAchecker_TMP_1 != ((unsigned long)((u64 *)0ULL))"
,
"source node"
:
189
,
"start line"
:
72
,
"target node"
:
190
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
14
,
"source"
:
"(*(dev->dma_mask)) != 0ULL"
,
"source node"
:
190
,
"start line"
:
72
,
"target node"
:
191
,
"thread"
:
3
},
{
"file"
:
14
,
"source"
:
"(unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL"
,
"source node"
:
191
,
"start line"
:
72
,
"target node"
:
192
,
"thread"
:
3
},
{
"file"
:
14
,
"return"
:
23
,
"source"
:
"return (unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL;"
,
"source node"
:
192
,
"start line"
:
72
,
"target node"
:
193
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"__CPAchecker_TMP_0 != ((unsigned long)((void *(*)(struct device *, size_t, dma_addr_t *, gfp_t, struct dma_attrs *))0))"
,
"source node"
:
193
,
"start line"
:
148
,
"target node"
:
194
,
"thread"
:
3
},
{
"enter"
:
24
,
"file"
:
4
,
"source"
:
"memory = (*(ops->alloc))(dev, size, dma_handle, dma_alloc_coherent_gfp_flags(dev, gfp), attrs);"
,
"source node"
:
194
,
"start line"
:
151
,
"target node"
:
195
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
24
,
"file"
:
4
,
"source"
:
"unsigned long dma_mask;"
,
"source node"
:
195
,
"start line"
:
117
,
"target node"
:
196
,
"thread"
:
3
},
{
"enter"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = dma_alloc_coherent_mask(dev, gfp);"
,
"source node"
:
196
,
"start line"
:
117
,
"target node"
:
197
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"unsigned long dma_mask;"
,
"source node"
:
197
,
"start line"
:
105
,
"target node"
:
198
,
"thread"
:
3
},
{
"assumption"
:
"dma_mask == 0UL;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = 0UL;"
,
"source node"
:
198
,
"start line"
:
106
,
"target node"
:
199
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"dma_mask = (unsigned long)dev->coherent_dma_mask;"
,
"source node"
:
199
,
"start line"
:
108
,
"target node"
:
200
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"dma_mask == 0UL"
,
"source node"
:
200
,
"start line"
:
109
,
"target node"
:
201
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"(((int)gfp) &1) == 0"
,
"source node"
:
201
,
"start line"
:
110
,
"target node"
:
202
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"4294967295UL"
,
"source node"
:
202
,
"start line"
:
110
,
"target node"
:
203
,
"thread"
:
3
},
{
"assumption"
:
"dma_mask == 4294967295UL;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = (int)gfp &1 ? 16777215UL : 4294967295UL;"
,
"source node"
:
203
,
"start line"
:
110
,
"target node"
:
204
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
25
,
"source"
:
"return dma_mask;"
,
"source node"
:
204
,
"start line"
:
112
,
"target node"
:
205
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long long)dma_mask) > 16777215ULL"
,
"source node"
:
205
,
"start line"
:
119
,
"target node"
:
206
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long long)dma_mask) > 4294967295ULL"
,
"source node"
:
206
,
"start line"
:
122
,
"target node"
:
207
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
24
,
"source"
:
"return gfp;"
,
"source node"
:
207
,
"start line"
:
125
,
"target node"
:
208
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"debug_dma_alloc_coherent(dev, size, *dma_handle, memory);"
,
"source node"
:
208
,
"start line"
:
153
,
"target node"
:
209
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
20
,
"source"
:
"return memory;"
,
"source node"
:
209
,
"start line"
:
155
,
"target node"
:
210
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((unsigned long)(((card->mm_pages)[0]).desc)) != ((unsigned long)((struct mm_dma_desc *)0))"
,
"source node"
:
210
,
"start line"
:
881
,
"target node"
:
211
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((unsigned long)(((card->mm_pages)[1]).desc)) != ((unsigned long)((struct mm_dma_desc *)0))"
,
"source node"
:
211
,
"start line"
:
881
,
"target node"
:
212
,
"thread"
:
3
},
{
"enter"
:
26
,
"file"
:
5
,
"source"
:
"reset_page((struct mm_page *)(&card->mm_pages));"
,
"source node"
:
212
,
"start line"
:
886
,
"target node"
:
213
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->cnt = 0;"
,
"source node"
:
213
,
"start line"
:
328
,
"target node"
:
214
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->headcnt = 0;"
,
"source node"
:
214
,
"start line"
:
329
,
"target node"
:
215
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->bio = (struct bio *)0;"
,
"source node"
:
215
,
"start line"
:
330
,
"target node"
:
216
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->biotail = &page->bio;"
,
"source node"
:
216
,
"start line"
:
331
,
"target node"
:
217
,
"thread"
:
3
},
{
"file"
:
5
,
"return"
:
26
,
"source"
:
"return;"
,
"source node"
:
217
,
"start line"
:
332
,
"target node"
:
218
,
"thread"
:
3
},
{
"enter"
:
26
,
"file"
:
5
,
"source"
:
"reset_page((struct mm_page *)(&card->mm_pages) + 1UL);"
,
"source node"
:
218
,
"start line"
:
887
,
"target node"
:
219
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->cnt = 0;"
,
"source node"
:
219
,
"start line"
:
328
,
"target node"
:
220
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->headcnt = 0;"
,
"source node"
:
220
,
"start line"
:
329
,
"target node"
:
221
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->bio = (struct bio *)0;"
,
"source node"
:
221
,
"start line"
:
330
,
"target node"
:
222
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->biotail = &page->bio;"
,
"source node"
:
222
,
"start line"
:
331
,
"target node"
:
223
,
"thread"
:
3
},
{
"file"
:
5
,
"return"
:
26
,
"source"
:
"return;"
,
"source node"
:
223
,
"start line"
:
332
,
"target node"
:
224
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->Ready = 0;"
,
"source node"
:
224
,
"start line"
:
888
,
"target node"
:
225
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->Active = -1;"
,
"source node"
:
225
,
"start line"
:
889
,
"target node"
:
226
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->bio = (struct bio *)0;"
,
"source node"
:
226
,
"start line"
:
890
,
"target node"
:
227
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->biotail = &card->bio;"
,
"source node"
:
227
,
"start line"
:
891
,
"target node"
:
228
,
"thread"
:
3
},
{
"enter"
:
27
,
"file"
:
5
,
"source"
:
"card->queue = ldv_blk_alloc_queue_10(208U);"
,
"source node"
:
228
,
"start line"
:
893
,
"target node"
:
229
,
"thread"
:
3
},
{
"file"
:
0
,
"source"
:
"ldv_func_ret_type ldv_func_res;"
,
"source node"
:
229
,
"start line"
:
1146
,
"target node"
:
230
,
"thread"
:
3
},
{
"file"
:
0
,
"source"
:
"ldv_func_res = blk_alloc_queue(ldv_func_arg1);"
,
"source node"
:
230
,
"start line"
:
1148
,
"target node"
:
231
,
"thread"
:
3
},
{
"enter"
:
28
,
"file"
:
0
,
"note"
:
"Allocate queue."
,
"return"
:
27
,
"source"
:
"return ldv_request_queue();"
,
"source node"
:
231
,
"start line"
:
1150
,
"target node"
:
232
,
"thread"
:
3
},
{
"file"
:
6
,
"source"
:
"struct request_queue *res;"
,
"source node"
:
232
,
"start line"
:
35
,
"target node"
:
233
,
"thread"
:
3
},
{
"enter"
:
29
,
"file"
:
6
,
"note"
:
"Choose an arbitrary return value."
,
"source"
:
"res = (struct request_queue *)ldv_undef_ptr();"
,
"source node"
:
233
,
"start line"
:
38
,
"target node"
:
234
,
"thread"
:
3
},
{
"file"
:
9
,
"return"
:
29
,
"source"
:
"return __VERIFIER_nondet_pointer();"
,
"source node"
:
234
,
"start line"
:
45
,
"target node"
:
235
,
"thread"
:
3
},
{
"enter"
:
30
,
"file"
:
6
,
"note"
:
"Queue should not be allocated twice."
,
"source"
:
"ldv_assert_linux_block_queue__double_allocation(ldv_queue_state == 0);"
,
"source node"
:
235
,
"start line"
:
36
,
"target node"
:
236
,
"thread"
:
3
},
{
"assumption"
:
"expr == 1;"
,
"assumption scope"
:
30
,
"condition"
:
true
,
"file"
:
15
,
"source"
:
"expr != 0"
,
"source node"
:
236
,
"start line"
:
4
,
"target node"
:
237
,
"thread"
:
3
},
{
"file"
:
15
,
"return"
:
30
,
"source"
:
"return;"
,
"source node"
:
237
,
"start line"
:
6
,
"target node"
:
238
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
6
,
"note"
:
"If memory is not available."
,
"source"
:
"((unsigned long)res) != ((unsigned long)((struct request_queue *)0))"
,
"source node"
:
238
,
"start line"
:
40
,
"target node"
:
239
,
"thread"
:
3
},
{
"assumption"
:
"ldv_queue_state == 1;"
,
"assumption scope"
:
28
,
"file"
:
6
,
"note"
:
"Allocate gendisk."
,
"source"
:
"ldv_queue_state = 1;"
,
"source node"
:
239
,
"start line"
:
42
,
"target node"
:
240
,
"thread"
:
3
},
{
"file"
:
6
,
"note"
:
"Queue was successfully created."
,
"return"
:
28
,
"source"
:
"return res;"
,
"source node"
:
240
,
"start line"
:
44
,
"target node"
:
241
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"__CPAchecker_TMP_6 != ((unsigned long)((struct request_queue *)0))"
,
"source node"
:
241
,
"start line"
:
894
,
"target node"
:
242
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"blk_queue_make_request(card->queue, &mm_make_request);"
,
"source node"
:
242
,
"start line"
:
897
,
"target node"
:
243
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"(card->queue)->queue_lock = &card->lock;"
,
"source node"
:
243
,
"start line"
:
898
,
"target node"
:
244
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"(card->queue)->queuedata = (void *)card;"
,
"source node"
:
244
,
"start line"
:
899
,
"target node"
:
245
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"tasklet_init(&card->tasklet, &process_page, (unsigned long)card);"
,
"source node"
:
245
,
"start line"
:
901
,
"target node"
:
246
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->check_batteries = 0;"
,
"source node"
:
246
,
"start line"
:
903
,
"target node"
:
247
,
"thread"
:
3
},
{
"enter"
:
18
,
"file"
:
5
,
"source"
:
"mem_present = readb((void const volatile *)(card->csr_remap + 7UL));"
,
"source node"
:
247
,
"start line"
:
905
,
"target node"
:
248
,
"thread"
:
3
},
{
"file"
:
12
,
"source"
:
"unsigned char ret;"
,
"source node"
:
248
,
"start line"
:
55
,
"target node"
:
249
,
"thread"
:
3
},
{
"file"
:
12
,
"return"
:
18
,
"source"
:
"return ret;"
,
"source node"
:
249
,
"start line"
:
53
,
"target node"
:
250
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((int)mem_present) == 254"
,
"source node"
:
250
,
"start line"
:
907
,
"target node"
:
251
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->mm_size = 131072U;"
,
"source node"
:
251
,
"start line"
:
908
,
"target node"
:
252
,
"thread"
:
3
},
{
"enter"
:
31
,
"file"
:
5
,
"source"
:
"set_led(card, 2, 0);"
,
"source node"
:
252
,
"start line"
:
928
,
"target node"
:
253
,
"thread"
:
3
},
{
"assumption"
:
"state == 0U;"
,
"assumption scope"
:
31
,
"file"
:
5
,
"source"
:
"unsigned char led;"
,
"source node"
:
253
,
"start line"
:
177
,
"target node"
:
254
,
"thread"
:
3
},
{
"enter"
:
18
,
"file"
:
5
,
"source"
:
"led = readb((void const volatile *)(card->csr_remap + 8UL));"
,
"source node"
:
254
,
"start line"
:
179
,
"target node"
:
255
,
"thread"
:
3
},
{
"file"
:
12
,
"source"
:
"unsigned char ret;"
,
"source node"
:
255
,
"start line"
:
55
,
"target node"
:
256
,
"thread"
:
3
},
{
"file"
:
12
,
"return"
:
18
,
"source"
:
"return ret;"
,
"source node"
:
256
,
"start line"
:
53
,
"target node"
:
257
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((unsigned int)state) != 255U"
,
"source node"
:
257
,
"start line"
:
180
,
"target node"
:
258
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"led = (unsigned char)((int)((signed char)led) &~ ((int)((signed char)(3 << shift))));"
,
"source node"
:
258
,
"start line"
:
183
,
"target node"
:
259
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"led = (unsigned char)((int)((signed char)led) | (int)((signed char)((int)state << shift)));"
,
"source node"
:
259
,
"start line"
:
184
,
"target node"
:
260
,
"thread"
:
3
},
{
"enter"
:
32
,
"file"
:
5
,
"source"
:
"writeb((int)led, (void volatile *)(card->csr_remap + 8UL));"
,
"source node"
:
260
,
"start line"
:
186
,
"target node"
:
261
,
"thread"
:
3
},
{
"file"
:
12
,
"return"
:
32
,
"source"
:
"return;"
,
"source node"
:
261
,
"start line"
:
62
,
"target node"
:
262
,
"thread"
:
3
},
{
"file"
:
5
,
"return"
:
31
,
"source"
:
"return;"
,
"source node"
:
262
,
"start line"
:
187
,
"target node"
:
263
,
"thread"
:
3
},
{
"enter"
:
31
,
"file"
:
5
,
"source"
:
"set_led(card, 4, 0);"
,
"source node"
:
263
,
"start line"
:
929
,
"target node"
:
264
,
"thread"
:
3
},
{
"assumption"
:
"state == 0U;"
,
"assumption scope"
:
31
,
"file"
:
5
,
"source"
:
"unsigned char led;"
,
"source node"
:
264
,
"start line"
:
177
,
"target node"
:
265
,
"thread"
:
3
},
{
"enter"
:
18
,
"file"
:
5
,
"source"
:
"led = readb((void const volatile *)(card->csr_remap + 8UL));"
,
"source node"
:
265
,
"start line"
:
179
,
"target node"
:
266
,
"thread"
:
3
},
{
"file"
:
12
,
"source"
:
"unsigned char ret;"
,
"source node"
:
266
,
"start line"
:
55
,
"target node"
:
267
,
"thread"
:
3
},
{
"file"
:
12
,
"return"
:
18
,
"source"
:
"return ret;"
,
"source node"
:
267
,
"start line"
:
53
,
"target node"
:
268
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((unsigned int)state) != 255U"
,
"source node"
:
268
,
"start line"
:
180
,
"target node"
:
269
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"led = (unsigned char)((int)((signed char)led) &~ ((int)((signed char)(3 << shift))));"
,
"source node"
:
269
,
"start line"
:
183
,
"target node"
:
270
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"led = (unsigned char)((int)((signed char)led) | (int)((signed char)((int)state << shift)));"
,
"source node"
:
270
,
"start line"
:
184
,
"target node"
:
271
,
"thread"
:
3
},
{
"enter"
:
32
,
"file"
:
5
,
"source"
:
"writeb((int)led, (void volatile *)(card->csr_remap + 8UL));"
,
"source node"
:
271
,
"start line"
:
186
,
"target node"
:
272
,
"thread"
:
3
},
{
"file"
:
12
,
"return"
:
32
,
"source"
:
"return;"
,
"source node"
:
272
,
"start line"
:
62
,
"target node"
:
273
,
"thread"
:
3
},
{
"file"
:
5
,
"return"
:
31
,
"source"
:
"return;"
,
"source node"
:
273
,
"start line"
:
187
,
"target node"
:
274
,
"thread"
:
3
},
{
"enter"
:
18
,
"file"
:
5
,
"source"
:
"batt_status = readb((void const volatile *)(card->csr_remap + 4UL));"
,
"source node"
:
274
,
"start line"
:
931
,
"target node"
:
275
,
"thread"
:
3
},
{
"file"
:
12
,
"source"
:
"unsigned char ret;"
,
"source node"
:
275
,
"start line"
:
55
,
"target node"
:
276
,
"thread"
:
3
},
{
"file"
:
12
,
"return"
:
18
,
"source"
:
"return ret;"
,
"source node"
:
276
,
"start line"
:
53
,
"target node"
:
277
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->battery[0].good = ((int)batt_status &2) == 0;"
,
"source node"
:
277
,
"start line"
:
933
,
"target node"
:
278
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->battery[1].good = ((int)batt_status &8) == 0;"
,
"source node"
:
278
,
"start line"
:
934
,
"target node"
:
279
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->battery[1].last_change = jiffies;"
,
"source node"
:
279
,
"start line"
:
935
,
"target node"
:
280
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->battery[0].last_change = tmp___6;"
,
"source node"
:
280
,
"start line"
:
935
,
"target node"
:
281
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((card->flags) &8) == 0"
,
"source node"
:
281
,
"start line"
:
937
,
"target node"
:
282
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((int)batt_status) &1) != 0"
,
"source node"
:
282
,
"start line"
:
942
,
"target node"
:
283
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"(char *)
\"
Disabled
\"
"
,
"source node"
:
283
,
"start line"
:
942
,
"target node"
:
284
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((card->battery)[0]).good) == 0"
,
"source node"
:
284
,
"start line"
:
943
,
"target node"
:
285
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"(char *)
\"
FAILURE
\"
"
,
"source node"
:
285
,
"start line"
:
943
,
"target node"
:
286
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((int)batt_status) &4) == 0"
,
"source node"
:
286
,
"start line"
:
943
,
"target node"
:
287
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"(char *)
\"
Enabled
\"
"
,
"source node"
:
287
,
"start line"
:
943
,
"target node"
:
288
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((card->battery)[1]).good) == 0"
,
"source node"
:
288
,
"start line"
:
944
,
"target node"
:
289
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"(char *)
\"
FAILURE
\"
"
,
"source node"
:
289
,
"start line"
:
944
,
"target node"
:
290
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"dev_printk(
\"\\
016
\"
, (struct device const *)(&(card->dev)->dev),
\"
Size %d KB, Battery 1 %s (%s), Battery 2 %s (%s)
\\
n
\"
, card->mm_size, (int)batt_status &1 ? (char *)
\"
Disabled
\"
: (char *)
\"
Enabled
\"
, card->battery[0].good != 0 ? (char *)
\"
OK
\"
: (char *)
\"
FAILURE
\"
, ((int)batt_status &4) != 0 ? (char *)
\"
Disabled
\"
: (char *)
\"
Enabled
\"
, card->battery[1].good != 0 ? (char *)
\"
OK
\"
: (char *)
\"
FAILURE
\"
);"
,
"source node"
:
290
,
"start line"
:
941
,
"target node"
:
291
,
"thread"
:
3
},
{
"enter"
:
33
,
"file"
:
5
,
"source"
:
"set_fault_to_battery_status(card);"
,
"source node"
:
291
,
"start line"
:
949
,
"target node"
:
292
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((card->battery)[0]).good) != 0"
,
"source node"
:
292
,
"start line"
:
657
,
"target node"
:
293
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((card->battery)[1]).good) == 0"
,
"source node"
:
293
,
"start line"
:
657
,
"target node"
:
294
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((card->battery)[0]).warned) == 0"
,
"source node"
:
294
,
"start line"
:
659
,
"target node"
:
295
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((card->battery)[1]).warned) == 0"
,
"source node"
:
295
,
"start line"
:
659
,
"target node"
:
296
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((card->battery)[0]).good) == 0"
,
"source node"
:
296
,
"start line"
:
661
,
"target node"
:
297
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((card->battery)[1]).good) != 0"
,
"source node"
:
297
,
"start line"
:
661
,
"target node"
:
298
,
"thread"
:
3
},
{
"enter"
:
31
,
"file"
:
5
,
"source"
:
"set_led(card, 4, 2);"
,
"source node"
:
298
,
"start line"
:
664
,
"target node"
:
299
,
"thread"
:
3
},
{
"assumption"
:
"state == 2U;"
,
"assumption scope"
:
31
,
"file"
:
5
,
"source"
:
"unsigned char led;"
,
"source node"
:
299
,
"start line"
:
177
,
"target node"
:
300
,
"thread"
:
3
},
{
"enter"
:
18
,
"file"
:
5
,
"source"
:
"led = readb((void const volatile *)(card->csr_remap + 8UL));"
,
"source node"
:
300
,
"start line"
:
179
,
"target node"
:
301
,
"thread"
:
3
},
{
"file"
:
12
,
"source"
:
"unsigned char ret;"
,
"source node"
:
301
,
"start line"
:
55
,
"target node"
:
302
,
"thread"
:
3
},
{
"file"
:
12
,
"return"
:
18
,
"source"
:
"return ret;"
,
"source node"
:
302
,
"start line"
:
53
,
"target node"
:
303
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((unsigned int)state) != 255U"
,
"source node"
:
303
,
"start line"
:
180
,
"target node"
:
304
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"led = (unsigned char)((int)((signed char)led) &~ ((int)((signed char)(3 << shift))));"
,
"source node"
:
304
,
"start line"
:
183
,
"target node"
:
305
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"led = (unsigned char)((int)((signed char)led) | (int)((signed char)((int)state << shift)));"
,
"source node"
:
305
,
"start line"
:
184
,
"target node"
:
306
,
"thread"
:
3
},
{
"enter"
:
32
,
"file"
:
5
,
"source"
:
"writeb((int)led, (void volatile *)(card->csr_remap + 8UL));"
,
"source node"
:
306
,
"start line"
:
186
,
"target node"
:
307
,
"thread"
:
3
},
{
"file"
:
12
,
"return"
:
32
,
"source"
:
"return;"
,
"source node"
:
307
,
"start line"
:
62
,
"target node"
:
308
,
"thread"
:
3
},
{
"file"
:
5
,
"return"
:
31
,
"source"
:
"return;"
,
"source node"
:
308
,
"start line"
:
187
,
"target node"
:
309
,
"thread"
:
3
},
{
"file"
:
5
,
"return"
:
33
,
"source"
:
"return;"
,
"source node"
:
309
,
"start line"
:
665
,
"target node"
:
310
,
"thread"
:
3
},
{
"enter"
:
34
,
"file"
:
5
,
"source"
:
"pci_read_config_dword((struct pci_dev const *)dev, 20, &saved_bar);"
,
"source node"
:
310
,
"start line"
:
952
,
"target node"
:
311
,
"thread"
:
3
},
{
"file"
:
10
,
"return"
:
34
,
"source"
:
"return pci_bus_read_config_dword(dev->bus, dev->devfn, where, val);"
,
"source node"
:
311
,
"start line"
:
845
,
"target node"
:
312
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"data = 4294967295U;"
,
"source node"
:
312
,
"start line"
:
953
,
"target node"
:
313
,
"thread"
:
3
},
{
"enter"
:
35
,
"file"
:
5
,
"source"
:
"pci_write_config_dword((struct pci_dev const *)dev, 20, data);"
,
"source node"
:
313
,
"start line"
:
954
,
"target node"
:
314
,
"thread"
:
3
},
{
"file"
:
10
,
"return"
:
35
,
"source"
:
"return pci_bus_write_config_dword(dev->bus, dev->devfn, where, val);"
,
"source node"
:
314
,
"start line"
:
858
,
"target node"
:
315
,
"thread"
:
3
},
{
"enter"
:
34
,
"file"
:
5
,
"source"
:
"pci_read_config_dword((struct pci_dev const *)dev, 20, &data);"
,
"source node"
:
315
,
"start line"
:
955
,
"target node"
:
316
,
"thread"
:
3
},
{
"file"
:
10
,
"return"
:
34
,
"source"
:
"return pci_bus_read_config_dword(dev->bus, dev->devfn, where, val);"
,
"source node"
:
316
,
"start line"
:
845
,
"target node"
:
317
,
"thread"
:
3
},
{
"enter"
:
35
,
"file"
:
5
,
"source"
:
"pci_write_config_dword((struct pci_dev const *)dev, 20, saved_bar);"
,
"source node"
:
317
,
"start line"
:
956
,
"target node"
:
318
,
"thread"
:
3
},
{
"file"
:
10
,
"return"
:
35
,
"source"
:
"return pci_bus_write_config_dword(dev->bus, dev->devfn, where, val);"
,
"source node"
:
318
,
"start line"
:
858
,
"target node"
:
319
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"data = data &4294967280U;"
,
"source node"
:
319
,
"start line"
:
957
,
"target node"
:
320
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"data = ~ data;"
,
"source node"
:
320
,
"start line"
:
958
,
"target node"
:
321
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"data = data + 1U;"
,
"source node"
:
321
,
"start line"
:
959
,
"target node"
:
322
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
37
,
"file"
:
5
,
"source"
:
"ldv_emg_request_irq(dev->irq, &mm_interrupt, 128UL,
\"
umem
\"
, (void *)card) != 0"
,
"source node"
:
322
,
"start line"
:
961
,
"target node"
:
323
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"irqreturn_t (*ldv_11_callback_handler)(int, void *);"
,
"source node"
:
323
,
"start line"
:
525
,
"target node"
:
324
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"void *ldv_11_data_data;"
,
"source node"
:
324
,
"start line"
:
526
,
"target node"
:
325
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"int ldv_11_line_line;"
,
"source node"
:
325
,
"start line"
:
527
,
"target node"
:
326
,
"thread"
:
3
},
{
"action"
:
2
,
"file"
:
0
,
"source"
:
"irqreturn_t (*ldv_11_thread_thread)(int, void *);"
,
"source node"
:
326
,
"start line"
:
528
,
"target node"
:
327
,
"thread"
:
3
},
{
"action"
:
11
,
"enter"
:
38
,
"file"
:
0
,
"return"
:
37
,
"source"
:
"return ldv_undef_int_negative();"
,
"source node"
:
327
,
"start line"
:
552
,
"target node"
:
328
,
"thread"
:
3
},
{
"file"
:
9
,
"source"
:
"int ret;"
,
"source node"
:
328
,
"start line"
:
54
,
"target node"
:
329
,
"thread"
:
3
},
{
"enter"
:
6
,
"file"
:
9
,
"source"
:
"ret = ldv_undef_int();"
,
"source node"
:
329
,
"start line"
:
54
,
"target node"
:
330
,
"thread"
:
3
},
{
"file"
:
9
,
"return"
:
6
,
"source"
:
"return __VERIFIER_nondet_int();"
,
"source node"
:
330
,
"start line"
:
41
,
"target node"
:
331
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
9
,
"source"
:
"__VERIFIER_assume(ret < 0);"
,
"source node"
:
331
,
"start line"
:
55
,
"target node"
:
332
,
"thread"
:
3
},
{
"file"
:
9
,
"return"
:
38
,
"source"
:
"return ret;"
,
"source node"
:
332
,
"start line"
:
56
,
"target node"
:
333
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"dev_printk(
\"\\
v
\"
, (struct device const *)(&(card->dev)->dev),
\"
Unable to allocate IRQ
\\
n
\"
);"
,
"source node"
:
333
,
"start line"
:
963
,
"target node"
:
334
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"ret = -19;"
,
"source node"
:
334
,
"start line"
:
965
,
"target node"
:
335
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((unsigned long)(((card->mm_pages)[0]).desc)) != ((unsigned long)((struct mm_dma_desc *)0))"
,
"source node"
:
335
,
"start line"
:
1006
,
"target node"
:
336
,
"thread"
:
3
},
{
"enter"
:
39
,
"file"
:
5
,
"source"
:
"pci_free_consistent(card->dev, 8192UL, (void *)card->mm_pages[0].desc, card->mm_pages[0].page_dma);"
,
"source node"
:
336
,
"start line"
:
1007
,
"target node"
:
337
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
11
,
"source"
:
"((unsigned long)hwdev) != ((unsigned long)((struct pci_dev *)0))"
,
"source node"
:
337
,
"start line"
:
26
,
"target node"
:
338
,
"thread"
:
3
},
{
"file"
:
11
,
"source"
:
"&hwdev->dev"
,
"source node"
:
338
,
"start line"
:
26
,
"target node"
:
339
,
"thread"
:
3
},
{
"enter"
:
40
,
"file"
:
11
,
"source"
:
"dma_free_attrs((unsigned long)hwdev != (unsigned long)((struct pci_dev *)0) ? &hwdev->dev : (struct device *)0, size, vaddr, dma_handle, (struct dma_attrs *)0);"
,
"source node"
:
339
,
"start line"
:
26
,
"target node"
:
340
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"struct dma_map_ops *ops;"
,
"source node"
:
340
,
"start line"
:
163
,
"target node"
:
341
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"int __ret_warn_on;"
,
"source node"
:
341
,
"start line"
:
165
,
"target node"
:
342
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"unsigned long _flags;"
,
"source node"
:
342
,
"start line"
:
166
,
"target node"
:
343
,
"thread"
:
3
},
{
"enter"
:
21
,
"file"
:
4
,
"source"
:
"ops = get_dma_ops(dev);"
,
"source node"
:
343
,
"start line"
:
164
,
"target node"
:
344
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
22
,
"file"
:
4
,
"source"
:
"__builtin_expect((unsigned long)dev == (unsigned long)((struct device *)0), 0L) == 0L"
,
"source node"
:
344
,
"start line"
:
37
,
"target node"
:
345
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
345
,
"start line"
:
26
,
"target node"
:
346
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long)(dev->archdata.dma_ops)) != ((unsigned long)((struct dma_map_ops *)0))"
,
"source node"
:
346
,
"start line"
:
37
,
"target node"
:
347
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
21
,
"source"
:
"return dev->archdata.dma_ops;"
,
"source node"
:
347
,
"start line"
:
40
,
"target node"
:
348
,
"thread"
:
3
},
{
"enter"
:
41
,
"file"
:
4
,
"source"
:
"_flags = arch_local_save_flags();"
,
"source node"
:
348
,
"start line"
:
166
,
"target node"
:
349
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __ret;"
,
"source node"
:
349
,
"start line"
:
804
,
"target node"
:
350
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __edi;"
,
"source node"
:
350
,
"start line"
:
805
,
"target node"
:
351
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __esi;"
,
"source node"
:
351
,
"start line"
:
806
,
"target node"
:
352
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __edx;"
,
"source node"
:
352
,
"start line"
:
807
,
"target node"
:
353
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __ecx;"
,
"source node"
:
353
,
"start line"
:
808
,
"target node"
:
354
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __eax;"
,
"source node"
:
354
,
"start line"
:
809
,
"target node"
:
355
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__edi = __edi;"
,
"source node"
:
355
,
"start line"
:
804
,
"target node"
:
356
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__esi = __esi;"
,
"source node"
:
356
,
"start line"
:
804
,
"target node"
:
357
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__edx = __edx;"
,
"source node"
:
357
,
"start line"
:
804
,
"target node"
:
358
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__ecx = __ecx;"
,
"source node"
:
358
,
"start line"
:
804
,
"target node"
:
359
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__eax = __eax;"
,
"source node"
:
359
,
"start line"
:
804
,
"target node"
:
360
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
22
,
"file"
:
16
,
"source"
:
"__builtin_expect((unsigned long)pv_irq_ops.save_fl.func == (unsigned long)((void *)0), 0L) != 0L"
,
"source node"
:
360
,
"start line"
:
804
,
"target node"
:
361
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
361
,
"start line"
:
26
,
"target node"
:
362
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__builtin_unreachable();"
,
"source node"
:
362
,
"start line"
:
804
,
"target node"
:
363
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__ret = __eax;"
,
"source node"
:
363
,
"start line"
:
804
,
"target node"
:
364
,
"thread"
:
3
},
{
"file"
:
16
,
"return"
:
41
,
"source"
:
"return __ret;"
,
"source node"
:
364
,
"start line"
:
804
,
"target node"
:
365
,
"thread"
:
3
},
{
"enter"
:
42
,
"file"
:
4
,
"source"
:
"__ret_warn_on = arch_irqs_disabled_flags(_flags) != 0;"
,
"source node"
:
365
,
"start line"
:
166
,
"target node"
:
366
,
"thread"
:
3
},
{
"file"
:
17
,
"return"
:
42
,
"source"
:
"return (flags &512UL) == 0UL;"
,
"source node"
:
366
,
"start line"
:
157
,
"target node"
:
367
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
22
,
"file"
:
4
,
"source"
:
"__builtin_expect(__ret_warn_on != 0, 0L) != 0L"
,
"source node"
:
367
,
"start line"
:
166
,
"target node"
:
368
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
368
,
"start line"
:
26
,
"target node"
:
369
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"warn_slowpath_null(
\"
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/arch/x86/include/asm/dma-mapping.h
\"
, 166);"
,
"source node"
:
369
,
"start line"
:
166
,
"target node"
:
370
,
"thread"
:
3
},
{
"enter"
:
22
,
"file"
:
4
,
"source"
:
"__builtin_expect(__ret_warn_on != 0, 0L);"
,
"source node"
:
370
,
"start line"
:
166
,
"target node"
:
371
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
371
,
"start line"
:
26
,
"target node"
:
372
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"debug_dma_free_coherent(dev, size, vaddr, bus);"
,
"source node"
:
372
,
"start line"
:
171
,
"target node"
:
373
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"__CPAchecker_TMP_0 != ((unsigned long)((void (*)(struct device *, size_t, void *, dma_addr_t, struct dma_attrs *))0))"
,
"source node"
:
373
,
"start line"
:
172
,
"target node"
:
374
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"(*(ops->free))(dev, size, vaddr, bus, attrs);"
,
"source node"
:
374
,
"start line"
:
173
,
"target node"
:
375
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
40
,
"source"
:
"return;"
,
"source node"
:
375
,
"start line"
:
174
,
"target node"
:
376
,
"thread"
:
3
},
{
"file"
:
11
,
"return"
:
39
,
"source"
:
"return;"
,
"source node"
:
376
,
"start line"
:
27
,
"target node"
:
377
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((unsigned long)(((card->mm_pages)[1]).desc)) != ((unsigned long)((struct mm_dma_desc *)0))"
,
"source node"
:
377
,
"start line"
:
1010
,
"target node"
:
378
,
"thread"
:
3
},
{
"enter"
:
39
,
"file"
:
5
,
"source"
:
"pci_free_consistent(card->dev, 8192UL, (void *)card->mm_pages[1].desc, card->mm_pages[1].page_dma);"
,
"source node"
:
378
,
"start line"
:
1011
,
"target node"
:
379
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
11
,
"source"
:
"((unsigned long)hwdev) != ((unsigned long)((struct pci_dev *)0))"
,
"source node"
:
379
,
"start line"
:
26
,
"target node"
:
380
,
"thread"
:
3
},
{
"file"
:
11
,
"source"
:
"&hwdev->dev"
,
"source node"
:
380
,
"start line"
:
26
,
"target node"
:
381
,
"thread"
:
3
},
{
"enter"
:
40
,
"file"
:
11
,
"source"
:
"dma_free_attrs((unsigned long)hwdev != (unsigned long)((struct pci_dev *)0) ? &hwdev->dev : (struct device *)0, size, vaddr, dma_handle, (struct dma_attrs *)0);"
,
"source node"
:
381
,
"start line"
:
26
,
"target node"
:
382
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"struct dma_map_ops *ops;"
,
"source node"
:
382
,
"start line"
:
163
,
"target node"
:
383
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"int __ret_warn_on;"
,
"source node"
:
383
,
"start line"
:
165
,
"target node"
:
384
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"unsigned long _flags;"
,
"source node"
:
384
,
"start line"
:
166
,
"target node"
:
385
,
"thread"
:
3
},
{
"enter"
:
21
,
"file"
:
4
,
"source"
:
"ops = get_dma_ops(dev);"
,
"source node"
:
385
,
"start line"
:
164
,
"target node"
:
386
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
22
,
"file"
:
4
,
"source"
:
"__builtin_expect((unsigned long)dev == (unsigned long)((struct device *)0), 0L) == 0L"
,
"source node"
:
386
,
"start line"
:
37
,
"target node"
:
387
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
387
,
"start line"
:
26
,
"target node"
:
388
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long)(dev->archdata.dma_ops)) != ((unsigned long)((struct dma_map_ops *)0))"
,
"source node"
:
388
,
"start line"
:
37
,
"target node"
:
389
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
21
,
"source"
:
"return dev->archdata.dma_ops;"
,
"source node"
:
389
,
"start line"
:
40
,
"target node"
:
390
,
"thread"
:
3
},
{
"enter"
:
41
,
"file"
:
4
,
"source"
:
"_flags = arch_local_save_flags();"
,
"source node"
:
390
,
"start line"
:
166
,
"target node"
:
391
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __ret;"
,
"source node"
:
391
,
"start line"
:
804
,
"target node"
:
392
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __edi;"
,
"source node"
:
392
,
"start line"
:
805
,
"target node"
:
393
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __esi;"
,
"source node"
:
393
,
"start line"
:
806
,
"target node"
:
394
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __edx;"
,
"source node"
:
394
,
"start line"
:
807
,
"target node"
:
395
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __ecx;"
,
"source node"
:
395
,
"start line"
:
808
,
"target node"
:
396
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"unsigned long __eax;"
,
"source node"
:
396
,
"start line"
:
809
,
"target node"
:
397
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__edi = __edi;"
,
"source node"
:
397
,
"start line"
:
804
,
"target node"
:
398
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__esi = __esi;"
,
"source node"
:
398
,
"start line"
:
804
,
"target node"
:
399
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__edx = __edx;"
,
"source node"
:
399
,
"start line"
:
804
,
"target node"
:
400
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__ecx = __ecx;"
,
"source node"
:
400
,
"start line"
:
804
,
"target node"
:
401
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__eax = __eax;"
,
"source node"
:
401
,
"start line"
:
804
,
"target node"
:
402
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
22
,
"file"
:
16
,
"source"
:
"__builtin_expect((unsigned long)pv_irq_ops.save_fl.func == (unsigned long)((void *)0), 0L) != 0L"
,
"source node"
:
402
,
"start line"
:
804
,
"target node"
:
403
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
403
,
"start line"
:
26
,
"target node"
:
404
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__builtin_unreachable();"
,
"source node"
:
404
,
"start line"
:
804
,
"target node"
:
405
,
"thread"
:
3
},
{
"file"
:
16
,
"source"
:
"__ret = __eax;"
,
"source node"
:
405
,
"start line"
:
804
,
"target node"
:
406
,
"thread"
:
3
},
{
"file"
:
16
,
"return"
:
41
,
"source"
:
"return __ret;"
,
"source node"
:
406
,
"start line"
:
804
,
"target node"
:
407
,
"thread"
:
3
},
{
"enter"
:
42
,
"file"
:
4
,
"source"
:
"__ret_warn_on = arch_irqs_disabled_flags(_flags) != 0;"
,
"source node"
:
407
,
"start line"
:
166
,
"target node"
:
408
,
"thread"
:
3
},
{
"file"
:
17
,
"return"
:
42
,
"source"
:
"return (flags &512UL) == 0UL;"
,
"source node"
:
408
,
"start line"
:
157
,
"target node"
:
409
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
22
,
"file"
:
4
,
"source"
:
"__builtin_expect(__ret_warn_on != 0, 0L) != 0L"
,
"source node"
:
409
,
"start line"
:
166
,
"target node"
:
410
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
410
,
"start line"
:
26
,
"target node"
:
411
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"warn_slowpath_null(
\"
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/arch/x86/include/asm/dma-mapping.h
\"
, 166);"
,
"source node"
:
411
,
"start line"
:
166
,
"target node"
:
412
,
"thread"
:
3
},
{
"enter"
:
22
,
"file"
:
4
,
"source"
:
"__builtin_expect(__ret_warn_on != 0, 0L);"
,
"source node"
:
412
,
"start line"
:
166
,
"target node"
:
413
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
413
,
"start line"
:
26
,
"target node"
:
414
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"debug_dma_free_coherent(dev, size, vaddr, bus);"
,
"source node"
:
414
,
"start line"
:
171
,
"target node"
:
415
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"__CPAchecker_TMP_0 != ((unsigned long)((void (*)(struct device *, size_t, void *, dma_addr_t, struct dma_attrs *))0))"
,
"source node"
:
415
,
"start line"
:
172
,
"target node"
:
416
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"(*(ops->free))(dev, size, vaddr, bus, attrs);"
,
"source node"
:
416
,
"start line"
:
173
,
"target node"
:
417
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
40
,
"source"
:
"return;"
,
"source node"
:
417
,
"start line"
:
174
,
"target node"
:
418
,
"thread"
:
3
},
{
"file"
:
11
,
"return"
:
39
,
"source"
:
"return;"
,
"source node"
:
418
,
"start line"
:
27
,
"target node"
:
419
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"iounmap((void volatile *)card->csr_remap);"
,
"source node"
:
419
,
"start line"
:
1015
,
"target node"
:
420
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"pci_release_regions(dev);"
,
"source node"
:
420
,
"start line"
:
1017
,
"target node"
:
421
,
"thread"
:
3
},
{
"file"
:
5
,
"return"
:
15
,
"source"
:
"return ret;"
,
"source node"
:
421
,
"start line"
:
1020
,
"target node"
:
422
,
"thread"
:
3
},
{
"enter"
:
43
,
"file"
:
0
,
"source"
:
"ldv_3_ret_default = ldv_post_probe(ldv_3_ret_default);"
,
"source node"
:
422
,
"start line"
:
863
,
"target node"
:
423
,
"thread"
:
3
},
{
"enter"
:
44
,
"file"
:
18
,
"return"
:
43
,
"source"
:
"return ldv_filter_positive_int(probe_ret_val);"
,
"source node"
:
423
,
"start line"
:
39
,
"target node"
:
424
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
18
,
"source"
:
"__VERIFIER_assume(val <= 0);"
,
"source node"
:
424
,
"start line"
:
23
,
"target node"
:
425
,
"thread"
:
3
},
{
"file"
:
18
,
"return"
:
44
,
"source"
:
"return val;"
,
"source node"
:
425
,
"start line"
:
24
,
"target node"
:
426
,
"thread"
:
3
},
{
"enter"
:
5
,
"file"
:
0
,
"source"
:
"ldv_free((void *)ldv_3_ldv_param_17_1_default);"
,
"source node"
:
426
,
"start line"
:
867
,
"target node"
:
427
,
"thread"
:
3
},
{
"file"
:
7
,
"source"
:
"free(s);"
,
"source node"
:
427
,
"start line"
:
63
,
"target node"
:
428
,
"thread"
:
3
},
{
"file"
:
7
,
"return"
:
5
,
"source"
:
"return;"
,
"source node"
:
428
,
"start line"
:
64
,
"target node"
:
429
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
6
,
"file"
:
0
,
"source"
:
"ldv_undef_int() == 0"
,
"source node"
:
429
,
"start line"
:
870
,
"target node"
:
430
,
"thread"
:
3
},
{
"file"
:
9
,
"return"
:
6
,
"source"
:
"return __VERIFIER_nondet_int();"
,
"source node"
:
430
,
"start line"
:
41
,
"target node"
:
431
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
0
,
"source"
:
"__VERIFIER_assume(ldv_3_ret_default != 0);"
,
"source node"
:
431
,
"start line"
:
883
,
"target node"
:
432
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
6
,
"file"
:
0
,
"source"
:
"ldv_undef_int() != 0"
,
"source node"
:
432
,
"start line"
:
852
,
"target node"
:
433
,
"thread"
:
3
},
{
"file"
:
9
,
"return"
:
6
,
"source"
:
"return __VERIFIER_nondet_int();"
,
"source node"
:
433
,
"start line"
:
41
,
"target node"
:
434
,
"thread"
:
3
},
{
"enter"
:
13
,
"file"
:
0
,
"source"
:
"ldv_3_ldv_param_17_1_default = (struct pci_device_id *)ldv_xmalloc_unknown_size(0UL);"
,
"source node"
:
434
,
"start line"
:
854
,
"target node"
:
435
,
"thread"
:
3
},
{
"file"
:
7
,
"source"
:
"void *res;"
,
"source node"
:
435
,
"start line"
:
116
,
"target node"
:
436
,
"thread"
:
3
},
{
"file"
:
7
,
"source"
:
"res = external_allocated_data();"
,
"source node"
:
436
,
"start line"
:
116
,
"target node"
:
437
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
7
,
"source"
:
"__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));"
,
"source node"
:
437
,
"start line"
:
117
,
"target node"
:
438
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
3
,
"file"
:
7
,
"source"
:
"__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);"
,
"source node"
:
438
,
"start line"
:
118
,
"target node"
:
439
,
"thread"
:
3
},
{
"file"
:
8
,
"return"
:
3
,
"source"
:
"return (unsigned long)ptr > 4294967295UL;"
,
"source node"
:
439
,
"start line"
:
22
,
"target node"
:
440
,
"thread"
:
3
},
{
"file"
:
7
,
"return"
:
13
,
"source"
:
"return res;"
,
"source node"
:
440
,
"start line"
:
119
,
"target node"
:
441
,
"thread"
:
3
},
{
"file"
:
0
,
"source"
:
"ldv_pre_probe();"
,
"source node"
:
441
,
"start line"
:
859
,
"target node"
:
442
,
"thread"
:
3
},
{
"enter"
:
15
,
"file"
:
5
,
"original file"
:
0
,
"original start line"
:
861
,
"source"
:
"ldv_3_ret_default = mm_pci_probe(ldv_3_resource_dev, ldv_3_ldv_param_17_1_default);"
,
"source node"
:
442
,
"start line"
:
791
,
"target node"
:
443
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"int ret;"
,
"source node"
:
443
,
"start line"
:
791
,
"target node"
:
444
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"struct cardinfo *card;"
,
"source node"
:
444
,
"start line"
:
792
,
"target node"
:
445
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned char mem_present;"
,
"source node"
:
445
,
"start line"
:
793
,
"target node"
:
446
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned char batt_status;"
,
"source node"
:
446
,
"start line"
:
794
,
"target node"
:
447
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned int saved_bar;"
,
"source node"
:
447
,
"start line"
:
795
,
"target node"
:
448
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned int data;"
,
"source node"
:
448
,
"start line"
:
796
,
"target node"
:
449
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned long csr_base;"
,
"source node"
:
449
,
"start line"
:
797
,
"target node"
:
450
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned long csr_len;"
,
"source node"
:
450
,
"start line"
:
798
,
"target node"
:
451
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"int magic_number;"
,
"source node"
:
451
,
"start line"
:
799
,
"target node"
:
452
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"int printed_version;"
,
"source node"
:
452
,
"start line"
:
800
,
"target node"
:
453
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"struct lock_class_key __key;"
,
"source node"
:
453
,
"start line"
:
810
,
"target node"
:
454
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"unsigned short cfg_command;"
,
"source node"
:
454
,
"start line"
:
811
,
"target node"
:
455
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"ret = -19;"
,
"source node"
:
455
,
"start line"
:
791
,
"target node"
:
456
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card = (struct cardinfo *)(&cards) + (unsigned long)num_cards;"
,
"source node"
:
456
,
"start line"
:
792
,
"target node"
:
457
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"tmp = printed_version;"
,
"source node"
:
457
,
"start line"
:
801
,
"target node"
:
458
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"printed_version = printed_version + 1;"
,
"source node"
:
458
,
"start line"
:
801
,
"target node"
:
459
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"tmp == 0"
,
"source node"
:
459
,
"start line"
:
801
,
"target node"
:
460
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"printk(
\"\\
016v2.3 : Micro Memory(tm) PCI memory board block driver
\\
n
\"
);"
,
"source node"
:
460
,
"start line"
:
802
,
"target node"
:
461
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"ret = pci_enable_device(dev);"
,
"source node"
:
461
,
"start line"
:
804
,
"target node"
:
462
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"ret == 0"
,
"source node"
:
462
,
"start line"
:
805
,
"target node"
:
463
,
"thread"
:
3
},
{
"enter"
:
16
,
"file"
:
5
,
"source"
:
"pci_write_config_byte((struct pci_dev const *)dev, 13, 248);"
,
"source node"
:
463
,
"start line"
:
808
,
"target node"
:
464
,
"thread"
:
3
},
{
"file"
:
10
,
"return"
:
16
,
"source"
:
"return pci_bus_write_config_byte(dev->bus, dev->devfn, where, (int)val);"
,
"source node"
:
464
,
"start line"
:
849
,
"target node"
:
465
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"pci_set_master(dev);"
,
"source node"
:
465
,
"start line"
:
809
,
"target node"
:
466
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->dev = dev;"
,
"source node"
:
466
,
"start line"
:
811
,
"target node"
:
467
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"csr_base = (unsigned long)dev->resource[0].start;"
,
"source node"
:
467
,
"start line"
:
813
,
"target node"
:
468
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((dev->resource)[0]).start) == 0ULL"
,
"source node"
:
468
,
"start line"
:
814
,
"target node"
:
469
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"(((dev->resource)[0]).end) != (((dev->resource)[0]).start)"
,
"source node"
:
469
,
"start line"
:
814
,
"target node"
:
470
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"(unsigned long)((dev->resource[0].end - dev->resource[0].start) + 1ULL)"
,
"source node"
:
470
,
"start line"
:
814
,
"target node"
:
471
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"csr_len = dev->resource[0].start != 0ULL || dev->resource[0].end != dev->resource[0].start ? (unsigned long)((dev->resource[0].end - dev->resource[0].start) + 1ULL) : 0UL;"
,
"source node"
:
471
,
"start line"
:
814
,
"target node"
:
472
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"csr_base != 0UL"
,
"source node"
:
472
,
"start line"
:
815
,
"target node"
:
473
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"csr_len != 0UL"
,
"source node"
:
473
,
"start line"
:
815
,
"target node"
:
474
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"dev_printk(
\"\\
016
\"
, (struct device const *)(&dev->dev),
\"
Micro Memory(tm) controller found (PCI Mem Module (Battery Backup))
\\
n
\"
);"
,
"source node"
:
474
,
"start line"
:
818
,
"target node"
:
475
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
17
,
"file"
:
5
,
"source"
:
"pci_set_dma_mask(dev, 0xffffffffffffffffULL) == 0"
,
"source node"
:
475
,
"start line"
:
821
,
"target node"
:
476
,
"thread"
:
3
},
{
"file"
:
11
,
"return"
:
17
,
"source"
:
"return dma_set_mask(&dev->dev, mask);"
,
"source node"
:
476
,
"start line"
:
107
,
"target node"
:
477
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"ret = pci_request_regions(dev,
\"
umem
\"
);"
,
"source node"
:
477
,
"start line"
:
827
,
"target node"
:
478
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"ret == 0"
,
"source node"
:
478
,
"start line"
:
828
,
"target node"
:
479
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->csr_remap = (unsigned char *)ioremap_nocache((resource_size_t)csr_base, csr_len);"
,
"source node"
:
479
,
"start line"
:
834
,
"target node"
:
480
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"__CPAchecker_TMP_1 != ((unsigned long)((unsigned char *)0U))"
,
"source node"
:
480
,
"start line"
:
835
,
"target node"
:
481
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"dev_printk(
\"\\
016
\"
, (struct device const *)(&(card->dev)->dev),
\"
CSR 0x%08lx -> 0x%p (0x%lx)
\\
n
\"
, csr_base, card->csr_remap, csr_len);"
,
"source node"
:
481
,
"start line"
:
843
,
"target node"
:
482
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"__CPAchecker_TMP_2 == 21525"
,
"source node"
:
482
,
"start line"
:
848
,
"target node"
:
483
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->flags = card->flags | 6;"
,
"source node"
:
483
,
"start line"
:
849
,
"target node"
:
484
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"magic_number = 89;"
,
"source node"
:
484
,
"start line"
:
850
,
"target node"
:
485
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
18
,
"file"
:
5
,
"source"
:
"((int)readb((void const volatile *)card->csr_remap)) == magic_number"
,
"source node"
:
485
,
"start line"
:
869
,
"target node"
:
486
,
"thread"
:
3
},
{
"file"
:
12
,
"source"
:
"unsigned char ret;"
,
"source node"
:
486
,
"start line"
:
55
,
"target node"
:
487
,
"thread"
:
3
},
{
"file"
:
12
,
"return"
:
18
,
"source"
:
"return ret;"
,
"source node"
:
487
,
"start line"
:
53
,
"target node"
:
488
,
"thread"
:
3
},
{
"enter"
:
19
,
"file"
:
5
,
"source"
:
"card->mm_pages[0].desc = (struct mm_dma_desc *)pci_alloc_consistent(card->dev, 8192UL, &card->mm_pages[0].page_dma);"
,
"source node"
:
488
,
"start line"
:
875
,
"target node"
:
489
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
11
,
"source"
:
"((unsigned long)hwdev) != ((unsigned long)((struct pci_dev *)0))"
,
"source node"
:
489
,
"start line"
:
19
,
"target node"
:
490
,
"thread"
:
3
},
{
"file"
:
11
,
"source"
:
"&hwdev->dev"
,
"source node"
:
490
,
"start line"
:
19
,
"target node"
:
491
,
"thread"
:
3
},
{
"enter"
:
20
,
"file"
:
11
,
"return"
:
19
,
"source"
:
"return dma_alloc_attrs((unsigned long)hwdev != (unsigned long)((struct pci_dev *)0) ? &hwdev->dev : (struct device *)0, size, dma_handle, 32U, (struct dma_attrs *)0);"
,
"source node"
:
491
,
"start line"
:
19
,
"target node"
:
492
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
20
,
"file"
:
4
,
"source"
:
"struct dma_map_ops *ops;"
,
"source node"
:
492
,
"start line"
:
134
,
"target node"
:
493
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"void *memory;"
,
"source node"
:
493
,
"start line"
:
136
,
"target node"
:
494
,
"thread"
:
3
},
{
"enter"
:
21
,
"file"
:
4
,
"source"
:
"ops = get_dma_ops(dev);"
,
"source node"
:
494
,
"start line"
:
134
,
"target node"
:
495
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
22
,
"file"
:
4
,
"source"
:
"__builtin_expect((unsigned long)dev == (unsigned long)((struct device *)0), 0L) == 0L"
,
"source node"
:
495
,
"start line"
:
37
,
"target node"
:
496
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
496
,
"start line"
:
26
,
"target node"
:
497
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long)(dev->archdata.dma_ops)) != ((unsigned long)((struct dma_map_ops *)0))"
,
"source node"
:
497
,
"start line"
:
37
,
"target node"
:
498
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
21
,
"source"
:
"return dev->archdata.dma_ops;"
,
"source node"
:
498
,
"start line"
:
40
,
"target node"
:
499
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
20
,
"file"
:
4
,
"source"
:
"gfp = gfp &4294967288U;"
,
"source node"
:
499
,
"start line"
:
137
,
"target node"
:
500
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long)dev) == ((unsigned long)((struct device *)0))"
,
"source node"
:
500
,
"start line"
:
142
,
"target node"
:
501
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"dev = &x86_dma_fallback_dev;"
,
"source node"
:
501
,
"start line"
:
143
,
"target node"
:
502
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
23
,
"file"
:
4
,
"source"
:
"is_device_dma_capable(dev) != 0"
,
"source node"
:
502
,
"start line"
:
145
,
"target node"
:
503
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
14
,
"source"
:
"__CPAchecker_TMP_1 != ((unsigned long)((u64 *)0ULL))"
,
"source node"
:
503
,
"start line"
:
72
,
"target node"
:
504
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
14
,
"source"
:
"(*(dev->dma_mask)) != 0ULL"
,
"source node"
:
504
,
"start line"
:
72
,
"target node"
:
505
,
"thread"
:
3
},
{
"file"
:
14
,
"source"
:
"(unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL"
,
"source node"
:
505
,
"start line"
:
72
,
"target node"
:
506
,
"thread"
:
3
},
{
"file"
:
14
,
"return"
:
23
,
"source"
:
"return (unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL;"
,
"source node"
:
506
,
"start line"
:
72
,
"target node"
:
507
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"__CPAchecker_TMP_0 != ((unsigned long)((void *(*)(struct device *, size_t, dma_addr_t *, gfp_t, struct dma_attrs *))0))"
,
"source node"
:
507
,
"start line"
:
148
,
"target node"
:
508
,
"thread"
:
3
},
{
"enter"
:
24
,
"file"
:
4
,
"source"
:
"memory = (*(ops->alloc))(dev, size, dma_handle, dma_alloc_coherent_gfp_flags(dev, gfp), attrs);"
,
"source node"
:
508
,
"start line"
:
151
,
"target node"
:
509
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
24
,
"file"
:
4
,
"source"
:
"unsigned long dma_mask;"
,
"source node"
:
509
,
"start line"
:
117
,
"target node"
:
510
,
"thread"
:
3
},
{
"enter"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = dma_alloc_coherent_mask(dev, gfp);"
,
"source node"
:
510
,
"start line"
:
117
,
"target node"
:
511
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"unsigned long dma_mask;"
,
"source node"
:
511
,
"start line"
:
105
,
"target node"
:
512
,
"thread"
:
3
},
{
"assumption"
:
"dma_mask == 0UL;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = 0UL;"
,
"source node"
:
512
,
"start line"
:
106
,
"target node"
:
513
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"dma_mask = (unsigned long)dev->coherent_dma_mask;"
,
"source node"
:
513
,
"start line"
:
108
,
"target node"
:
514
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"dma_mask == 0UL"
,
"source node"
:
514
,
"start line"
:
109
,
"target node"
:
515
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"(((int)gfp) &1) == 0"
,
"source node"
:
515
,
"start line"
:
110
,
"target node"
:
516
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"4294967295UL"
,
"source node"
:
516
,
"start line"
:
110
,
"target node"
:
517
,
"thread"
:
3
},
{
"assumption"
:
"dma_mask == 4294967295UL;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = (int)gfp &1 ? 16777215UL : 4294967295UL;"
,
"source node"
:
517
,
"start line"
:
110
,
"target node"
:
518
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
25
,
"source"
:
"return dma_mask;"
,
"source node"
:
518
,
"start line"
:
112
,
"target node"
:
519
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long long)dma_mask) > 16777215ULL"
,
"source node"
:
519
,
"start line"
:
119
,
"target node"
:
520
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long long)dma_mask) > 4294967295ULL"
,
"source node"
:
520
,
"start line"
:
122
,
"target node"
:
521
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
24
,
"source"
:
"return gfp;"
,
"source node"
:
521
,
"start line"
:
125
,
"target node"
:
522
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"debug_dma_alloc_coherent(dev, size, *dma_handle, memory);"
,
"source node"
:
522
,
"start line"
:
153
,
"target node"
:
523
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
20
,
"source"
:
"return memory;"
,
"source node"
:
523
,
"start line"
:
155
,
"target node"
:
524
,
"thread"
:
3
},
{
"enter"
:
19
,
"file"
:
5
,
"source"
:
"card->mm_pages[1].desc = (struct mm_dma_desc *)pci_alloc_consistent(card->dev, 8192UL, &card->mm_pages[1].page_dma);"
,
"source node"
:
524
,
"start line"
:
878
,
"target node"
:
525
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
11
,
"source"
:
"((unsigned long)hwdev) != ((unsigned long)((struct pci_dev *)0))"
,
"source node"
:
525
,
"start line"
:
19
,
"target node"
:
526
,
"thread"
:
3
},
{
"file"
:
11
,
"source"
:
"&hwdev->dev"
,
"source node"
:
526
,
"start line"
:
19
,
"target node"
:
527
,
"thread"
:
3
},
{
"enter"
:
20
,
"file"
:
11
,
"return"
:
19
,
"source"
:
"return dma_alloc_attrs((unsigned long)hwdev != (unsigned long)((struct pci_dev *)0) ? &hwdev->dev : (struct device *)0, size, dma_handle, 32U, (struct dma_attrs *)0);"
,
"source node"
:
527
,
"start line"
:
19
,
"target node"
:
528
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
20
,
"file"
:
4
,
"source"
:
"struct dma_map_ops *ops;"
,
"source node"
:
528
,
"start line"
:
134
,
"target node"
:
529
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"void *memory;"
,
"source node"
:
529
,
"start line"
:
136
,
"target node"
:
530
,
"thread"
:
3
},
{
"enter"
:
21
,
"file"
:
4
,
"source"
:
"ops = get_dma_ops(dev);"
,
"source node"
:
530
,
"start line"
:
134
,
"target node"
:
531
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
22
,
"file"
:
4
,
"source"
:
"__builtin_expect((unsigned long)dev == (unsigned long)((struct device *)0), 0L) == 0L"
,
"source node"
:
531
,
"start line"
:
37
,
"target node"
:
532
,
"thread"
:
3
},
{
"file"
:
13
,
"return"
:
22
,
"source"
:
"return exp;"
,
"source node"
:
532
,
"start line"
:
26
,
"target node"
:
533
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long)(dev->archdata.dma_ops)) != ((unsigned long)((struct dma_map_ops *)0))"
,
"source node"
:
533
,
"start line"
:
37
,
"target node"
:
534
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
21
,
"source"
:
"return dev->archdata.dma_ops;"
,
"source node"
:
534
,
"start line"
:
40
,
"target node"
:
535
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
20
,
"file"
:
4
,
"source"
:
"gfp = gfp &4294967288U;"
,
"source node"
:
535
,
"start line"
:
137
,
"target node"
:
536
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long)dev) == ((unsigned long)((struct device *)0))"
,
"source node"
:
536
,
"start line"
:
142
,
"target node"
:
537
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"dev = &x86_dma_fallback_dev;"
,
"source node"
:
537
,
"start line"
:
143
,
"target node"
:
538
,
"thread"
:
3
},
{
"condition"
:
true
,
"enter"
:
23
,
"file"
:
4
,
"source"
:
"is_device_dma_capable(dev) != 0"
,
"source node"
:
538
,
"start line"
:
145
,
"target node"
:
539
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
14
,
"source"
:
"__CPAchecker_TMP_1 != ((unsigned long)((u64 *)0ULL))"
,
"source node"
:
539
,
"start line"
:
72
,
"target node"
:
540
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
14
,
"source"
:
"(*(dev->dma_mask)) != 0ULL"
,
"source node"
:
540
,
"start line"
:
72
,
"target node"
:
541
,
"thread"
:
3
},
{
"file"
:
14
,
"source"
:
"(unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL"
,
"source node"
:
541
,
"start line"
:
72
,
"target node"
:
542
,
"thread"
:
3
},
{
"file"
:
14
,
"return"
:
23
,
"source"
:
"return (unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL;"
,
"source node"
:
542
,
"start line"
:
72
,
"target node"
:
543
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"__CPAchecker_TMP_0 != ((unsigned long)((void *(*)(struct device *, size_t, dma_addr_t *, gfp_t, struct dma_attrs *))0))"
,
"source node"
:
543
,
"start line"
:
148
,
"target node"
:
544
,
"thread"
:
3
},
{
"enter"
:
24
,
"file"
:
4
,
"source"
:
"memory = (*(ops->alloc))(dev, size, dma_handle, dma_alloc_coherent_gfp_flags(dev, gfp), attrs);"
,
"source node"
:
544
,
"start line"
:
151
,
"target node"
:
545
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
24
,
"file"
:
4
,
"source"
:
"unsigned long dma_mask;"
,
"source node"
:
545
,
"start line"
:
117
,
"target node"
:
546
,
"thread"
:
3
},
{
"enter"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = dma_alloc_coherent_mask(dev, gfp);"
,
"source node"
:
546
,
"start line"
:
117
,
"target node"
:
547
,
"thread"
:
3
},
{
"assumption"
:
"gfp == 32U;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"unsigned long dma_mask;"
,
"source node"
:
547
,
"start line"
:
105
,
"target node"
:
548
,
"thread"
:
3
},
{
"assumption"
:
"dma_mask == 0UL;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = 0UL;"
,
"source node"
:
548
,
"start line"
:
106
,
"target node"
:
549
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"dma_mask = (unsigned long)dev->coherent_dma_mask;"
,
"source node"
:
549
,
"start line"
:
108
,
"target node"
:
550
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"dma_mask == 0UL"
,
"source node"
:
550
,
"start line"
:
109
,
"target node"
:
551
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"(((int)gfp) &1) == 0"
,
"source node"
:
551
,
"start line"
:
110
,
"target node"
:
552
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"4294967295UL"
,
"source node"
:
552
,
"start line"
:
110
,
"target node"
:
553
,
"thread"
:
3
},
{
"assumption"
:
"dma_mask == 4294967295UL;"
,
"assumption scope"
:
25
,
"file"
:
4
,
"source"
:
"dma_mask = (int)gfp &1 ? 16777215UL : 4294967295UL;"
,
"source node"
:
553
,
"start line"
:
110
,
"target node"
:
554
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
25
,
"source"
:
"return dma_mask;"
,
"source node"
:
554
,
"start line"
:
112
,
"target node"
:
555
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long long)dma_mask) > 16777215ULL"
,
"source node"
:
555
,
"start line"
:
119
,
"target node"
:
556
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
4
,
"source"
:
"((unsigned long long)dma_mask) > 4294967295ULL"
,
"source node"
:
556
,
"start line"
:
122
,
"target node"
:
557
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
24
,
"source"
:
"return gfp;"
,
"source node"
:
557
,
"start line"
:
125
,
"target node"
:
558
,
"thread"
:
3
},
{
"file"
:
4
,
"source"
:
"debug_dma_alloc_coherent(dev, size, *dma_handle, memory);"
,
"source node"
:
558
,
"start line"
:
153
,
"target node"
:
559
,
"thread"
:
3
},
{
"file"
:
4
,
"return"
:
20
,
"source"
:
"return memory;"
,
"source node"
:
559
,
"start line"
:
155
,
"target node"
:
560
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((unsigned long)(((card->mm_pages)[0]).desc)) != ((unsigned long)((struct mm_dma_desc *)0))"
,
"source node"
:
560
,
"start line"
:
881
,
"target node"
:
561
,
"thread"
:
3
},
{
"condition"
:
true
,
"file"
:
5
,
"source"
:
"((unsigned long)(((card->mm_pages)[1]).desc)) != ((unsigned long)((struct mm_dma_desc *)0))"
,
"source node"
:
561
,
"start line"
:
881
,
"target node"
:
562
,
"thread"
:
3
},
{
"enter"
:
26
,
"file"
:
5
,
"source"
:
"reset_page((struct mm_page *)(&card->mm_pages));"
,
"source node"
:
562
,
"start line"
:
886
,
"target node"
:
563
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->cnt = 0;"
,
"source node"
:
563
,
"start line"
:
328
,
"target node"
:
564
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->headcnt = 0;"
,
"source node"
:
564
,
"start line"
:
329
,
"target node"
:
565
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->bio = (struct bio *)0;"
,
"source node"
:
565
,
"start line"
:
330
,
"target node"
:
566
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->biotail = &page->bio;"
,
"source node"
:
566
,
"start line"
:
331
,
"target node"
:
567
,
"thread"
:
3
},
{
"file"
:
5
,
"return"
:
26
,
"source"
:
"return;"
,
"source node"
:
567
,
"start line"
:
332
,
"target node"
:
568
,
"thread"
:
3
},
{
"enter"
:
26
,
"file"
:
5
,
"source"
:
"reset_page((struct mm_page *)(&card->mm_pages) + 1UL);"
,
"source node"
:
568
,
"start line"
:
887
,
"target node"
:
569
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->cnt = 0;"
,
"source node"
:
569
,
"start line"
:
328
,
"target node"
:
570
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->headcnt = 0;"
,
"source node"
:
570
,
"start line"
:
329
,
"target node"
:
571
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->bio = (struct bio *)0;"
,
"source node"
:
571
,
"start line"
:
330
,
"target node"
:
572
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"page->biotail = &page->bio;"
,
"source node"
:
572
,
"start line"
:
331
,
"target node"
:
573
,
"thread"
:
3
},
{
"file"
:
5
,
"return"
:
26
,
"source"
:
"return;"
,
"source node"
:
573
,
"start line"
:
332
,
"target node"
:
574
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->Ready = 0;"
,
"source node"
:
574
,
"start line"
:
888
,
"target node"
:
575
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->Active = -1;"
,
"source node"
:
575
,
"start line"
:
889
,
"target node"
:
576
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->bio = (struct bio *)0;"
,
"source node"
:
576
,
"start line"
:
890
,
"target node"
:
577
,
"thread"
:
3
},
{
"file"
:
5
,
"source"
:
"card->biotail = &card->bio;"
,
"source node"
:
577
,
"start line"
:
891
,
"target node"
:
578
,
"thread"
:
3
},
{
"enter"
:
27
,
"file"
:
5
,
"source"
:
"card->queue = ldv_blk_alloc_queue_10(208U);"
,
"source node"
:
578
,
"start line"
:
893
,
"target node"
:
579
,
"thread"
:
3
},
{
"file"
:
0
,
"source"
:
"ldv_func_ret_type ldv_func_res;"
,
"source node"
:
579
,
"start line"
:
1146
,
"target node"
:
580
,
"thread"
:
3
},
{
"file"
:
0
,
"source"
:
"ldv_func_res = blk_alloc_queue(ldv_func_arg1);"
,
"source node"
:
580
,
"start line"
:
1148
,
"target node"
:
581
,
"thread"
:
3
},
{
"enter"
:
28
,
"file"
:
0
,
"source"
:
"ldv_request_queue();"
,
"source node"
:
581
,
"start line"
:
1150
,
"target node"
:
582
,
"thread"
:
3
,
"warn"
:
"Queue should not be allocated twice."
},
{
"file"
:
6
,
"source"
:
"struct request_queue *res;"
,
"source node"
:
582
,
"start line"
:
35
,
"target node"
:
583
,
"thread"
:
3
},
{
"enter"
:
29
,
"file"
:
6
,
"note"
:
"Choose an arbitrary return value."
,
"source"
:
"res = (struct request_queue *)ldv_undef_ptr();"
,
"source node"
:
583
,
"start line"
:
38
,
"target node"
:
584
,
"thread"
:
3
},
{
"file"
:
9
,
"return"
:
29
,
"source"
:
"return __VERIFIER_nondet_pointer();"
,
"source node"
:
584
,
"start line"
:
45
,
"target node"
:
585
,
"thread"
:
3
},
{
"enter"
:
30
,
"file"
:
6
,
"note"
:
"Queue should not be allocated twice."
,
"source"
:
"ldv_assert_linux_block_queue__double_allocation(ldv_queue_state == 0);"
,
"source node"
:
585
,
"start line"
:
36
,
"target node"
:
586
,
"thread"
:
3
},
{
"assumption"
:
"expr == 0;"
,
"assumption scope"
:
30
,
"condition"
:
true
,
"file"
:
15
,
"source"
:
"expr == 0"
,
"source node"
:
586
,
"start line"
:
4
,
"target node"
:
587
,
"thread"
:
3
},
{
"file"
:
15
,
"source"
:
"__VERIFIER_error();"
,
"source node"
:
587
,
"start line"
:
5
,
"target node"
:
588
,
"thread"
:
3
}
],
"entry node"
:
0
,
"files"
:
[
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/avtg/drivers/block/umem.ko/linux:block:queue/weaver/.tmp_umem.c.aux"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/include/linux/export.h"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/arch/x86/include/asm/paravirt_types.h"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/include/linux/jiffies.h"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/arch/x86/include/asm/dma-mapping.h"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/drivers/block/umem.c"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/job/root/linux/block/queue.c"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/job/root/verifier/memory.c"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/job/root/linux/err.c"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/job/root/verifier/nondet.c"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/include/linux/pci.h"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/include/asm-generic/pci-dma-compat.h"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/arch/x86/include/asm/io.h"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/job/root/verifier/gcc.c"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/include/linux/dma-mapping.h"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/vtg/drivers/block/umem.ko/linux:block:queue/rsb/bug kind funcs.c"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/arch/x86/include/asm/paravirt.h"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/lkbce/arch/x86/include/asm/irqflags.h"
,
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/97773e6cc7ede3176f4428a61159eccd/klever-core-work-dir/job/root/linux/ldv/common.c"
],
"funcs"
:
[
"ldv_main_14"
,
"ldv_dispatch_insmod_register_14_3"
,
"ldv_xmalloc"
,
"ldv_is_err"
,
"ldv_insmod_6"
,
"ldv_free"
,
"ldv_undef_int"
,
"ldv_insmod_mm_init_6_9"
,
"mm_init"
,
"ldv___pci_register_driver_14"
,
"ldv_emg___pci_register_driver"
,
"ldv_dispatch_register_13_3"
,
"ldv_pci_scenario_3"
,
"ldv_xmalloc_unknown_size"
,
"ldv_pci_scenario_probe_3_17"
,
"mm_pci_probe"
,
"pci_write_config_byte"
,
"pci_set_dma_mask"
,
"readb"
,
"pci_alloc_consistent"
,
"dma_alloc_attrs"
,
"get_dma_ops"
,
"__builtin_expect"
,
"is_device_dma_capable"
,
"dma_alloc_coherent_gfp_flags"
,
"dma_alloc_coherent_mask"
,
"reset_page"
,
"ldv_blk_alloc_queue_10"
,
"ldv_request_queue"
,
"ldv_undef_ptr"
,
"ldv_assert_linux_block_queue__double_allocation"
,
"set_led"
,
"writeb"
,
"set_fault_to_battery_status"
,
"pci_read_config_dword"
,
"pci_write_config_dword"
,
"ldv_request_irq_11"
,
"ldv_emg_request_irq"
,
"ldv_undef_int_negative"
,
"pci_free_consistent"
,
"dma_free_attrs"
,
"arch_local_save_flags"
,
"arch_irqs_disabled_flags"
,
"ldv_post_probe"
,
"ldv_filter_positive_int"
],
"nodes"
:
[
[
null
,
0
],
[
0
,
1
],
[
1
,
2
],
[
2
,
3
],
[
3
,
4
],
[
4
,
5
],
[
5
,
6
],
[
6
,
7
],
[
7
,
8
],
[
8
,
9
],
[
9
,
10
],
[
10
,
11
],
[
11
,
12
],
[
12
,
13
],
[
13
,
14
],
[
14
,
15
],
[
15
,
16
],
[
16
,
17
],
[
17
,
18
],
[
18
,
19
],
[
19
,
20
],
[
20
,
21
],
[
21
,
22
],
[
22
,
23
],
[
23
,
24
],
[
24
,
25
],
[
25
,
26
],
[
26
,
27
],
[
27
,
28
],
[
28
,
29
],
[
29
,
30
],
[
30
,
31
],
[
31
,
32
],
[
32
,
33
],
[
33
,
34
],
[
34
,
35
],
[
35
,
36
],
[
36
,
37
],
[
37
,
38
],
[
38
,
39
],
[
39
,
40
],
[
40
,
41
],
[
41
,
42
],
[
42
,
43
],
[
43
,
44
],
[
44
,
45
],
[
45
,
46
],
[
46
,
47
],
[
47
,
48
],
[
48
,
49
],
[
49
,
50
],
[
50
,
51
],
[
51
,
52
],
[
52
,
53
],
[
53
,
54
],
[
54
,
55
],
[
55
,
56
],
[
56
,
57
],
[
57
,
58
],
[
58
,
59
],
[
59
,
60
],
[
60
,
61
],
[
61
,
62
],
[
62
,
63
],
[
63
,
64
],
[
64
,
65
],
[
65
,
66
],
[
66
,
67
],
[
67
,
68
],
[
68
,
69
],
[
69
,
70
],
[
70
,
71
],
[
71
,
72
],
[
72
,
73
],
[
73
,
74
],
[
74
,
75
],
[
75
,
76
],
[
76
,
77
],
[
77
,
78
],
[
78
,
79
],
[
79
,
80
],
[
80
,
81
],
[
81
,
82
],
[
82
,
83
],
[
83
,
84
],
[
84
,
85
],
[
85
,
86
],
[
86
,
87
],
[
87
,
88
],
[
88
,
89
],
[
89
,
90
],
[
90
,
91
],
[
91
,
92
],
[
92
,
93
],
[
93
,
94
],
[
94
,
95
],
[
95
,
96
],
[
96
,
97
],
[
97
,
98
],
[
98
,
99
],
[
99
,
100
],
[
100
,
101
],
[
101
,
102
],
[
102
,
103
],
[
103
,
104
],
[
104
,
105
],
[
105
,
106
],
[
106
,
107
],
[
107
,
108
],
[
108
,
109
],
[
109
,
110
],
[
110
,
111
],
[
111
,
112
],
[
112
,
113
],
[
113
,
114
],
[
114
,
115
],
[
115
,
116
],
[
116
,
117
],
[
117
,
118
],
[
118
,
119
],
[
119
,
120
],
[
120
,
121
],
[
121
,
122
],
[
122
,
123
],
[
123
,
124
],
[
124
,
125
],
[
125
,
126
],
[
126
,
127
],
[
127
,
128
],
[
128
,
129
],
[
129
,
130
],
[
130
,
131
],
[
131
,
132
],
[
132
,
133
],
[
133
,
134
],
[
134
,
135
],
[
135
,
136
],
[
136
,
137
],
[
137
,
138
],
[
138
,
139
],
[
139
,
140
],
[
140
,
141
],
[
141
,
142
],
[
142
,
143
],
[
143
,
144
],
[
144
,
145
],
[
145
,
146
],
[
146
,
147
],
[
147
,
148
],
[
148
,
149
],
[
149
,
150
],
[
150
,
151
],
[
151
,
152
],
[
152
,
153
],
[
153
,
154
],
[
154
,
155
],
[
155
,
156
],
[
156
,
157
],
[
157
,
158
],
[
158
,
159
],
[
159
,
160
],
[
160
,
161
],
[
161
,
162
],
[
162
,
163
],
[
163
,
164
],
[
164
,
165
],
[
165
,
166
],
[
166
,
167
],
[
167
,
168
],
[
168
,
169
],
[
169
,
170
],
[
170
,
171
],
[
171
,
172
],
[
172
,
173
],
[
173
,
174
],
[
174
,
175
],
[
175
,
176
],
[
176
,
177
],
[
177
,
178
],
[
178
,
179
],
[
179
,
180
],
[
180
,
181
],
[
181
,
182
],
[
182
,
183
],
[
183
,
184
],
[
184
,
185
],
[
185
,
186
],
[
186
,
187
],
[
187
,
188
],
[
188
,
189
],
[
189
,
190
],
[
190
,
191
],
[
191
,
192
],
[
192
,
193
],
[
193
,
194
],
[
194
,
195
],
[
195
,
196
],
[
196
,
197
],
[
197
,
198
],
[
198
,
199
],
[
199
,
200
],
[
200
,
201
],
[
201
,
202
],
[
202
,
203
],
[
203
,
204
],
[
204
,
205
],
[
205
,
206
],
[
206
,
207
],
[
207
,
208
],
[
208
,
209
],
[
209
,
210
],
[
210
,
211
],
[
211
,
212
],
[
212
,
213
],
[
213
,
214
],
[
214
,
215
],
[
215
,
216
],
[
216
,
217
],
[
217
,
218
],
[
218
,
219
],
[
219
,
220
],
[
220
,
221
],
[
221
,
222
],
[
222
,
223
],
[
223
,
224
],
[
224
,
225
],
[
225
,
226
],
[
226
,
227
],
[
227
,
228
],
[
228
,
229
],
[
229
,
230
],
[
230
,
231
],
[
231
,
232
],
[
232
,
233
],
[
233
,
234
],
[
234
,
235
],
[
235
,
236
],
[
236
,
237
],
[
237
,
238
],
[
238
,
239
],
[
239
,
240
],
[
240
,
241
],
[
241
,
242
],
[
242
,
243
],
[
243
,
244
],
[
244
,
245
],
[
245
,
246
],
[
246
,
247
],
[
247
,
248
],
[
248
,
249
],
[
249
,
250
],
[
250
,
251
],
[
251
,
252
],
[
252
,
253
],
[
253
,
254
],
[
254
,
255
],
[
255
,
256
],
[
256
,
257
],
[
257
,
258
],
[
258
,
259
],
[
259
,
260
],
[
260
,
261
],
[
261
,
262
],
[
262
,
263
],
[
263
,
264
],
[
264
,
265
],
[
265
,
266
],
[
266
,
267
],
[
267
,
268
],
[
268
,
269
],
[
269
,
270
],
[
270
,
271
],
[
271
,
272
],
[
272
,
273
],
[
273
,
274
],
[
274
,
275
],
[
275
,
276
],
[
276
,
277
],
[
277
,
278
],
[
278
,
279
],
[
279
,
280
],
[
280
,
281
],
[
281
,
282
],
[
282
,
283
],
[
283
,
284
],
[
284
,
285
],
[
285
,
286
],
[
286
,
287
],
[
287
,
288
],
[
288
,
289
],
[
289
,
290
],
[
290
,
291
],
[
291
,
292
],
[
292
,
293
],
[
293
,
294
],
[
294
,
295
],
[
295
,
296
],
[
296
,
297
],
[
297
,
298
],
[
298
,
299
],
[
299
,
300
],
[
300
,
301
],
[
301
,
302
],
[
302
,
303
],
[
303
,
304
],
[
304
,
305
],
[
305
,
306
],
[
306
,
307
],
[
307
,
308
],
[
308
,
309
],
[
309
,
310
],
[
310
,
311
],
[
311
,
312
],
[
312
,
313
],
[
313
,
314
],
[
314
,
315
],
[
315
,
316
],
[
316
,
317
],
[
317
,
318
],
[
318
,
319
],
[
319
,
320
],
[
320
,
321
],
[
321
,
322
],
[
322
,
323
],
[
323
,
324
],
[
324
,
325
],
[
325
,
326
],
[
326
,
327
],
[
327
,
328
],
[
328
,
329
],
[
329
,
330
],
[
330
,
331
],
[
331
,
332
],
[
332
,
333
],
[
333
,
334
],
[
334
,
335
],
[
335
,
336
],
[
336
,
337
],
[
337
,
338
],
[
338
,
339
],
[
339
,
340
],
[
340
,
341
],
[
341
,
342
],
[
342
,
343
],
[
343
,
344
],
[
344
,
345
],
[
345
,
346
],
[
346
,
347
],
[
347
,
348
],
[
348
,
349
],
[
349
,
350
],
[
350
,
351
],
[
351
,
352
],
[
352
,
353
],
[
353
,
354
],
[
354
,
355
],
[
355
,
356
],
[
356
,
357
],
[
357
,
358
],
[
358
,
359
],
[
359
,
360
],
[
360
,
361
],
[
361
,
362
],
[
362
,
363
],
[
363
,
364
],
[
364
,
365
],
[
365
,
366
],
[
366
,
367
],
[
367
,
368
],
[
368
,
369
],
[
369
,
370
],
[
370
,
371
],
[
371
,
372
],
[
372
,
373
],
[
373
,
374
],
[
374
,
375
],
[
375
,
376
],
[
376
,
377
],
[
377
,
378
],
[
378
,
379
],
[
379
,
380
],
[
380
,
381
],
[
381
,
382
],
[
382
,
383
],
[
383
,
384
],
[
384
,
385
],
[
385
,
386
],
[
386
,
387
],
[
387
,
388
],
[
388
,
389
],
[
389
,
390
],
[
390
,
391
],
[
391
,
392
],
[
392
,
393
],
[
393
,
394
],
[
394
,
395
],
[
395
,
396
],
[
396
,
397
],
[
397
,
398
],
[
398
,
399
],
[
399
,
400
],
[
400
,
401
],
[
401
,
402
],
[
402
,
403
],
[
403
,
404
],
[
404
,
405
],
[
405
,
406
],
[
406
,
407
],
[
407
,
408
],
[
408
,
409
],
[
409
,
410
],
[
410
,
411
],
[
411
,
412
],
[
412
,
413
],
[
413
,
414
],
[
414
,
415
],
[
415
,
416
],
[
416
,
417
],
[
417
,
418
],
[
418
,
419
],
[
419
,
420
],
[
420
,
421
],
[
421
,
422
],
[
422
,
423
],
[
423
,
424
],
[
424
,
425
],
[
425
,
426
],
[
426
,
427
],
[
427
,
428
],
[
428
,
429
],
[
429
,
430
],
[
430
,
431
],
[
431
,
432
],
[
432
,
433
],
[
433
,
434
],
[
434
,
435
],
[
435
,
436
],
[
436
,
437
],
[
437
,
438
],
[
438
,
439
],
[
439
,
440
],
[
440
,
441
],
[
441
,
442
],
[
442
,
443
],
[
443
,
444
],
[
444
,
445
],
[
445
,
446
],
[
446
,
447
],
[
447
,
448
],
[
448
,
449
],
[
449
,
450
],
[
450
,
451
],
[
451
,
452
],
[
452
,
453
],
[
453
,
454
],
[
454
,
455
],
[
455
,
456
],
[
456
,
457
],
[
457
,
458
],
[
458
,
459
],
[
459
,
460
],
[
460
,
461
],
[
461
,
462
],
[
462
,
463
],
[
463
,
464
],
[
464
,
465
],
[
465
,
466
],
[
466
,
467
],
[
467
,
468
],
[
468
,
469
],
[
469
,
470
],
[
470
,
471
],
[
471
,
472
],
[
472
,
473
],
[
473
,
474
],
[
474
,
475
],
[
475
,
476
],
[
476
,
477
],
[
477
,
478
],
[
478
,
479
],
[
479
,
480
],
[
480
,
481
],
[
481
,
482
],
[
482
,
483
],
[
483
,
484
],
[
484
,
485
],
[
485
,
486
],
[
486
,
487
],
[
487
,
488
],
[
488
,
489
],
[
489
,
490
],
[
490
,
491
],
[
491
,
492
],
[
492
,
493
],
[
493
,
494
],
[
494
,
495
],
[
495
,
496
],
[
496
,
497
],
[
497
,
498
],
[
498
,
499
],
[
499
,
500
],
[
500
,
501
],
[
501
,
502
],
[
502
,
503
],
[
503
,
504
],
[
504
,
505
],
[
505
,
506
],
[
506
,
507
],
[
507
,
508
],
[
508
,
509
],
[
509
,
510
],
[
510
,
511
],
[
511
,
512
],
[
512
,
513
],
[
513
,
514
],
[
514
,
515
],
[
515
,
516
],
[
516
,
517
],
[
517
,
518
],
[
518
,
519
],
[
519
,
520
],
[
520
,
521
],
[
521
,
522
],
[
522
,
523
],
[
523
,
524
],
[
524
,
525
],
[
525
,
526
],
[
526
,
527
],
[
527
,
528
],
[
528
,
529
],
[
529
,
530
],
[
530
,
531
],
[
531
,
532
],
[
532
,
533
],
[
533
,
534
],
[
534
,
535
],
[
535
,
536
],
[
536
,
537
],
[
537
,
538
],
[
538
,
539
],
[
539
,
540
],
[
540
,
541
],
[
541
,
542
],
[
542
,
543
],
[
543
,
544
],
[
544
,
545
],
[
545
,
546
],
[
546
,
547
],
[
547
,
548
],
[
548
,
549
],
[
549
,
550
],
[
550
,
551
],
[
551
,
552
],
[
552
,
553
],
[
553
,
554
],
[
554
,
555
],
[
555
,
556
],
[
556
,
557
],
[
557
,
558
],
[
558
,
559
],
[
559
,
560
],
[
560
,
561
],
[
561
,
562
],
[
562
,
563
],
[
563
,
564
],
[
564
,
565
],
[
565
,
566
],
[
566
,
567
],
[
567
,
568
],
[
568
,
569
],
[
569
,
570
],
[
570
,
571
],
[
571
,
572
],
[
572
,
573
],
[
573
,
574
],
[
574
,
575
],
[
575
,
576
],
[
576
,
577
],
[
577
,
578
],
[
578
,
579
],
[
579
,
580
],
[
580
,
581
],
[
581
,
582
],
[
582
,
583
],
[
583
,
584
],
[
584
,
585
],
[
585
,
586
],
[
586
,
587
],
[
587
,
null
]
],
"violation nodes"
:
[
588
]
}
« Previous
1
2
Next »
(1-1/2)
Loading...
