Project

General

Profile

Download (326 KB)

Bug #8046 » error-trace.json

Evgeny Novikov, 04/24/2017 04:50 PM

 
{
"actions": [
"Initialize rule models.",
"Start environment model scenarios.",
"Declare auxiliary variables.",
"Trigger module initialization.",
"Initialize the module after insmod with 'skfddi_pci_driver_init' function. Invoke callback skfddi_pci_driver_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.",
"Get network device structure.",
"Switch network device to the up state. Invoke callback ndo_open from net_device_ops.",
"Get line, callbacks and data arguments.",
"Register interrupt callback (callbacks).",
"An interrupt is registered.",
"An interrupt happens, execute the bottom half function to handle it. Invoke callback handler from INTERRUPT."
],
"callback actions": [
4,
10,
12,
16
],
"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 char const * const boot_msg = (char const */* const */)\"SysKonnect FDDI PCI Adapter driver v2.07 for\\n SK-55xx/SK-58xx adapters (SK-NET FDDI-FP/UP/LP)\";",
"source node": 5,
"start line": 70,
"target node": 6,
"thread": 0
},
{
"file": 5,
"source": "static struct pci_device_id const skfddi_pci_tbl[2U] = { {4424U, 16384U, 4294967295U, 4294967295U, 0U, 0U, 0UL}};",
"source node": 6,
"start line": 152,
"target node": 7,
"thread": 0
},
{
"file": 5,
"source": "struct pci_device_id const __mod_pci_device_table;",
"source node": 7,
"start line": 156,
"target node": 8,
"thread": 0
},
{
"file": 5,
"source": "static int num_boards;",
"source node": 8,
"start line": 162,
"target node": 9,
"thread": 0
},
{
"file": 5,
"source": "static struct net_device_ops const skfp_netdev_ops = #line 164 {0, 0, &skfp_open, &skfp_close, &skfp_send_pkt, 0, 0, &skfp_ctl_set_multicast_list, &skfp_ctl_set_mac_address, 0, &skfp_ioctl, 0, &fddi_change_mtu, 0, 0, 0, &skfp_ctl_get_stats, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0};",
"source node": 9,
"start line": 164,
"target node": 10,
"thread": 0
},
{
"file": 5,
"source": "static struct pci_driver skfddi_pci_driver = #line 2241 {{0, 0}, \"skfddi\", (struct pci_device_id const *)(&skfddi_pci_tbl), &skfp_init_one, &skfp_remove_one, 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": 10,
"start line": 2241,
"target node": 11,
"thread": 0
},
{
"file": 0,
"source": "struct ldv_thread ldv_thread_13;",
"source node": 11,
"start line": 106,
"target node": 12,
"thread": 0
},
{
"file": 0,
"source": "struct ldv_thread ldv_thread_2;",
"source node": 12,
"start line": 107,
"target node": 13,
"thread": 0
},
{
"file": 0,
"source": "struct ldv_thread ldv_thread_3;",
"source node": 13,
"start line": 108,
"target node": 14,
"thread": 0
},
{
"file": 0,
"source": "struct ldv_thread ldv_thread_4;",
"source node": 14,
"start line": 109,
"target node": 15,
"thread": 0
},
{
"file": 0,
"source": "struct ldv_thread ldv_thread_5;",
"source node": 15,
"start line": 110,
"target node": 16,
"thread": 0
},
{
"file": 6,
"source": "struct fddi_addr const fddi_broadcast;",
"source node": 16,
"start line": 470,
"target node": 17,
"thread": 0
},
{
"file": 7,
"source": "extern unsigned char const byte_rev_table[256U];",
"source node": 17,
"start line": 6,
"target node": 18,
"thread": 0
},
{
"file": 8,
"source": "static char write_mdr_warning[35U] = #line 53 { 'E', '3', '5', '0', ' ', 'w', 'r', 'i', 't', 'e', '_', 'm', 'd', 'r', '(', ')', ' ', 'F', 'M', '_', 'S', 'N', 'P', 'P', 'N', 'D', ' ', 'i', 's', ' ', 's', 'e', 't', '\\n', '\\000'};",
"source node": 18,
"start line": 53,
"target node": 19,
"thread": 0
},
{
"file": 8,
"source": "static char cam_warning[27U] = #line 54 { 'E', '_', 'S', 'M', 'T', '_', '0', '0', '4', ':', ' ', 'C', 'A', 'M', ' ', 's', 't', 'i', 'l', 'l', ' ', 'b', 'u', 's', 'y', '\\n', '\\000'};",
"source node": 19,
"start line": 54,
"target node": 20,
"thread": 0
},
{
"file": 8,
"source": "struct fddi_addr const fddi_broadcast = {{255U, 255U, 255U, 255U, 255U, 255U}};",
"source node": 20,
"start line": 73,
"target node": 21,
"thread": 0
},
{
"file": 8,
"source": "static struct fddi_addr const null_addr = {{0U, 0U, 0U, 0U, 0U, 0U}};",
"source node": 21,
"start line": 74,
"target node": 22,
"thread": 0
},
{
"file": 8,
"source": "static struct fddi_addr const dbeacon_multi = {{1U, 128U, 194U, 0U, 1U, 0U}};",
"source node": 22,
"start line": 75,
"target node": 23,
"thread": 0
},
{
"file": 8,
"source": "static unsigned short const my_said = 65535U;",
"source node": 23,
"start line": 77,
"target node": 24,
"thread": 0
},
{
"file": 8,
"source": "static unsigned short const my_sagp = 65535U;",
"source node": 24,
"start line": 78,
"target node": 25,
"thread": 0
},
{
"file": 9,
"source": "static struct fddi_addr const SMT_Unknown = {{0U, 0U, 31U, 0U, 0U, 0U}};",
"source node": 25,
"start line": 53,
"target node": 26,
"thread": 0
},
{
"file": 9,
"source": "static u_short const plist_nif[4U] = { 1U, 2U, 3U, 0U};",
"source node": 26,
"start line": 151,
"target node": 27,
"thread": 0
},
{
"file": 9,
"source": "static struct smt_pdef const smt_pdef[41U] = #line 1577 { {1, 12, \"s6\"}, {2, 8, \"1111\"}, {3, 8, \"scc\"}, {4, 12, \"8\"}, {5, 8, \"ss\"}, {6, 12, \"ssss\"}, {7, 20, \"ss66\"}, {8, 28, \"[6s]\"}, {9, 44, \"sslllllllll\"}, {10, 20, \"ssccccll\"}, {11, 16, \"ssll\"}, {12, 12, \"ssl\"}, {13, 36, \"ssl\"}, {14, 12, \"ssl\"}, {15, 36, \"\"}, {18, 8, \"l\"}, {19, 40, \"l\"}, {20, 12, \"sccss\"}, {21, 8, \"l\"}, {22, 8, \"l\"}, {23, 8, \"l\"}, {24, 8, \"l\"}, {25, 12, \"s6\"}, {26, 8, \"l\"}, {27, 8, \"l\"}, {28, 8, \"l\"}, {29, 8, \"l\"}, {4149, 0, \"l8\"}, {4168, 0, \"ll\"}, {8332, 0, \"4lss66\"}, {8333, 0, \"4lllll\"}, {8334, 0, \"4llll\"}, {8335, 0, \"4ll6666s6\"}, {8336, 0, \"4lssl\"}, {12811, 12, \"42s\"}, {12815, 12, \"4l\"}, {12816, 12, \"4l\"}, {16464, 0, \"4l1111ll\"}, {16465, 0, \"4lssss\"}, {16466, 0, \"4ll\"}, {16467, 0, \"4lsslss\"}};",
"source node": 27,
"start line": 1577,
"target node": 28,
"thread": 0
},
{
"file": 10,
"source": "static unsigned char const cf_to_ptype[13U] = #line 76 \"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/cfm.c\" { 4U, 4U, 4U, 4U, 4U, 4U, 1U, 1U, 2U, 0U, 1U, 2U, 1U};",
"source node": 28,
"start line": 76,
"target node": 29,
"thread": 0
},
{
"file": 10,
"source": "static char path_iso[24U] = #line 560 { 0, 0, 0, 4, 0, 1, 0, 0, 0, 0, 0, 2, 0, 1, 0, 0, 0, 0, 0, 4, 0, 2, 0, 0};",
"source node": 29,
"start line": 560,
"target node": 30,
"thread": 0
},
{
"file": 10,
"source": "static char path_wrap_a[24U] = #line 566 { 0, 0, 0, 4, 0, 1, 0, 3, 0, 0, 0, 2, 0, 1, 0, 3, 0, 0, 0, 4, 0, 2, 0, 0};",
"source node": 30,
"start line": 566,
"target node": 31,
"thread": 0
},
{
"file": 10,
"source": "static char path_wrap_b[24U] = #line 572 { 0, 0, 0, 4, 0, 2, 0, 3, 0, 0, 0, 2, 0, 1, 0, 3, 0, 0, 0, 4, 0, 1, 0, 0};",
"source node": 31,
"start line": 572,
"target node": 32,
"thread": 0
},
{
"file": 10,
"source": "static char path_thru[24U] = #line 578 { 0, 0, 0, 4, 0, 1, 0, 3, 0, 0, 0, 2, 0, 1, 0, 3, 0, 0, 0, 4, 0, 2, 0, 3};",
"source node": 32,
"start line": 578,
"target node": 33,
"thread": 0
},
{
"file": 10,
"source": "static char path_wrap_s[16U] = #line 584 { 0, 0, 0, 4, 0, 1, 0, 3, 0, 0, 0, 2, 0, 1, 0, 3};",
"source node": 33,
"start line": 584,
"target node": 34,
"thread": 0
},
{
"file": 10,
"source": "static char path_iso_s[16U] = #line 589 { 0, 0, 0, 4, 0, 1, 0, 0, 0, 0, 0, 2, 0, 1, 0, 0};",
"source node": 34,
"start line": 589,
"target node": 35,
"thread": 0
},
{
"file": 11,
"source": "static u_char const plcs_control_c_u[17U] = #line 136 \"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/pcmplc.c\" { 'P', 'L', 'C', '_', 'C', 'N', 'T', 'R', 'L', '_', 'C', '_', 'U', '=', '\\000'};",
"source node": 35,
"start line": 136,
"target node": 36,
"thread": 0
},
{
"file": 11,
"source": "static u_char const plcs_control_c_s[17U] = #line 137 { 'P', 'L', 'C', '_', 'C', 'N', 'T', 'R', 'L', '_', 'C', '_', 'S', '=', '\\001', '\\002', '\\000'};",
"source node": 36,
"start line": 137,
"target node": 37,
"thread": 0
},
{
"file": 11,
"source": "static struct plt const pltm[8U] = #line 170 { {6, 65048}, {7, 65244}, {8, 65296}, {9, 55771}, {11, 63094}, {12, 65389}, {13, 61473}, {0, 0}};",
"source node": 37,
"start line": 170,
"target node": 38,
"thread": 0
},
{
"file": 11,
"source": "static int const plc_imsk_na = 636;",
"source node": 38,
"start line": 189,
"target node": 39,
"thread": 0
},
{
"file": 11,
"source": "static int const plc_imsk_act = 636;",
"source node": 39,
"start line": 198,
"target node": 40,
"thread": 0
},
{
"file": 12,
"source": "static struct s_p_tab const p_tab[142U] = #line 76 { {4106U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {4107U, 1U, 58U, {'8', '\\000'}}, {4109U, 1U, 66U, {'S', '\\000'}}, {4110U, 1U, 68U, {'S', '\\000'}}, {4111U, 1U, 70U, {'S', '\\000'}}, {4112U, 1U, 72U, {'D', '\\000'}}, {4113U, 2U, 104U, {'D', '\\000'}}, {4114U, 1U, 136U, {'S', '\\000'}}, {4116U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {4117U, 1U, 138U, {'B', '\\000'}}, {4118U, 1U, 139U, {'B', '\\000'}}, {4119U, 1U, 140U, {'B', '\\000'}}, {4120U, 1U, 141U, {'B', '\\000'}}, {4121U, 1U, 142U, {'S', '\\000'}}, {4122U, 2U, 144U, {'w', 'S', '\\000'}}, {4123U, 2U, 146U, {'w', 'S', '\\000'}}, {4125U, 2U, 148U, {'w', 'S', '\\000'}}, {4126U, 2U, 150U, {'b', 'B', '\\000'}}, {4127U, 2U, 152U, {'l', 'L', '\\000'}}, {4128U, 1U, 160U, {'I', 'I', '\\000'}}, {4129U, 1U, 164U, {'I', '\\000'}}, {4130U, 1U, 166U, {'F', '\\000'}}, {4136U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {4137U, 1U, 168U, {'E', '\\000'}}, {4138U, 1U, 170U, {'E', '\\000'}}, {4140U, 1U, 174U, {'F', '\\000'}}, {4141U, 1U, 172U, {'E', '\\000'}}, {4142U, 1U, 175U, {'F', '\\000'}}, {4146U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {4147U, 1U, 176U, {'P', '\\000'}}, {4148U, 1U, 184U, {'P', '\\000'}}, {4149U, 1U, 192U, {'4', 'P', '\\000'}}, {4150U, 1U, 208U, {'8', '\\000'}}, {4156U, 4U, 0U, {'w', 'S', '\\000'}}, {4336U, 2U, 0U, {'8', '\\000'}}, {4337U, 2U, 8U, {'8', '\\000'}}, {4338U, 2U, 16U, {'l', 'L', '\\000'}}, {4339U, 2U, 24U, {'l', 'L', '\\000'}}, {4340U, 2U, 32U, {'l', 'L', '\\000'}}, {4341U, 2U, 40U, {'l', 'L', '\\000'}}, {4342U, 2U, 48U, {'l', 'L', '\\000'}}, {4343U, 2U, 56U, {'w', 'S', '\\000'}}, {8202U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {8203U, 1U, 0U, {'S', '\\000'}}, {8205U, 1U, 8U, {'T', '\\000'}}, {8206U, 1U, 16U, {'T', '\\000'}}, {8212U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {8214U, 1U, 27U, {'B', '\\000'}}, {8215U, 1U, 28U, {'S', '\\000'}}, {8216U, 1U, 30U, {'A', '\\000'}}, {8217U, 1U, 36U, {'A', '\\000'}}, {8218U, 1U, 42U, {'A', '\\000'}}, {8219U, 1U, 48U, {'A', '\\000'}}, {8221U, 1U, 54U, {'E', '\\000'}}, {8224U, 2U, 56U, {'w', 'S', '\\000'}}, {8225U, 1U, 58U, {'E', '\\000'}}, {8226U, 1U, 60U, {'S', '\\000'}}, {8232U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {8233U, 1U, 62U, {'A', '\\000'}}, {8242U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {8243U, 1U, 88U, {'T', '\\000'}}, {8244U, 1U, 96U, {'T', '\\000'}}, {8245U, 1U, 112U, {'T', '\\000'}}, {8246U, 1U, 128U, {'T', '\\000'}}, {8248U, 1U, 136U, {'T', '\\000'}}, {8249U, 1U, 144U, {'T', '\\000'}}, {8250U, 1U, 152U, {'T', '\\000'}}, {8251U, 1U, 160U, {'T', '\\000'}}, {8252U, 1U, 168U, {'T', '\\000'}}, {8253U, 1U, 176U, {'T', '\\000'}}, {8254U, 1U, 184U, {'T', '\\000'}}, {8262U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {8263U, 1U, 192U, {'C', '\\000'}}, {8264U, 1U, 200U, {'C', '\\000'}}, {8265U, 1U, 208U, {'C', '\\000'}}, {8266U, 1U, 216U, {'C', '\\000'}}, {8273U, 1U, 224U, {'C', '\\000'}}, {8274U, 1U, 232U, {'C', '\\000'}}, {8275U, 1U, 240U, {'C', '\\000'}}, {8276U, 1U, 248U, {'C', '\\000'}}, {8278U, 1U, 256U, {'C', '\\000'}}, {8282U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {8287U, 2U, 320U, {'w', 'S', '\\000'}}, {8288U, 1U, 322U, {'S', '\\000'}}, {8292U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {8295U, 2U, 324U, {'w', 'S', '\\000'}}, {8297U, 1U, 326U, {'S', '\\000'}}, {8302U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {8303U, 1U, 328U, {'S', '\\000'}}, {8304U, 1U, 330U, {'F', '\\000'}}, {8305U, 1U, 331U, {'F', '\\000'}}, {8306U, 1U, 332U, {'F', '\\000'}}, {8307U, 1U, 333U, {'F', '\\000'}}, {8308U, 1U, 334U, {'F', '\\000'}}, {8309U, 1U, 335U, {'F', '\\000'}}, {8310U, 2U, 336U, {'b', 'F', '\\000'}}, {8432U, 8U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {8433U, 2U, 72U, {'l', 'T', '\\000'}}, {12810U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {12811U, 1U, 0U, {'r', '\\000'}}, {12815U, 2U, 8U, {'l', '4', '\\000'}}, {12816U, 2U, 16U, {'l', '4', '\\000'}}, {12818U, 1U, 0U, {'\\000'}}, {12819U, 2U, 24U, {'l', 'T', '\\000'}}, {12820U, 2U, 32U, {'l', 'L', '\\000'}}, {12821U, 2U, 40U, {'l', 'T', '\\000'}}, {12822U, 2U, 48U, {'l', 'T', '\\000'}}, {12823U, 2U, 56U, {'l', 'T', '\\000'}}, {16394U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {16396U, 1U, 0U, {'E', '\\000'}}, {16397U, 1U, 2U, {'E', '\\000'}}, {16398U, 2U, 4U, {'b', 'B', '\\000'}}, {16399U, 1U, 5U, {'2', '\\000'}}, {16400U, 1U, 8U, {'E', '\\000'}}, {16401U, 2U, 10U, {'l', '4', '\\000'}}, {16402U, 1U, 14U, {'S', '\\000'}}, {16403U, 1U, 16U, {'B', '\\000'}}, {16406U, 1U, 18U, {'E', '\\000'}}, {16407U, 1U, 17U, {'B', '\\000'}}, {16413U, 1U, 20U, {'R', '\\000'}}, {16414U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {16415U, 2U, 22U, {'w', 'E', '\\000'}}, {16417U, 1U, 26U, {'F', '\\000'}}, {16418U, 1U, 24U, {'E', '\\000'}}, {16424U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {16425U, 1U, 40U, {'C', '\\000'}}, {16426U, 1U, 32U, {'C', '\\000'}}, {16434U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {16435U, 1U, 72U, {'F', '\\000'}}, {16436U, 1U, 56U, {'C', '\\000'}}, {16437U, 1U, 64U, {'C', '\\000'}}, {16442U, 2U, 73U, {'b', 'B', '\\000'}}, {16443U, 2U, 74U, {'b', 'B', '\\000'}}, {16444U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {16445U, 1U, 76U, {'E', '\\000'}}, {16446U, 1U, 80U, {'E', '\\000'}}, {16447U, 1U, 82U, {'E', '\\000'}}, {16448U, 1U, 85U, {'F', '\\000'}}, {16449U, 1U, 84U, {'F', '\\000'}}, {16454U, 4U, 0U, {'w', 'S', '\\000'}}, {0U, 16U, (unsigned short)0, {(char)0, (char)0, (char)0}}, {0U, (unsigned char)0, (unsigned short)0, {(char)0, (char)0, (char)0}}};",
"source node": 40,
"start line": 76,
"target node": 41,
"thread": 0
},
{
"file": 13,
"source": "static char const man_data[32U] = #line 160 { 'x', 'x', 'x', 'S', 'K', '-', 'N', 'E', 'T', ' ', 'F', 'D', 'D', 'I', ' ', 'S', 'M', 'T', ' ', '7', '.', '3', ' ', '-', ' ', 'V', '2', '.', '8', '.', '8', '\\000'};",
"source node": 41,
"start line": 160,
"target node": 42,
"thread": 0
},
{
"file": 14,
"source": "u_char const oem_id[13U];",
"source node": 42,
"start line": 39,
"target node": 43,
"thread": 0
},
{
"file": 15,
"source": "static struct evc_init const evc_inits[10U] = #line 55 { {5U, 0U, 1U, 4168U}, {8U, 1U, 1U, 8332U}, {7U, 1U, 1U, 8333U}, {9U, 1U, 1U, 8334U}, {2U, 1U, 1U, 8335U}, {1U, 1U, 1U, 8336U}, {11U, 1U, 2U, 16464U}, {10U, 1U, 2U, 16466U}, {4U, 1U, 2U, 16465U}, {3U, 1U, 2U, 16467U}};",
"source node": 43,
"start line": 55,
"target node": 44,
"thread": 0
},
{
"file": 16,
"source": "u_char const oem_id[13U] = #line 62 \"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/drvfbi.c\" { 'x', 'P', 'O', 'S', '_', 'I', 'D', ':', 'x', 'x', 'x', 'x', '\\000'};",
"source node": 44,
"start line": 62,
"target node": 45,
"thread": 0
},
{
"file": 17,
"source": "static u_short const plist_raf_alc_res[8U] = #line 60 \"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/ess.c\" { 18U, 12811U, 12815U, 12816U, 25U, 26U, 29U, 0U};",
"source node": 45,
"start line": 60,
"target node": 46,
"thread": 0
},
{
"file": 17,
"source": "static u_short const plist_raf_chg_req[5U] = { 12811U, 12815U, 12816U, 26U, 0U};",
"source node": 46,
"start line": 64,
"target node": 47,
"thread": 0
},
{
"file": 17,
"source": "static struct fddi_addr const smt_sba_da = {{128U, 1U, 67U, 0U, 128U, 12U}};",
"source node": 47,
"start line": 67,
"target node": 48,
"thread": 0
},
{
"file": 17,
"source": "static struct fddi_addr const null_addr___0 = {{0U, 0U, 0U, 0U, 0U, 0U}};",
"source node": 48,
"start line": 68,
"target node": 49,
"thread": 0
},
{
"assumption": "ldv_dma_calls == 0;",
"file": 18,
"source": "int ldv_dma_calls = 0;",
"source node": 49,
"start line": 21,
"target node": 50,
"thread": 0
},
{
"enter": 93,
"file": 0,
"line": 960,
"source": "Begin program execution",
"source node": 50,
"target node": 51,
"thread": 1
},
{
"enter": 0,
"file": 0,
"source": "ldv_main_13((void *)0);",
"source node": 51,
"start line": 962,
"target node": 52,
"thread": 13
},
{
"action": 0,
"file": 0,
"source": "ldv_initialize();",
"source node": 52,
"start line": 541,
"target node": 53,
"thread": 13
},
{
"action": 1,
"enter": 1,
"file": 0,
"source": "ldv_dispatch_insmod_register_13_3();",
"source node": 53,
"start line": 545,
"target node": 54,
"thread": 13
},
{
"file": 0,
"source": "struct ldv_struct_main_13 *cf_arg_5;",
"source node": 54,
"start line": 139,
"target node": 55,
"thread": 13
},
{
"enter": 2,
"file": 0,
"source": "cf_arg_5 = (struct ldv_struct_main_13 *)ldv_xmalloc(4UL);",
"source node": 55,
"start line": 139,
"target node": 56,
"thread": 13
},
{
"file": 19,
"source": "void *res;",
"source node": 56,
"start line": 68,
"target node": 57,
"thread": 13
},
{
"file": 19,
"source": "res = malloc(size);",
"source node": 57,
"start line": 68,
"target node": 58,
"thread": 13
},
{
"condition": true,
"file": 19,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 58,
"start line": 69,
"target node": 59,
"thread": 13
},
{
"condition": true,
"enter": 3,
"file": 19,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 59,
"start line": 70,
"target node": 60,
"thread": 13
},
{
"file": 20,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 60,
"start line": 22,
"target node": 61,
"thread": 13
},
{
"file": 19,
"return": 2,
"source": "return res;",
"source node": 61,
"start line": 71,
"target node": 62,
"thread": 13
},
{
"enter": 4,
"file": 0,
"source": "ldv_insmod_5((void *)cf_arg_5);",
"source node": 62,
"start line": 140,
"target node": 63,
"thread": 5
},
{
"action": 2,
"file": 0,
"source": "int ldv_5_ret_default;",
"source node": 63,
"start line": 402,
"target node": 64,
"thread": 5
},
{
"action": 2,
"file": 0,
"source": "void (*ldv_5_skfddi_pci_driver_exit_default)(void);",
"source node": 64,
"start line": 403,
"target node": 65,
"thread": 5
},
{
"action": 2,
"file": 0,
"source": "int (*ldv_5_skfddi_pci_driver_init_default)(void);",
"source node": 65,
"start line": 404,
"target node": 66,
"thread": 5
},
{
"action": 3,
"enter": 5,
"file": 0,
"source": "ldv_free(arg0);",
"source node": 66,
"start line": 408,
"target node": 67,
"thread": 5
},
{
"file": 19,
"source": "free(s);",
"source node": 67,
"start line": 63,
"target node": 68,
"thread": 5
},
{
"file": 19,
"return": 5,
"source": "return;",
"source node": 68,
"start line": 64,
"target node": 69,
"thread": 5
},
{
"action": 4,
"enter": 7,
"file": 5,
"original file": 0,
"original start line": 413,
"source": "ldv_5_ret_default = skfddi_pci_driver_init();",
"source node": 69,
"start line": 2248,
"target node": 70,
"thread": 5
},
{
"enter": 9,
"file": 5,
"source": "ldv_emg___pci_register_driver(&skfddi_pci_driver, &__this_module, \"skfp\");",
"source node": 70,
"start line": 2248,
"target node": 71,
"thread": 5
},
{
"action": 2,
"file": 0,
"source": "struct pci_driver *ldv_12_pci_driver_pci_driver;",
"source node": 71,
"start line": 185,
"target node": 72,
"thread": 5
},
{
"action": 5,
"file": 0,
"source": "ldv_12_pci_driver_pci_driver = arg0;",
"source node": 72,
"start line": 191,
"target node": 73,
"thread": 5
},
{
"action": 6,
"enter": 11,
"file": 0,
"source": "ldv_dispatch_register_12_3(ldv_12_pci_driver_pci_driver);",
"source node": 73,
"start line": 195,
"target node": 74,
"thread": 5
},
{
"file": 0,
"source": "struct ldv_struct_pci_scenario_4 *cf_arg_4;",
"source node": 74,
"start line": 166,
"target node": 75,
"thread": 5
},
{
"enter": 2,
"file": 0,
"source": "cf_arg_4 = (struct ldv_struct_pci_scenario_4 *)ldv_xmalloc(16UL);",
"source node": 75,
"start line": 166,
"target node": 76,
"thread": 5
},
{
"file": 19,
"source": "void *res;",
"source node": 76,
"start line": 68,
"target node": 77,
"thread": 5
},
{
"file": 19,
"source": "res = malloc(size);",
"source node": 77,
"start line": 68,
"target node": 78,
"thread": 5
},
{
"condition": true,
"file": 19,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 78,
"start line": 69,
"target node": 79,
"thread": 5
},
{
"condition": true,
"enter": 3,
"file": 19,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 79,
"start line": 70,
"target node": 80,
"thread": 5
},
{
"file": 20,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 80,
"start line": 22,
"target node": 81,
"thread": 5
},
{
"file": 19,
"return": 2,
"source": "return res;",
"source node": 81,
"start line": 71,
"target node": 82,
"thread": 5
},
{
"file": 0,
"source": "cf_arg_4->arg0 = arg0;",
"source node": 82,
"start line": 167,
"target node": 83,
"thread": 5
},
{
"enter": 12,
"file": 0,
"source": "ldv_pci_scenario_4((void *)cf_arg_4);",
"source node": 83,
"start line": 168,
"target node": 84,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "struct pci_driver *ldv_4_container_pci_driver;",
"source node": 84,
"start line": 567,
"target node": 85,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "struct pci_device_id *ldv_4_ldv_param_17_1_default;",
"source node": 85,
"start line": 568,
"target node": 86,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "struct pci_dev *ldv_4_resource_dev;",
"source node": 86,
"start line": 569,
"target node": 87,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "pm_message_t ldv_4_resource_pm_message;",
"source node": 87,
"start line": 570,
"target node": 88,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "int ldv_4_ret_default;",
"source node": 88,
"start line": 571,
"target node": 89,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "struct ldv_struct_pci_scenario_4 *data;",
"source node": 89,
"start line": 572,
"target node": 90,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "data = (struct ldv_struct_pci_scenario_4 *)arg0;",
"source node": 90,
"start line": 574,
"target node": 91,
"thread": 4
},
{
"action": 7,
"condition": true,
"file": 0,
"source": "((unsigned long)data) != ((unsigned long)((struct ldv_struct_pci_scenario_4 *)0))",
"source node": 91,
"start line": 581,
"target node": 92,
"thread": 4
},
{
"action": 7,
"file": 0,
"source": "ldv_4_container_pci_driver = data->arg0;",
"source node": 92,
"start line": 582,
"target node": 93,
"thread": 4
},
{
"action": 7,
"enter": 5,
"file": 0,
"source": "ldv_free((void *)data);",
"source node": 93,
"start line": 583,
"target node": 94,
"thread": 4
},
{
"file": 19,
"source": "free(s);",
"source node": 94,
"start line": 63,
"target node": 95,
"thread": 4
},
{
"file": 19,
"return": 5,
"source": "return;",
"source node": 95,
"start line": 64,
"target node": 96,
"thread": 4
},
{
"action": 8,
"enter": 2,
"file": 0,
"source": "ldv_4_resource_dev = (struct pci_dev *)ldv_xmalloc(2936UL);",
"source node": 96,
"start line": 588,
"target node": 97,
"thread": 4
},
{
"file": 19,
"source": "void *res;",
"source node": 97,
"start line": 68,
"target node": 98,
"thread": 4
},
{
"file": 19,
"source": "res = malloc(size);",
"source node": 98,
"start line": 68,
"target node": 99,
"thread": 4
},
{
"condition": true,
"file": 19,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 99,
"start line": 69,
"target node": 100,
"thread": 4
},
{
"condition": true,
"enter": 3,
"file": 19,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 100,
"start line": 70,
"target node": 101,
"thread": 4
},
{
"file": 20,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 101,
"start line": 22,
"target node": 102,
"thread": 4
},
{
"file": 19,
"return": 2,
"source": "return res;",
"source node": 102,
"start line": 71,
"target node": 103,
"thread": 4
},
{
"action": 9,
"enter": 13,
"file": 0,
"source": "ldv_4_ldv_param_17_1_default = (struct pci_device_id *)ldv_xmalloc_unknown_size(0UL);",
"source node": 103,
"start line": 605,
"target node": 104,
"thread": 4
},
{
"file": 19,
"source": "void *res;",
"source node": 104,
"start line": 116,
"target node": 105,
"thread": 4
},
{
"file": 19,
"source": "res = external_allocated_data();",
"source node": 105,
"start line": 116,
"target node": 106,
"thread": 4
},
{
"condition": true,
"file": 19,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 106,
"start line": 117,
"target node": 107,
"thread": 4
},
{
"condition": true,
"enter": 3,
"file": 19,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 107,
"start line": 118,
"target node": 108,
"thread": 4
},
{
"file": 20,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 108,
"start line": 22,
"target node": 109,
"thread": 4
},
{
"file": 19,
"return": 13,
"source": "return res;",
"source node": 109,
"start line": 119,
"target node": 110,
"thread": 4
},
{
"action": 10,
"file": 0,
"source": "ldv_pre_probe();",
"source node": 110,
"start line": 610,
"target node": 111,
"thread": 4
},
{
"action": 10,
"enter": 15,
"file": 5,
"original file": 0,
"original start line": 612,
"source": "ldv_4_ret_default = skfp_init_one(ldv_4_resource_dev, ldv_4_ldv_param_17_1_default);",
"source node": 111,
"start line": 206,
"target node": 112,
"thread": 4
},
{
"file": 5,
"source": "struct net_device *dev;",
"source node": 112,
"start line": 206,
"target node": 113,
"thread": 4
},
{
"file": 5,
"source": "struct s_smc *smc;",
"source node": 113,
"start line": 207,
"target node": 114,
"thread": 4
},
{
"file": 5,
"source": "void *mem;",
"source node": 114,
"start line": 208,
"target node": 115,
"thread": 4
},
{
"file": 5,
"source": "int err;",
"source node": 115,
"start line": 209,
"target node": 116,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor;",
"source node": 116,
"start line": 210,
"target node": 117,
"thread": 4
},
{
"file": 5,
"source": "descriptor.modname = \"skfp\";",
"source node": 117,
"start line": 212,
"target node": 118,
"thread": 4
},
{
"file": 5,
"source": "descriptor.function = \"skfp_init_one\";",
"source node": 118,
"start line": 212,
"target node": 119,
"thread": 4
},
{
"file": 5,
"source": "descriptor.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 119,
"start line": 212,
"target node": 120,
"thread": 4
},
{
"file": 5,
"source": "descriptor.format = \"entering skfp_init_one\\n\";",
"source node": 120,
"start line": 212,
"target node": 121,
"thread": 4
},
{
"file": 5,
"source": "descriptor.lineno = 212U;",
"source node": 121,
"start line": 212,
"target node": 122,
"thread": 4
},
{
"file": 5,
"source": "descriptor.flags = 0U;",
"source node": 122,
"start line": 212,
"target node": 123,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor.flags &1L, 0L) != 0L",
"source node": 123,
"start line": 212,
"target node": 124,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 124,
"start line": 26,
"target node": 125,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor, \"entering skfp_init_one\\n\");",
"source node": 125,
"start line": 212,
"target node": 126,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "num_boards == 0",
"source node": 126,
"start line": 214,
"target node": 127,
"thread": 4
},
{
"file": 5,
"source": "printk(\"%s\\n\", boot_msg);",
"source node": 127,
"start line": 215,
"target node": 128,
"thread": 4
},
{
"file": 5,
"source": "err = pci_enable_device(pdev);",
"source node": 128,
"start line": 217,
"target node": 129,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "err == 0",
"source node": 129,
"start line": 218,
"target node": 130,
"thread": 4
},
{
"file": 5,
"source": "err = pci_request_regions(pdev, \"skfddi\");",
"source node": 130,
"start line": 221,
"target node": 131,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "err == 0",
"source node": 131,
"start line": 222,
"target node": 132,
"thread": 4
},
{
"file": 5,
"source": "pci_set_master(pdev);",
"source node": 132,
"start line": 225,
"target node": 133,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "((((pdev->resource)[0]).flags) &512UL) != 0UL",
"source node": 133,
"start line": 228,
"target node": 134,
"thread": 4
},
{
"enter": 17,
"file": 5,
"source": "mem = ioremap(pdev->resource[0].start, 16384UL);",
"source node": 134,
"start line": 234,
"target node": 135,
"thread": 4
},
{
"file": 23,
"return": 17,
"source": "return ioremap_nocache(offset, size);",
"source node": 135,
"start line": 184,
"target node": 136,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "((unsigned long)mem) != ((unsigned long)((void *)0))",
"source node": 136,
"start line": 244,
"target node": 137,
"thread": 4
},
{
"file": 5,
"source": "dev = alloc_fddidev(8048);",
"source node": 137,
"start line": 251,
"target node": 138,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "((unsigned long)dev) != ((unsigned long)((struct net_device *)0))",
"source node": 138,
"start line": 252,
"target node": 139,
"thread": 4
},
{
"file": 5,
"source": "dev->irq = (int)pdev->irq;",
"source node": 139,
"start line": 259,
"target node": 140,
"thread": 4
},
{
"file": 5,
"source": "dev->netdev_ops = &skfp_netdev_ops;",
"source node": 140,
"start line": 260,
"target node": 141,
"thread": 4
},
{
"file": 5,
"source": "dev->dev.parent = &pdev->dev;",
"source node": 141,
"start line": 262,
"target node": 142,
"thread": 4
},
{
"enter": 18,
"file": 5,
"source": "smc = (struct s_smc *)netdev_priv((struct net_device const *)dev);",
"source node": 142,
"start line": 265,
"target node": 143,
"thread": 4
},
{
"file": 24,
"return": 18,
"source": "return (void *)((char *)dev + 3200UL);",
"source node": 143,
"start line": 1605,
"target node": 144,
"thread": 4
},
{
"file": 5,
"source": "smc->os.dev = dev;",
"source node": 144,
"start line": 266,
"target node": 145,
"thread": 4
},
{
"file": 5,
"source": "smc->os.bus_type = 0U;",
"source node": 145,
"start line": 267,
"target node": 146,
"thread": 4
},
{
"file": 5,
"source": "smc->os.pdev = *pdev;",
"source node": 146,
"start line": 268,
"target node": 147,
"thread": 4
},
{
"file": 5,
"source": "smc->os.QueueSkb = 20UL;",
"source node": 147,
"start line": 269,
"target node": 148,
"thread": 4
},
{
"file": 5,
"source": "smc->os.MaxFrameSize = 4550UL;",
"source node": 148,
"start line": 270,
"target node": 149,
"thread": 4
},
{
"file": 5,
"source": "smc->os.dev = dev;",
"source node": 149,
"start line": 271,
"target node": 150,
"thread": 4
},
{
"file": 5,
"source": "smc->hw.slot = -1;",
"source node": 150,
"start line": 272,
"target node": 151,
"thread": 4
},
{
"file": 5,
"source": "smc->hw.iop = mem;",
"source node": 151,
"start line": 273,
"target node": 152,
"thread": 4
},
{
"file": 5,
"source": "smc->os.ResetRequested = 0U;",
"source node": 152,
"start line": 274,
"target node": 153,
"thread": 4
},
{
"enter": 19,
"file": 5,
"source": "skb_queue_head_init(&smc->os.SendSkbQueue);",
"source node": 153,
"start line": 275,
"target node": 154,
"thread": 4
},
{
"file": 25,
"source": "struct lock_class_key __key;",
"source node": 154,
"start line": 1149,
"target node": 155,
"thread": 4
},
{
"enter": 20,
"file": 25,
"source": "spinlock_check(&list->lock);",
"source node": 155,
"start line": 1149,
"target node": 156,
"thread": 4
},
{
"file": 26,
"return": 20,
"source": "return &lock->__annonCompField19.rlock;",
"source node": 156,
"start line": 292,
"target node": 157,
"thread": 4
},
{
"file": 25,
"source": "__raw_spin_lock_init(&list->lock.__annonCompField19.rlock, \"&(&list->lock)->rlock\", &__key);",
"source node": 157,
"start line": 1149,
"target node": 158,
"thread": 4
},
{
"enter": 21,
"file": 25,
"source": "__skb_queue_head_init(list);",
"source node": 158,
"start line": 1150,
"target node": 159,
"thread": 4
},
{
"file": 25,
"source": "list->next = (struct sk_buff *)list;",
"source node": 159,
"start line": 1135,
"target node": 160,
"thread": 4
},
{
"file": 25,
"source": "list->prev = tmp;",
"source node": 160,
"start line": 1135,
"target node": 161,
"thread": 4
},
{
"file": 25,
"source": "list->qlen = 0U;",
"source node": 161,
"start line": 1136,
"target node": 162,
"thread": 4
},
{
"file": 25,
"return": 21,
"source": "return;",
"source node": 162,
"start line": 1137,
"target node": 163,
"thread": 4
},
{
"file": 25,
"return": 19,
"source": "return;",
"source node": 163,
"start line": 1151,
"target node": 164,
"thread": 4
},
{
"file": 5,
"source": "dev->base_addr = (unsigned long)mem;",
"source node": 164,
"start line": 277,
"target node": 165,
"thread": 4
},
{
"enter": 22,
"file": 5,
"source": "err = skfp_driver_init(dev);",
"source node": 165,
"start line": 279,
"target node": 166,
"thread": 4
},
{
"file": 5,
"source": "struct s_smc *smc;",
"source node": 166,
"start line": 383,
"target node": 167,
"thread": 4
},
{
"file": 5,
"source": "skfddi_priv *bp;",
"source node": 167,
"start line": 385,
"target node": 168,
"thread": 4
},
{
"file": 5,
"source": "int err;",
"source node": 168,
"start line": 386,
"target node": 169,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor;",
"source node": 169,
"start line": 387,
"target node": 170,
"thread": 4
},
{
"file": 5,
"source": "struct lock_class_key __key;",
"source node": 170,
"start line": 389,
"target node": 171,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___0;",
"source node": 171,
"start line": 392,
"target node": 172,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___1;",
"source node": 172,
"start line": 394,
"target node": 173,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___2;",
"source node": 173,
"start line": 396,
"target node": 174,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___3;",
"source node": 174,
"start line": 399,
"target node": 175,
"thread": 4
},
{
"enter": 18,
"file": 5,
"source": "smc = (struct s_smc *)netdev_priv((struct net_device const *)dev);",
"source node": 175,
"start line": 383,
"target node": 176,
"thread": 4
},
{
"file": 24,
"return": 18,
"source": "return (void *)((char *)dev + 3200UL);",
"source node": 176,
"start line": 1605,
"target node": 177,
"thread": 4
},
{
"file": 5,
"source": "bp = &smc->os;",
"source node": 177,
"start line": 384,
"target node": 178,
"thread": 4
},
{
"file": 5,
"source": "err = -5;",
"source node": 178,
"start line": 385,
"target node": 179,
"thread": 4
},
{
"file": 5,
"source": "descriptor.modname = \"skfp\";",
"source node": 179,
"start line": 387,
"target node": 180,
"thread": 4
},
{
"file": 5,
"source": "descriptor.function = \"skfp_driver_init\";",
"source node": 180,
"start line": 387,
"target node": 181,
"thread": 4
},
{
"file": 5,
"source": "descriptor.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 181,
"start line": 387,
"target node": 182,
"thread": 4
},
{
"file": 5,
"source": "descriptor.format = \"entering skfp_driver_init\\n\";",
"source node": 182,
"start line": 387,
"target node": 183,
"thread": 4
},
{
"file": 5,
"source": "descriptor.lineno = 387U;",
"source node": 183,
"start line": 387,
"target node": 184,
"thread": 4
},
{
"file": 5,
"source": "descriptor.flags = 0U;",
"source node": 184,
"start line": 387,
"target node": 185,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor.flags &1L, 0L) != 0L",
"source node": 185,
"start line": 387,
"target node": 186,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 186,
"start line": 26,
"target node": 187,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor, \"entering skfp_driver_init\\n\");",
"source node": 187,
"start line": 387,
"target node": 188,
"thread": 4
},
{
"file": 5,
"source": "bp->base_addr = dev->base_addr;",
"source node": 188,
"start line": 390,
"target node": 189,
"thread": 4
},
{
"file": 5,
"source": "smc->hw.irq = (short)dev->irq;",
"source node": 189,
"start line": 393,
"target node": 190,
"thread": 4
},
{
"enter": 20,
"file": 5,
"source": "spinlock_check(&bp->DriverLock);",
"source node": 190,
"start line": 395,
"target node": 191,
"thread": 4
},
{
"file": 26,
"return": 20,
"source": "return &lock->__annonCompField19.rlock;",
"source node": 191,
"start line": 292,
"target node": 192,
"thread": 4
},
{
"file": 5,
"source": "__raw_spin_lock_init(&bp->DriverLock.__annonCompField19.rlock, \"&(&bp->DriverLock)->rlock\", &__key);",
"source node": 192,
"start line": 395,
"target node": 193,
"thread": 4
},
{
"enter": 23,
"file": 5,
"source": "bp->LocalRxBuffer = (unsigned char *)pci_alloc_consistent(&bp->pdev, 4550UL, &bp->LocalRxBufferDMA);",
"source node": 193,
"start line": 398,
"target node": 194,
"thread": 4
},
{
"condition": true,
"file": 27,
"source": "((unsigned long)hwdev) == ((unsigned long)((struct pci_dev *)0))",
"source node": 194,
"start line": 19,
"target node": 195,
"thread": 4
},
{
"file": 27,
"source": "(struct device *)0",
"source node": 195,
"start line": 19,
"target node": 196,
"thread": 4
},
{
"enter": 24,
"file": 27,
"return": 23,
"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": 196,
"start line": 19,
"target node": 197,
"thread": 4
},
{
"assumption": "dev == 0LL; ((signed long long int)(&(dev->kobj))) == 16LL; ((signed long long int)(&(dev->kobj.entry))) == 24LL; (dev->kobj.sd) == 0LL; ((signed long long int)(&(dev->kobj.sd->count))) == 0LL; ((signed long long int)(&(dev->kobj.sd->active))) == 4LL; ((signed long long int)(&(dev->kobj.sd->dep_map))) == 8LL; (&(dev->kobj.sd->dep_map.class_cache)) == 16LL; (dev->kobj.sd->name) == 0LL; ((signed long long int)(&(dev->kobj.sd->rb))) == 72LL; ((signed long long int)(&(dev->kobj.sd->u))) == 96LL; ((signed long long int)(&(dev->kobj.sd->__annonCompField21))) == 116LL; ((signed long long int)(&(dev->kobj.kref))) == 72LL; ((signed long long int)(&(dev->kobj.kref.refcount))) == 72LL; ((signed long long int)(&(dev->kobj.release))) == 76LL; ((signed long long int)(&(dev->kobj.release.work))) == 76LL; ((signed long long int)(&(dev->kobj.release.work.data))) == 76LL; ((signed long long int)(&(dev->kobj.release.work.entry))) == 84LL; ((signed long long int)(&(dev->kobj.release.work.lockdep_map))) == 108LL; (&(dev->kobj.release.work.lockdep_map.class_cache)) == 116LL; ((signed long long int)(&(dev->kobj.release.timer))) == 156LL; ((signed long long int)(&(dev->kobj.release.timer.entry))) == 156LL; (&(dev->kobj.release.timer.start_comm)) == 220LL; ((signed long long int)(&(dev->kobj.release.timer.lockdep_map))) == 236LL; (&(dev->kobj.release.timer.lockdep_map.class_cache)) == 244LL; (dev->type) == 32LL; (dev->type->release) == 0LL; ((signed long long int)(&(dev->mutex))) == 328LL; ((signed long long int)(&(dev->mutex.count))) == 328LL; ((signed long long int)(&(dev->mutex.wait_lock))) == 332LL; ((signed long long int)(&(dev->mutex.wait_lock.__annonCompField19))) == 332LL; ((signed long long int)(&(dev->mutex.wait_list))) == 404LL; ((signed long long int)(&(dev->mutex.dep_map))) == 444LL; (&(dev->mutex.dep_map.class_cache)) == 452LL; ((signed long long int)(&(dev->power))) == 520LL; ((signed long long int)(&(dev->power.power_state))) == 520LL; ((signed long long int)(&(dev->power.lock))) == 530LL; ((signed long long int)(&(dev->power.lock.__annonCompField19))) == 530LL; ((signed long long int)(&(dev->power.entry))) == 602LL; ((signed long long int)(&(dev->power.completion))) == 618LL; ((signed long long int)(&(dev->power.completion.wait))) == 622LL; ((signed long long int)(&(dev->power.completion.wait.lock))) == 622LL; ((signed long long int)(&(dev->power.completion.wait.lock.__annonCompField19))) == 622LL; ((signed long long int)(&(dev->power.completion.wait.task_list))) == 694LL; ((signed long long int)(&(dev->power.suspend_timer))) == 724LL; ((signed long long int)(&(dev->power.suspend_timer.entry))) == 724LL; (&(dev->power.suspend_timer.start_comm)) == 788LL; ((signed long long int)(&(dev->power.suspend_timer.lockdep_map))) == 804LL; (&(dev->power.suspend_timer.lockdep_map.class_cache)) == 812LL; ((signed long long int)(&(dev->power.work))) == 860LL; ((signed long long int)(&(dev->power.work.data))) == 860LL; ((signed long long int)(&(dev->power.work.entry))) == 868LL; ((signed long long int)(&(dev->power.work.lockdep_map))) == 892LL; (&(dev->power.work.lockdep_map.class_cache)) == 900LL; ((signed long long int)(&(dev->power.wait_queue))) == 940LL; ((signed long long int)(&(dev->power.wait_queue.lock))) == 940LL; ((signed long long int)(&(dev->power.wait_queue.lock.__annonCompField19))) == 940LL; ((signed long long int)(&(dev->power.wait_queue.task_list))) == 1012LL; ((signed long long int)(&(dev->power.usage_count))) == 1028LL; ((signed long long int)(&(dev->power.child_count))) == 1032LL; ((signed long long int)(&(dev->dma_pools))) == 1156LL; ((signed long long int)(&(dev->archdata))) == 1180LL; ((signed long long int)(&(dev->acpi_node))) == 1204LL; ((signed long long int)(&(dev->devres_lock))) == 1220LL; ((signed long long int)(&(dev->devres_lock.__annonCompField19))) == 1220LL; ((signed long long int)(&(dev->devres_head))) == 1292LL; ((signed long long int)(&(dev->knode_class))) == 1308LL; ((signed long long int)(&(dev->knode_class.n_node))) == 1316LL; ((signed long long int)(&(dev->knode_class.n_ref))) == 1332LL; ((signed long long int)(&(dev->knode_class.n_ref.refcount))) == 1332LL; gfp == 32U;",
"assumption scope": 24,
"file": 4,
"source": "struct dma_map_ops *ops;",
"source node": 197,
"start line": 138,
"target node": 198,
"thread": 4
},
{
"file": 4,
"source": "void *memory;",
"source node": 198,
"start line": 140,
"target node": 199,
"thread": 4
},
{
"enter": 25,
"file": 4,
"source": "ops = get_dma_ops(dev);",
"source node": 199,
"start line": 138,
"target node": 200,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 4,
"source": "__builtin_expect((unsigned long)dev == (unsigned long)((struct device *)0), 0L) != 0L",
"source node": 200,
"start line": 37,
"target node": 201,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 201,
"start line": 26,
"target node": 202,
"thread": 4
},
{
"file": 4,
"return": 25,
"source": "return dma_ops;",
"source node": 202,
"start line": 38,
"target node": 203,
"thread": 4
},
{
"assumption": "gfp == 32U;",
"assumption scope": 24,
"file": 4,
"source": "gfp = gfp &4294967288U;",
"source node": 203,
"start line": 141,
"target node": 204,
"thread": 4
},
{
"condition": true,
"file": 4,
"source": "((unsigned long)dev) == ((unsigned long)((struct device *)0))",
"source node": 204,
"start line": 146,
"target node": 205,
"thread": 4
},
{
"file": 4,
"source": "dev = &x86_dma_fallback_dev;",
"source node": 205,
"start line": 147,
"target node": 206,
"thread": 4
},
{
"condition": true,
"enter": 26,
"file": 4,
"source": "is_device_dma_capable(dev) != 0",
"source node": 206,
"start line": 149,
"target node": 207,
"thread": 4
},
{
"condition": true,
"file": 28,
"source": "__CPAchecker_TMP_1 != ((unsigned long)((u64 *)0ULL))",
"source node": 207,
"start line": 72,
"target node": 208,
"thread": 4
},
{
"condition": true,
"file": 28,
"source": "(*(dev->dma_mask)) != 0ULL",
"source node": 208,
"start line": 72,
"target node": 209,
"thread": 4
},
{
"file": 28,
"source": "(unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL",
"source node": 209,
"start line": 72,
"target node": 210,
"thread": 4
},
{
"file": 28,
"return": 26,
"source": "return (unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL;",
"source node": 210,
"start line": 72,
"target node": 211,
"thread": 4
},
{
"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": 211,
"start line": 152,
"target node": 212,
"thread": 4
},
{
"enter": 27,
"file": 4,
"source": "memory = (*(ops->alloc))(dev, size, dma_handle, dma_alloc_coherent_gfp_flags(dev, gfp), attrs);",
"source node": 212,
"start line": 155,
"target node": 213,
"thread": 4
},
{
"assumption": "gfp == 32U;",
"assumption scope": 27,
"file": 4,
"source": "unsigned long dma_mask;",
"source node": 213,
"start line": 121,
"target node": 214,
"thread": 4
},
{
"enter": 28,
"file": 4,
"source": "dma_mask = dma_alloc_coherent_mask(dev, gfp);",
"source node": 214,
"start line": 121,
"target node": 215,
"thread": 4
},
{
"assumption": "gfp == 32U;",
"assumption scope": 28,
"file": 4,
"source": "unsigned long dma_mask;",
"source node": 215,
"start line": 109,
"target node": 216,
"thread": 4
},
{
"assumption": "dma_mask == 0UL;",
"assumption scope": 28,
"file": 4,
"source": "dma_mask = 0UL;",
"source node": 216,
"start line": 110,
"target node": 217,
"thread": 4
},
{
"file": 4,
"source": "dma_mask = (unsigned long)dev->coherent_dma_mask;",
"source node": 217,
"start line": 112,
"target node": 218,
"thread": 4
},
{
"condition": true,
"file": 4,
"source": "dma_mask == 0UL",
"source node": 218,
"start line": 113,
"target node": 219,
"thread": 4
},
{
"condition": true,
"file": 4,
"source": "(((int)gfp) &1) == 0",
"source node": 219,
"start line": 114,
"target node": 220,
"thread": 4
},
{
"file": 4,
"source": "4294967295UL",
"source node": 220,
"start line": 114,
"target node": 221,
"thread": 4
},
{
"assumption": "dma_mask == 4294967295UL;",
"assumption scope": 28,
"file": 4,
"source": "dma_mask = (int)gfp &1 ? 16777215UL : 4294967295UL;",
"source node": 221,
"start line": 114,
"target node": 222,
"thread": 4
},
{
"file": 4,
"return": 28,
"source": "return dma_mask;",
"source node": 222,
"start line": 116,
"target node": 223,
"thread": 4
},
{
"condition": true,
"file": 4,
"source": "((unsigned long long)dma_mask) > 16777215ULL",
"source node": 223,
"start line": 123,
"target node": 224,
"thread": 4
},
{
"condition": true,
"file": 4,
"source": "((unsigned long long)dma_mask) > 4294967295ULL",
"source node": 224,
"start line": 126,
"target node": 225,
"thread": 4
},
{
"file": 4,
"return": 27,
"source": "return gfp;",
"source node": 225,
"start line": 129,
"target node": 226,
"thread": 4
},
{
"file": 4,
"source": "debug_dma_alloc_coherent(dev, size, *dma_handle, memory);",
"source node": 226,
"start line": 157,
"target node": 227,
"thread": 4
},
{
"file": 4,
"return": 24,
"source": "return memory;",
"source node": 227,
"start line": 159,
"target node": 228,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "__CPAchecker_TMP_1 != ((unsigned long)((unsigned char *)0U))",
"source node": 228,
"start line": 399,
"target node": 229,
"thread": 4
},
{
"enter": 29,
"file": 5,
"source": "bp->SharedMemSize = (ulong)mac_drv_check_space();",
"source node": 229,
"start line": 406,
"target node": 230,
"thread": 4
},
{
"file": 29,
"return": 29,
"source": "return 20032U;",
"source node": 230,
"start line": 241,
"target node": 231,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.modname = \"skfp\";",
"source node": 231,
"start line": 407,
"target node": 232,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.function = \"skfp_driver_init\";",
"source node": 232,
"start line": 407,
"target node": 233,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 233,
"start line": 407,
"target node": 234,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.format = \"Memory for HWM: %ld\\n\";",
"source node": 234,
"start line": 407,
"target node": 235,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.lineno = 407U;",
"source node": 235,
"start line": 407,
"target node": 236,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.flags = 0U;",
"source node": 236,
"start line": 407,
"target node": 237,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___0.flags &1L, 0L) != 0L",
"source node": 237,
"start line": 407,
"target node": 238,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 238,
"start line": 26,
"target node": 239,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___0, \"Memory for HWM: %ld\\n\", bp->SharedMemSize);",
"source node": 239,
"start line": 407,
"target node": 240,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "(bp->SharedMemSize) != 0UL",
"source node": 240,
"start line": 408,
"target node": 241,
"thread": 4
},
{
"file": 5,
"source": "bp->SharedMemSize = bp->SharedMemSize + 16UL;",
"source node": 241,
"start line": 409,
"target node": 242,
"thread": 4
},
{
"enter": 23,
"file": 5,
"source": "bp->SharedMemAddr = pci_alloc_consistent(&bp->pdev, bp->SharedMemSize, &bp->SharedMemDMA);",
"source node": 242,
"start line": 411,
"target node": 243,
"thread": 4
},
{
"condition": true,
"file": 27,
"source": "((unsigned long)hwdev) == ((unsigned long)((struct pci_dev *)0))",
"source node": 243,
"start line": 19,
"target node": 244,
"thread": 4
},
{
"file": 27,
"source": "(struct device *)0",
"source node": 244,
"start line": 19,
"target node": 245,
"thread": 4
},
{
"enter": 24,
"file": 27,
"return": 23,
"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": 245,
"start line": 19,
"target node": 246,
"thread": 4
},
{
"assumption": "dev == 0LL; ((signed long long int)(&(dev->kobj))) == 16LL; ((signed long long int)(&(dev->kobj.entry))) == 24LL; (dev->kobj.sd) == 0LL; ((signed long long int)(&(dev->kobj.sd->count))) == 0LL; ((signed long long int)(&(dev->kobj.sd->active))) == 4LL; ((signed long long int)(&(dev->kobj.sd->dep_map))) == 8LL; (&(dev->kobj.sd->dep_map.class_cache)) == 16LL; (dev->kobj.sd->name) == 0LL; ((signed long long int)(&(dev->kobj.sd->rb))) == 72LL; ((signed long long int)(&(dev->kobj.sd->u))) == 96LL; ((signed long long int)(&(dev->kobj.sd->__annonCompField21))) == 116LL; ((signed long long int)(&(dev->kobj.kref))) == 72LL; ((signed long long int)(&(dev->kobj.kref.refcount))) == 72LL; ((signed long long int)(&(dev->kobj.release))) == 76LL; ((signed long long int)(&(dev->kobj.release.work))) == 76LL; ((signed long long int)(&(dev->kobj.release.work.data))) == 76LL; ((signed long long int)(&(dev->kobj.release.work.entry))) == 84LL; ((signed long long int)(&(dev->kobj.release.work.lockdep_map))) == 108LL; (&(dev->kobj.release.work.lockdep_map.class_cache)) == 116LL; ((signed long long int)(&(dev->kobj.release.timer))) == 156LL; ((signed long long int)(&(dev->kobj.release.timer.entry))) == 156LL; (&(dev->kobj.release.timer.start_comm)) == 220LL; ((signed long long int)(&(dev->kobj.release.timer.lockdep_map))) == 236LL; (&(dev->kobj.release.timer.lockdep_map.class_cache)) == 244LL; (dev->type) == 32LL; (dev->type->release) == 0LL; ((signed long long int)(&(dev->mutex))) == 328LL; ((signed long long int)(&(dev->mutex.count))) == 328LL; ((signed long long int)(&(dev->mutex.wait_lock))) == 332LL; ((signed long long int)(&(dev->mutex.wait_lock.__annonCompField19))) == 332LL; ((signed long long int)(&(dev->mutex.wait_list))) == 404LL; ((signed long long int)(&(dev->mutex.dep_map))) == 444LL; (&(dev->mutex.dep_map.class_cache)) == 452LL; ((signed long long int)(&(dev->power))) == 520LL; ((signed long long int)(&(dev->power.power_state))) == 520LL; ((signed long long int)(&(dev->power.lock))) == 530LL; ((signed long long int)(&(dev->power.lock.__annonCompField19))) == 530LL; ((signed long long int)(&(dev->power.entry))) == 602LL; ((signed long long int)(&(dev->power.completion))) == 618LL; ((signed long long int)(&(dev->power.completion.wait))) == 622LL; ((signed long long int)(&(dev->power.completion.wait.lock))) == 622LL; ((signed long long int)(&(dev->power.completion.wait.lock.__annonCompField19))) == 622LL; ((signed long long int)(&(dev->power.completion.wait.task_list))) == 694LL; ((signed long long int)(&(dev->power.suspend_timer))) == 724LL; ((signed long long int)(&(dev->power.suspend_timer.entry))) == 724LL; (&(dev->power.suspend_timer.start_comm)) == 788LL; ((signed long long int)(&(dev->power.suspend_timer.lockdep_map))) == 804LL; (&(dev->power.suspend_timer.lockdep_map.class_cache)) == 812LL; ((signed long long int)(&(dev->power.work))) == 860LL; ((signed long long int)(&(dev->power.work.data))) == 860LL; ((signed long long int)(&(dev->power.work.entry))) == 868LL; ((signed long long int)(&(dev->power.work.lockdep_map))) == 892LL; (&(dev->power.work.lockdep_map.class_cache)) == 900LL; ((signed long long int)(&(dev->power.wait_queue))) == 940LL; ((signed long long int)(&(dev->power.wait_queue.lock))) == 940LL; ((signed long long int)(&(dev->power.wait_queue.lock.__annonCompField19))) == 940LL; ((signed long long int)(&(dev->power.wait_queue.task_list))) == 1012LL; ((signed long long int)(&(dev->power.usage_count))) == 1028LL; ((signed long long int)(&(dev->power.child_count))) == 1032LL; ((signed long long int)(&(dev->dma_pools))) == 1156LL; ((signed long long int)(&(dev->archdata))) == 1180LL; ((signed long long int)(&(dev->acpi_node))) == 1204LL; ((signed long long int)(&(dev->devres_lock))) == 1220LL; ((signed long long int)(&(dev->devres_lock.__annonCompField19))) == 1220LL; ((signed long long int)(&(dev->devres_head))) == 1292LL; ((signed long long int)(&(dev->knode_class))) == 1308LL; ((signed long long int)(&(dev->knode_class.n_node))) == 1316LL; ((signed long long int)(&(dev->knode_class.n_ref))) == 1332LL; ((signed long long int)(&(dev->knode_class.n_ref.refcount))) == 1332LL; gfp == 32U;",
"assumption scope": 24,
"file": 4,
"source": "struct dma_map_ops *ops;",
"source node": 246,
"start line": 138,
"target node": 247,
"thread": 4
},
{
"file": 4,
"source": "void *memory;",
"source node": 247,
"start line": 140,
"target node": 248,
"thread": 4
},
{
"enter": 25,
"file": 4,
"source": "ops = get_dma_ops(dev);",
"source node": 248,
"start line": 138,
"target node": 249,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 4,
"source": "__builtin_expect((unsigned long)dev == (unsigned long)((struct device *)0), 0L) != 0L",
"source node": 249,
"start line": 37,
"target node": 250,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 250,
"start line": 26,
"target node": 251,
"thread": 4
},
{
"file": 4,
"return": 25,
"source": "return dma_ops;",
"source node": 251,
"start line": 38,
"target node": 252,
"thread": 4
},
{
"assumption": "gfp == 32U;",
"assumption scope": 24,
"file": 4,
"source": "gfp = gfp &4294967288U;",
"source node": 252,
"start line": 141,
"target node": 253,
"thread": 4
},
{
"condition": true,
"file": 4,
"source": "((unsigned long)dev) == ((unsigned long)((struct device *)0))",
"source node": 253,
"start line": 146,
"target node": 254,
"thread": 4
},
{
"file": 4,
"source": "dev = &x86_dma_fallback_dev;",
"source node": 254,
"start line": 147,
"target node": 255,
"thread": 4
},
{
"condition": true,
"enter": 26,
"file": 4,
"source": "is_device_dma_capable(dev) != 0",
"source node": 255,
"start line": 149,
"target node": 256,
"thread": 4
},
{
"condition": true,
"file": 28,
"source": "__CPAchecker_TMP_1 != ((unsigned long)((u64 *)0ULL))",
"source node": 256,
"start line": 72,
"target node": 257,
"thread": 4
},
{
"condition": true,
"file": 28,
"source": "(*(dev->dma_mask)) != 0ULL",
"source node": 257,
"start line": 72,
"target node": 258,
"thread": 4
},
{
"file": 28,
"source": "(unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL",
"source node": 258,
"start line": 72,
"target node": 259,
"thread": 4
},
{
"file": 28,
"return": 26,
"source": "return (unsigned long)dev->dma_mask != (unsigned long)((u64 *)0ULL) &&*(dev->dma_mask) != 0ULL;",
"source node": 259,
"start line": 72,
"target node": 260,
"thread": 4
},
{
"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": 260,
"start line": 152,
"target node": 261,
"thread": 4
},
{
"enter": 27,
"file": 4,
"source": "memory = (*(ops->alloc))(dev, size, dma_handle, dma_alloc_coherent_gfp_flags(dev, gfp), attrs);",
"source node": 261,
"start line": 155,
"target node": 262,
"thread": 4
},
{
"assumption": "gfp == 32U;",
"assumption scope": 27,
"file": 4,
"source": "unsigned long dma_mask;",
"source node": 262,
"start line": 121,
"target node": 263,
"thread": 4
},
{
"enter": 28,
"file": 4,
"source": "dma_mask = dma_alloc_coherent_mask(dev, gfp);",
"source node": 263,
"start line": 121,
"target node": 264,
"thread": 4
},
{
"assumption": "gfp == 32U;",
"assumption scope": 28,
"file": 4,
"source": "unsigned long dma_mask;",
"source node": 264,
"start line": 109,
"target node": 265,
"thread": 4
},
{
"assumption": "dma_mask == 0UL;",
"assumption scope": 28,
"file": 4,
"source": "dma_mask = 0UL;",
"source node": 265,
"start line": 110,
"target node": 266,
"thread": 4
},
{
"file": 4,
"source": "dma_mask = (unsigned long)dev->coherent_dma_mask;",
"source node": 266,
"start line": 112,
"target node": 267,
"thread": 4
},
{
"condition": true,
"file": 4,
"source": "dma_mask == 0UL",
"source node": 267,
"start line": 113,
"target node": 268,
"thread": 4
},
{
"condition": true,
"file": 4,
"source": "(((int)gfp) &1) == 0",
"source node": 268,
"start line": 114,
"target node": 269,
"thread": 4
},
{
"file": 4,
"source": "4294967295UL",
"source node": 269,
"start line": 114,
"target node": 270,
"thread": 4
},
{
"assumption": "dma_mask == 4294967295UL;",
"assumption scope": 28,
"file": 4,
"source": "dma_mask = (int)gfp &1 ? 16777215UL : 4294967295UL;",
"source node": 270,
"start line": 114,
"target node": 271,
"thread": 4
},
{
"file": 4,
"return": 28,
"source": "return dma_mask;",
"source node": 271,
"start line": 116,
"target node": 272,
"thread": 4
},
{
"condition": true,
"file": 4,
"source": "((unsigned long long)dma_mask) > 16777215ULL",
"source node": 272,
"start line": 123,
"target node": 273,
"thread": 4
},
{
"condition": true,
"file": 4,
"source": "((unsigned long long)dma_mask) > 4294967295ULL",
"source node": 273,
"start line": 126,
"target node": 274,
"thread": 4
},
{
"file": 4,
"return": 27,
"source": "return gfp;",
"source node": 274,
"start line": 129,
"target node": 275,
"thread": 4
},
{
"file": 4,
"source": "debug_dma_alloc_coherent(dev, size, *dma_handle, memory);",
"source node": 275,
"start line": 157,
"target node": 276,
"thread": 4
},
{
"file": 4,
"return": 24,
"source": "return memory;",
"source node": 276,
"start line": 159,
"target node": 277,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "__CPAchecker_TMP_2 != ((unsigned long)((void *)0))",
"source node": 277,
"start line": 414,
"target node": 278,
"thread": 4
},
{
"file": 5,
"source": "bp->SharedMemHeap = 0UL;",
"source node": 278,
"start line": 420,
"target node": 279,
"thread": 4
},
{
"file": 5,
"source": "memset(bp->SharedMemAddr, 0, bp->SharedMemSize);",
"source node": 279,
"start line": 427,
"target node": 280,
"thread": 4
},
{
"enter": 30,
"file": 5,
"source": "card_stop(smc);",
"source node": 280,
"start line": 429,
"target node": 281,
"thread": 4
},
{
"file": 16,
"source": "u_long tmp;",
"source node": 281,
"start line": 165,
"target node": 282,
"thread": 4
},
{
"enter": 31,
"file": 16,
"source": "smt_stop_watchdog(smc);",
"source node": 282,
"start line": 165,
"target node": 283,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "((int)(smc->hw.wdog_used)) != 0",
"source node": 283,
"start line": 569,
"target node": 284,
"thread": 4
},
{
"file": 16,
"source": "iowrite16(2, smc->hw.iop + 312UL);",
"source node": 284,
"start line": 570,
"target node": 285,
"thread": 4
},
{
"file": 16,
"return": 31,
"source": "return;",
"source node": 285,
"start line": 571,
"target node": 286,
"thread": 4
},
{
"file": 16,
"source": "smc->hw.mac_ring_is_up = 0U;",
"source node": 286,
"start line": 166,
"target node": 287,
"thread": 4
},
{
"file": 16,
"source": "iowrite16(0, smc->hw.iop + 1088UL);",
"source node": 287,
"start line": 172,
"target node": 288,
"thread": 4
},
{
"file": 16,
"source": "iowrite8(16, smc->hw.iop + 4UL);",
"source node": 288,
"start line": 173,
"target node": 289,
"thread": 4
},
{
"enter": 32,
"file": 16,
"source": "tmp = hwt_quick_read(smc);",
"source node": 289,
"start line": 174,
"target node": 290,
"thread": 4
},
{
"file": 30,
"source": "u_long interval;",
"source node": 290,
"start line": 201,
"target node": 291,
"thread": 4
},
{
"file": 30,
"source": "u_long time;",
"source node": 291,
"start line": 202,
"target node": 292,
"thread": 4
},
{
"file": 30,
"source": "interval = (u_long)ioread32(smc->hw.iop + 288UL);",
"source node": 292,
"start line": 204,
"target node": 293,
"thread": 4
},
{
"file": 30,
"source": "iowrite16(2, smc->hw.iop + 296UL);",
"source node": 293,
"start line": 205,
"target node": 294,
"thread": 4
},
{
"file": 30,
"source": "time = (u_long)ioread32(smc->hw.iop + 292UL);",
"source node": 294,
"start line": 206,
"target node": 295,
"thread": 4
},
{
"file": 30,
"source": "iowrite32((u32)time, smc->hw.iop + 288UL);",
"source node": 295,
"start line": 207,
"target node": 296,
"thread": 4
},
{
"file": 30,
"source": "iowrite16(4, smc->hw.iop + 296UL);",
"source node": 296,
"start line": 208,
"target node": 297,
"thread": 4
},
{
"file": 30,
"source": "iowrite32((u32)interval, smc->hw.iop + 288UL);",
"source node": 297,
"start line": 209,
"target node": 298,
"thread": 4
},
{
"file": 30,
"return": 32,
"source": "return time;",
"source node": 298,
"start line": 211,
"target node": 299,
"thread": 4
},
{
"enter": 33,
"file": 16,
"source": "hwt_wait_time(smc, tmp, 125000L);",
"source node": 299,
"start line": 174,
"target node": 300,
"thread": 4
},
{
"file": 30,
"source": "long diff;",
"source node": 300,
"start line": 229,
"target node": 301,
"thread": 4
},
{
"file": 30,
"source": "long interval;",
"source node": 301,
"start line": 230,
"target node": 302,
"thread": 4
},
{
"file": 30,
"source": "int wrapped;",
"source node": 302,
"start line": 231,
"target node": 303,
"thread": 4
},
{
"file": 30,
"source": "u_long tmp;",
"source node": 303,
"start line": 232,
"target node": 304,
"thread": 4
},
{
"condition": true,
"file": 30,
"source": "((unsigned int)(smc->hw.timer_activ)) != 0U",
"source node": 304,
"start line": 236,
"target node": 305,
"thread": 4
},
{
"enter": 32,
"file": 30,
"source": "tmp = hwt_quick_read(smc);",
"source node": 305,
"start line": 236,
"target node": 306,
"thread": 4
},
{
"file": 30,
"source": "u_long interval;",
"source node": 306,
"start line": 201,
"target node": 307,
"thread": 4
},
{
"file": 30,
"source": "u_long time;",
"source node": 307,
"start line": 202,
"target node": 308,
"thread": 4
},
{
"file": 30,
"source": "interval = (u_long)ioread32(smc->hw.iop + 288UL);",
"source node": 308,
"start line": 204,
"target node": 309,
"thread": 4
},
{
"file": 30,
"source": "iowrite16(2, smc->hw.iop + 296UL);",
"source node": 309,
"start line": 205,
"target node": 310,
"thread": 4
},
{
"file": 30,
"source": "time = (u_long)ioread32(smc->hw.iop + 292UL);",
"source node": 310,
"start line": 206,
"target node": 311,
"thread": 4
},
{
"file": 30,
"source": "iowrite32((u32)time, smc->hw.iop + 288UL);",
"source node": 311,
"start line": 207,
"target node": 312,
"thread": 4
},
{
"file": 30,
"source": "iowrite16(4, smc->hw.iop + 296UL);",
"source node": 312,
"start line": 208,
"target node": 313,
"thread": 4
},
{
"file": 30,
"source": "iowrite32((u32)interval, smc->hw.iop + 288UL);",
"source node": 313,
"start line": 209,
"target node": 314,
"thread": 4
},
{
"file": 30,
"return": 32,
"source": "return time;",
"source node": 314,
"start line": 211,
"target node": 315,
"thread": 4
},
{
"condition": true,
"enter": 32,
"file": 30,
"source": "tmp == hwt_quick_read(smc)",
"source node": 315,
"start line": 236,
"target node": 316,
"thread": 4
},
{
"file": 30,
"source": "u_long interval;",
"source node": 316,
"start line": 201,
"target node": 317,
"thread": 4
},
{
"file": 30,
"source": "u_long time;",
"source node": 317,
"start line": 202,
"target node": 318,
"thread": 4
},
{
"file": 30,
"source": "interval = (u_long)ioread32(smc->hw.iop + 288UL);",
"source node": 318,
"start line": 204,
"target node": 319,
"thread": 4
},
{
"file": 30,
"source": "iowrite16(2, smc->hw.iop + 296UL);",
"source node": 319,
"start line": 205,
"target node": 320,
"thread": 4
},
{
"file": 30,
"source": "time = (u_long)ioread32(smc->hw.iop + 292UL);",
"source node": 320,
"start line": 206,
"target node": 321,
"thread": 4
},
{
"file": 30,
"source": "iowrite32((u32)time, smc->hw.iop + 288UL);",
"source node": 321,
"start line": 207,
"target node": 322,
"thread": 4
},
{
"file": 30,
"source": "iowrite16(4, smc->hw.iop + 296UL);",
"source node": 322,
"start line": 208,
"target node": 323,
"thread": 4
},
{
"file": 30,
"source": "iowrite32((u32)interval, smc->hw.iop + 288UL);",
"source node": 323,
"start line": 209,
"target node": 324,
"thread": 4
},
{
"file": 30,
"return": 32,
"source": "return time;",
"source node": 324,
"start line": 211,
"target node": 325,
"thread": 4
},
{
"file": 30,
"return": 33,
"source": "return;",
"source node": 325,
"start line": 238,
"target node": 326,
"thread": 4
},
{
"file": 16,
"source": "iowrite8(1, smc->hw.iop + 4UL);",
"source node": 326,
"start line": 178,
"target node": 327,
"thread": 4
},
{
"file": 16,
"source": "iowrite8(2, smc->hw.iop + 4UL);",
"source node": 327,
"start line": 179,
"target node": 328,
"thread": 4
},
{
"file": 16,
"source": "iowrite8(21, smc->hw.iop + 6UL);",
"source node": 328,
"start line": 180,
"target node": 329,
"thread": 4
},
{
"file": 16,
"source": "smc->hw.hw_state = 0U;",
"source node": 329,
"start line": 181,
"target node": 330,
"thread": 4
},
{
"file": 16,
"return": 30,
"source": "return;",
"source node": 330,
"start line": 182,
"target node": 331,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.modname = \"skfp\";",
"source node": 331,
"start line": 431,
"target node": 332,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.function = \"skfp_driver_init\";",
"source node": 332,
"start line": 431,
"target node": 333,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 333,
"start line": 431,
"target node": 334,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.format = \"mac_drv_init()..\\n\";",
"source node": 334,
"start line": 431,
"target node": 335,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.lineno = 431U;",
"source node": 335,
"start line": 431,
"target node": 336,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.flags = 0U;",
"source node": 336,
"start line": 431,
"target node": 337,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___1.flags &1L, 0L) != 0L",
"source node": 337,
"start line": 431,
"target node": 338,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 338,
"start line": 26,
"target node": 339,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___1, \"mac_drv_init()..\\n\");",
"source node": 339,
"start line": 431,
"target node": 340,
"thread": 4
},
{
"condition": true,
"enter": 34,
"file": 5,
"source": "mac_drv_init(smc) == 0",
"source node": 340,
"start line": 432,
"target node": 341,
"thread": 4
},
{
"enter": 35,
"file": 29,
"source": "tmp = (union s_fp_descr volatile *)mac_drv_get_desc_mem(smc, 1920U);",
"source node": 341,
"start line": 271,
"target node": 342,
"thread": 4
},
{
"file": 5,
"source": "char *virt;",
"source node": 342,
"start line": 1348,
"target node": 343,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor;",
"source node": 343,
"start line": 1349,
"target node": 344,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___0;",
"source node": 344,
"start line": 1352,
"target node": 345,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___1;",
"source node": 345,
"start line": 1354,
"target node": 346,
"thread": 4
},
{
"file": 5,
"source": "descriptor.modname = \"skfp\";",
"source node": 346,
"start line": 1351,
"target node": 347,
"thread": 4
},
{
"file": 5,
"source": "descriptor.function = \"mac_drv_get_desc_mem\";",
"source node": 347,
"start line": 1351,
"target node": 348,
"thread": 4
},
{
"file": 5,
"source": "descriptor.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 348,
"start line": 1351,
"target node": 349,
"thread": 4
},
{
"file": 5,
"source": "descriptor.format = \"mac_drv_get_desc_mem\\n\";",
"source node": 349,
"start line": 1351,
"target node": 350,
"thread": 4
},
{
"file": 5,
"source": "descriptor.lineno = 1351U;",
"source node": 350,
"start line": 1351,
"target node": 351,
"thread": 4
},
{
"file": 5,
"source": "descriptor.flags = 0U;",
"source node": 351,
"start line": 1351,
"target node": 352,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor.flags &1L, 0L) != 0L",
"source node": 352,
"start line": 1351,
"target node": 353,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 353,
"start line": 26,
"target node": 354,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor, \"mac_drv_get_desc_mem\\n\");",
"source node": 354,
"start line": 1351,
"target node": 355,
"thread": 4
},
{
"enter": 36,
"file": 5,
"source": "virt = (char *)mac_drv_get_space(smc, size);",
"source node": 355,
"start line": 1355,
"target node": 356,
"thread": 4
},
{
"file": 5,
"source": "void *virt;",
"source node": 356,
"start line": 1308,
"target node": 357,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor;",
"source node": 357,
"start line": 1309,
"target node": 358,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___0;",
"source node": 358,
"start line": 1311,
"target node": 359,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___1;",
"source node": 359,
"start line": 1313,
"target node": 360,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___2;",
"source node": 360,
"start line": 1315,
"target node": 361,
"thread": 4
},
{
"file": 5,
"source": "descriptor.modname = \"skfp\";",
"source node": 361,
"start line": 1310,
"target node": 362,
"thread": 4
},
{
"file": 5,
"source": "descriptor.function = \"mac_drv_get_space\";",
"source node": 362,
"start line": 1310,
"target node": 363,
"thread": 4
},
{
"file": 5,
"source": "descriptor.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 363,
"start line": 1310,
"target node": 364,
"thread": 4
},
{
"file": 5,
"source": "descriptor.format = \"mac_drv_get_space (%d bytes), \";",
"source node": 364,
"start line": 1310,
"target node": 365,
"thread": 4
},
{
"file": 5,
"source": "descriptor.lineno = 1310U;",
"source node": 365,
"start line": 1310,
"target node": 366,
"thread": 4
},
{
"file": 5,
"source": "descriptor.flags = 0U;",
"source node": 366,
"start line": 1310,
"target node": 367,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor.flags &1L, 0L) != 0L",
"source node": 367,
"start line": 1310,
"target node": 368,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 368,
"start line": 26,
"target node": 369,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor, \"mac_drv_get_space (%d bytes), \", size);",
"source node": 369,
"start line": 1310,
"target node": 370,
"thread": 4
},
{
"file": 5,
"source": "virt = smc->os.SharedMemAddr + smc->os.SharedMemHeap;",
"source node": 370,
"start line": 1311,
"target node": 371,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "((smc->os.SharedMemHeap) + ((ulong)size)) <= (smc->os.SharedMemSize)",
"source node": 371,
"start line": 1313,
"target node": 372,
"thread": 4
},
{
"file": 5,
"source": "smc->os.SharedMemHeap = smc->os.SharedMemHeap + (ulong)size;",
"source node": 372,
"start line": 1317,
"target node": 373,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.modname = \"skfp\";",
"source node": 373,
"start line": 1319,
"target node": 374,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.function = \"mac_drv_get_space\";",
"source node": 374,
"start line": 1319,
"target node": 375,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 375,
"start line": 1319,
"target node": 376,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.format = \"mac_drv_get_space end\\n\";",
"source node": 376,
"start line": 1319,
"target node": 377,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.lineno = 1319U;",
"source node": 377,
"start line": 1319,
"target node": 378,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.flags = 0U;",
"source node": 378,
"start line": 1319,
"target node": 379,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___0.flags &1L, 0L) != 0L",
"source node": 379,
"start line": 1319,
"target node": 380,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 380,
"start line": 26,
"target node": 381,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___0, \"mac_drv_get_space end\\n\");",
"source node": 381,
"start line": 1319,
"target node": 382,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.modname = \"skfp\";",
"source node": 382,
"start line": 1320,
"target node": 383,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.function = \"mac_drv_get_space\";",
"source node": 383,
"start line": 1320,
"target node": 384,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 384,
"start line": 1320,
"target node": 385,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.format = \"virt addr: %lx\\n\";",
"source node": 385,
"start line": 1320,
"target node": 386,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.lineno = 1320U;",
"source node": 386,
"start line": 1320,
"target node": 387,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.flags = 0U;",
"source node": 387,
"start line": 1320,
"target node": 388,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___1.flags &1L, 0L) != 0L",
"source node": 388,
"start line": 1320,
"target node": 389,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 389,
"start line": 26,
"target node": 390,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___1, \"virt addr: %lx\\n\", (unsigned long)virt);",
"source node": 390,
"start line": 1320,
"target node": 391,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.modname = \"skfp\";",
"source node": 391,
"start line": 1321,
"target node": 392,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.function = \"mac_drv_get_space\";",
"source node": 392,
"start line": 1321,
"target node": 393,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 393,
"start line": 1321,
"target node": 394,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.format = \"bus addr: %lx\\n\";",
"source node": 394,
"start line": 1321,
"target node": 395,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.lineno = 1323U;",
"source node": 395,
"start line": 1321,
"target node": 396,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.flags = 0U;",
"source node": 396,
"start line": 1321,
"target node": 397,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___2.flags &1L, 0L) != 0L",
"source node": 397,
"start line": 1321,
"target node": 398,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 398,
"start line": 26,
"target node": 399,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___2, \"bus addr: %lx\\n\", (unsigned long)(smc->os.SharedMemDMA + (unsigned long long)((long)virt - (long)smc->os.SharedMemAddr)));",
"source node": 399,
"start line": 1321,
"target node": 400,
"thread": 4
},
{
"file": 5,
"return": 36,
"source": "return virt;",
"source node": 400,
"start line": 1324,
"target node": 401,
"thread": 4
},
{
"file": 5,
"source": "size = 16U - ((unsigned int)((long)virt) &15U);",
"source node": 401,
"start line": 1357,
"target node": 402,
"thread": 4
},
{
"file": 5,
"source": "size = size &15U;",
"source node": 402,
"start line": 1358,
"target node": 403,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.modname = \"skfp\";",
"source node": 403,
"start line": 1360,
"target node": 404,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.function = \"mac_drv_get_desc_mem\";",
"source node": 404,
"start line": 1360,
"target node": 405,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 405,
"start line": 1360,
"target node": 406,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.format = \"Allocate %u bytes alignment gap \";",
"source node": 406,
"start line": 1360,
"target node": 407,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.lineno = 1360U;",
"source node": 407,
"start line": 1360,
"target node": 408,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.flags = 0U;",
"source node": 408,
"start line": 1360,
"target node": 409,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___0.flags &1L, 0L) != 0L",
"source node": 409,
"start line": 1360,
"target node": 410,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 410,
"start line": 26,
"target node": 411,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___0, \"Allocate %u bytes alignment gap \", size);",
"source node": 411,
"start line": 1360,
"target node": 412,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.modname = \"skfp\";",
"source node": 412,
"start line": 1361,
"target node": 413,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.function = \"mac_drv_get_desc_mem\";",
"source node": 413,
"start line": 1361,
"target node": 414,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 414,
"start line": 1361,
"target node": 415,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.format = \"for descriptor memory.\\n\";",
"source node": 415,
"start line": 1361,
"target node": 416,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.lineno = 1361U;",
"source node": 416,
"start line": 1361,
"target node": 417,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.flags = 0U;",
"source node": 417,
"start line": 1361,
"target node": 418,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___1.flags &1L, 0L) != 0L",
"source node": 418,
"start line": 1361,
"target node": 419,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 419,
"start line": 26,
"target node": 420,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___1, \"for descriptor memory.\\n\");",
"source node": 420,
"start line": 1361,
"target node": 421,
"thread": 4
},
{
"condition": true,
"enter": 36,
"file": 5,
"source": "((unsigned long)mac_drv_get_space(smc, size)) != ((unsigned long)((void *)0))",
"source node": 421,
"start line": 1363,
"target node": 422,
"thread": 4
},
{
"file": 5,
"source": "void *virt;",
"source node": 422,
"start line": 1308,
"target node": 423,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor;",
"source node": 423,
"start line": 1309,
"target node": 424,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___0;",
"source node": 424,
"start line": 1311,
"target node": 425,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___1;",
"source node": 425,
"start line": 1313,
"target node": 426,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___2;",
"source node": 426,
"start line": 1315,
"target node": 427,
"thread": 4
},
{
"file": 5,
"source": "descriptor.modname = \"skfp\";",
"source node": 427,
"start line": 1310,
"target node": 428,
"thread": 4
},
{
"file": 5,
"source": "descriptor.function = \"mac_drv_get_space\";",
"source node": 428,
"start line": 1310,
"target node": 429,
"thread": 4
},
{
"file": 5,
"source": "descriptor.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 429,
"start line": 1310,
"target node": 430,
"thread": 4
},
{
"file": 5,
"source": "descriptor.format = \"mac_drv_get_space (%d bytes), \";",
"source node": 430,
"start line": 1310,
"target node": 431,
"thread": 4
},
{
"file": 5,
"source": "descriptor.lineno = 1310U;",
"source node": 431,
"start line": 1310,
"target node": 432,
"thread": 4
},
{
"file": 5,
"source": "descriptor.flags = 0U;",
"source node": 432,
"start line": 1310,
"target node": 433,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor.flags &1L, 0L) != 0L",
"source node": 433,
"start line": 1310,
"target node": 434,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 434,
"start line": 26,
"target node": 435,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor, \"mac_drv_get_space (%d bytes), \", size);",
"source node": 435,
"start line": 1310,
"target node": 436,
"thread": 4
},
{
"file": 5,
"source": "virt = smc->os.SharedMemAddr + smc->os.SharedMemHeap;",
"source node": 436,
"start line": 1311,
"target node": 437,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "((smc->os.SharedMemHeap) + ((ulong)size)) <= (smc->os.SharedMemSize)",
"source node": 437,
"start line": 1313,
"target node": 438,
"thread": 4
},
{
"file": 5,
"source": "smc->os.SharedMemHeap = smc->os.SharedMemHeap + (ulong)size;",
"source node": 438,
"start line": 1317,
"target node": 439,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.modname = \"skfp\";",
"source node": 439,
"start line": 1319,
"target node": 440,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.function = \"mac_drv_get_space\";",
"source node": 440,
"start line": 1319,
"target node": 441,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 441,
"start line": 1319,
"target node": 442,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.format = \"mac_drv_get_space end\\n\";",
"source node": 442,
"start line": 1319,
"target node": 443,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.lineno = 1319U;",
"source node": 443,
"start line": 1319,
"target node": 444,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.flags = 0U;",
"source node": 444,
"start line": 1319,
"target node": 445,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___0.flags &1L, 0L) != 0L",
"source node": 445,
"start line": 1319,
"target node": 446,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 446,
"start line": 26,
"target node": 447,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___0, \"mac_drv_get_space end\\n\");",
"source node": 447,
"start line": 1319,
"target node": 448,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.modname = \"skfp\";",
"source node": 448,
"start line": 1320,
"target node": 449,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.function = \"mac_drv_get_space\";",
"source node": 449,
"start line": 1320,
"target node": 450,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 450,
"start line": 1320,
"target node": 451,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.format = \"virt addr: %lx\\n\";",
"source node": 451,
"start line": 1320,
"target node": 452,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.lineno = 1320U;",
"source node": 452,
"start line": 1320,
"target node": 453,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.flags = 0U;",
"source node": 453,
"start line": 1320,
"target node": 454,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___1.flags &1L, 0L) != 0L",
"source node": 454,
"start line": 1320,
"target node": 455,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 455,
"start line": 26,
"target node": 456,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___1, \"virt addr: %lx\\n\", (unsigned long)virt);",
"source node": 456,
"start line": 1320,
"target node": 457,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.modname = \"skfp\";",
"source node": 457,
"start line": 1321,
"target node": 458,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.function = \"mac_drv_get_space\";",
"source node": 458,
"start line": 1321,
"target node": 459,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 459,
"start line": 1321,
"target node": 460,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.format = \"bus addr: %lx\\n\";",
"source node": 460,
"start line": 1321,
"target node": 461,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.lineno = 1323U;",
"source node": 461,
"start line": 1321,
"target node": 462,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.flags = 0U;",
"source node": 462,
"start line": 1321,
"target node": 463,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___2.flags &1L, 0L) != 0L",
"source node": 463,
"start line": 1321,
"target node": 464,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 464,
"start line": 26,
"target node": 465,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___2, \"bus addr: %lx\\n\", (unsigned long)(smc->os.SharedMemDMA + (unsigned long long)((long)virt - (long)smc->os.SharedMemAddr)));",
"source node": 465,
"start line": 1321,
"target node": 466,
"thread": 4
},
{
"file": 5,
"return": 36,
"source": "return virt;",
"source node": 466,
"start line": 1324,
"target node": 467,
"thread": 4
},
{
"file": 5,
"return": 35,
"source": "return (void *)(virt + (unsigned long)size);",
"source node": 467,
"start line": 1367,
"target node": 468,
"thread": 4
},
{
"file": 29,
"source": "smc->os.hwm.descr_p = tmp;",
"source node": 468,
"start line": 271,
"target node": 469,
"thread": 4
},
{
"condition": true,
"file": 29,
"source": "((unsigned long)tmp) != ((unsigned long)((volatile union s_fp_descr *)0))",
"source node": 469,
"start line": 271,
"target node": 470,
"thread": 4
},
{
"enter": 36,
"file": 29,
"source": "tmp___1 = (Mbuf *)mac_drv_get_space(smc, 18112U);",
"source node": 470,
"start line": 284,
"target node": 471,
"thread": 4
},
{
"file": 5,
"source": "void *virt;",
"source node": 471,
"start line": 1308,
"target node": 472,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor;",
"source node": 472,
"start line": 1309,
"target node": 473,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___0;",
"source node": 473,
"start line": 1311,
"target node": 474,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___1;",
"source node": 474,
"start line": 1313,
"target node": 475,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor___2;",
"source node": 475,
"start line": 1315,
"target node": 476,
"thread": 4
},
{
"file": 5,
"source": "descriptor.modname = \"skfp\";",
"source node": 476,
"start line": 1310,
"target node": 477,
"thread": 4
},
{
"file": 5,
"source": "descriptor.function = \"mac_drv_get_space\";",
"source node": 477,
"start line": 1310,
"target node": 478,
"thread": 4
},
{
"file": 5,
"source": "descriptor.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 478,
"start line": 1310,
"target node": 479,
"thread": 4
},
{
"file": 5,
"source": "descriptor.format = \"mac_drv_get_space (%d bytes), \";",
"source node": 479,
"start line": 1310,
"target node": 480,
"thread": 4
},
{
"file": 5,
"source": "descriptor.lineno = 1310U;",
"source node": 480,
"start line": 1310,
"target node": 481,
"thread": 4
},
{
"file": 5,
"source": "descriptor.flags = 0U;",
"source node": 481,
"start line": 1310,
"target node": 482,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor.flags &1L, 0L) != 0L",
"source node": 482,
"start line": 1310,
"target node": 483,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 483,
"start line": 26,
"target node": 484,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor, \"mac_drv_get_space (%d bytes), \", size);",
"source node": 484,
"start line": 1310,
"target node": 485,
"thread": 4
},
{
"file": 5,
"source": "virt = smc->os.SharedMemAddr + smc->os.SharedMemHeap;",
"source node": 485,
"start line": 1311,
"target node": 486,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "((smc->os.SharedMemHeap) + ((ulong)size)) <= (smc->os.SharedMemSize)",
"source node": 486,
"start line": 1313,
"target node": 487,
"thread": 4
},
{
"file": 5,
"source": "smc->os.SharedMemHeap = smc->os.SharedMemHeap + (ulong)size;",
"source node": 487,
"start line": 1317,
"target node": 488,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.modname = \"skfp\";",
"source node": 488,
"start line": 1319,
"target node": 489,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.function = \"mac_drv_get_space\";",
"source node": 489,
"start line": 1319,
"target node": 490,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 490,
"start line": 1319,
"target node": 491,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.format = \"mac_drv_get_space end\\n\";",
"source node": 491,
"start line": 1319,
"target node": 492,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.lineno = 1319U;",
"source node": 492,
"start line": 1319,
"target node": 493,
"thread": 4
},
{
"file": 5,
"source": "descriptor___0.flags = 0U;",
"source node": 493,
"start line": 1319,
"target node": 494,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___0.flags &1L, 0L) != 0L",
"source node": 494,
"start line": 1319,
"target node": 495,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 495,
"start line": 26,
"target node": 496,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___0, \"mac_drv_get_space end\\n\");",
"source node": 496,
"start line": 1319,
"target node": 497,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.modname = \"skfp\";",
"source node": 497,
"start line": 1320,
"target node": 498,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.function = \"mac_drv_get_space\";",
"source node": 498,
"start line": 1320,
"target node": 499,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 499,
"start line": 1320,
"target node": 500,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.format = \"virt addr: %lx\\n\";",
"source node": 500,
"start line": 1320,
"target node": 501,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.lineno = 1320U;",
"source node": 501,
"start line": 1320,
"target node": 502,
"thread": 4
},
{
"file": 5,
"source": "descriptor___1.flags = 0U;",
"source node": 502,
"start line": 1320,
"target node": 503,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___1.flags &1L, 0L) != 0L",
"source node": 503,
"start line": 1320,
"target node": 504,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 504,
"start line": 26,
"target node": 505,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___1, \"virt addr: %lx\\n\", (unsigned long)virt);",
"source node": 505,
"start line": 1320,
"target node": 506,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.modname = \"skfp\";",
"source node": 506,
"start line": 1321,
"target node": 507,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.function = \"mac_drv_get_space\";",
"source node": 507,
"start line": 1321,
"target node": 508,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 508,
"start line": 1321,
"target node": 509,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.format = \"bus addr: %lx\\n\";",
"source node": 509,
"start line": 1321,
"target node": 510,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.lineno = 1323U;",
"source node": 510,
"start line": 1321,
"target node": 511,
"thread": 4
},
{
"file": 5,
"source": "descriptor___2.flags = 0U;",
"source node": 511,
"start line": 1321,
"target node": 512,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___2.flags &1L, 0L) != 0L",
"source node": 512,
"start line": 1321,
"target node": 513,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 513,
"start line": 26,
"target node": 514,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___2, \"bus addr: %lx\\n\", (unsigned long)(smc->os.SharedMemDMA + (unsigned long long)((long)virt - (long)smc->os.SharedMemAddr)));",
"source node": 514,
"start line": 1321,
"target node": 515,
"thread": 4
},
{
"file": 5,
"return": 36,
"source": "return virt;",
"source node": 515,
"start line": 1324,
"target node": 516,
"thread": 4
},
{
"file": 29,
"source": "smc->os.hwm.mbuf_pool.mb_start = tmp___1;",
"source node": 516,
"start line": 284,
"target node": 517,
"thread": 4
},
{
"condition": true,
"file": 29,
"source": "((unsigned long)tmp___1) != ((unsigned long)((Mbuf *)0))",
"source node": 517,
"start line": 284,
"target node": 518,
"thread": 4
},
{
"file": 29,
"return": 34,
"source": "return 0;",
"source node": 518,
"start line": 297,
"target node": 519,
"thread": 4
},
{
"enter": 37,
"file": 5,
"source": "read_address(smc, (u_char *)0U);",
"source node": 519,
"start line": 436,
"target node": 520,
"thread": 4
},
{
"file": 16,
"source": "char ConnectorType;",
"source node": 520,
"start line": 286,
"target node": 521,
"thread": 4
},
{
"file": 16,
"source": "char PmdType;",
"source node": 521,
"start line": 287,
"target node": 522,
"thread": 4
},
{
"file": 16,
"source": "int i;",
"source node": 522,
"start line": 288,
"target node": 523,
"thread": 4
},
{
"file": 16,
"source": "unsigned int tmp;",
"source node": 523,
"start line": 289,
"target node": 524,
"thread": 4
},
{
"assumption": "i == 0;",
"assumption scope": 37,
"file": 16,
"source": "i = 0;",
"source node": 524,
"start line": 291,
"target node": 525,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 525,
"start line": 291,
"target node": 526,
"thread": 4
},
{
"file": 16,
"source": "tmp = ioread8(smc->hw.iop + (unsigned long)(i + 256));",
"source node": 526,
"start line": 292,
"target node": 527,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_phys_addr.a[i] = bitrev8((int)((unsigned char)tmp));",
"source node": 527,
"start line": 292,
"target node": 528,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 528,
"start line": 10,
"target node": 529,
"thread": 4
},
{
"assumption": "i == 1;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 529,
"start line": 291,
"target node": 530,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 530,
"start line": 291,
"target node": 531,
"thread": 4
},
{
"file": 16,
"source": "tmp = ioread8(smc->hw.iop + (unsigned long)(i + 256));",
"source node": 531,
"start line": 292,
"target node": 532,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_phys_addr.a[i] = bitrev8((int)((unsigned char)tmp));",
"source node": 532,
"start line": 292,
"target node": 533,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 533,
"start line": 10,
"target node": 534,
"thread": 4
},
{
"assumption": "i == 2;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 534,
"start line": 291,
"target node": 535,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 535,
"start line": 291,
"target node": 536,
"thread": 4
},
{
"file": 16,
"source": "tmp = ioread8(smc->hw.iop + (unsigned long)(i + 256));",
"source node": 536,
"start line": 292,
"target node": 537,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_phys_addr.a[i] = bitrev8((int)((unsigned char)tmp));",
"source node": 537,
"start line": 292,
"target node": 538,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 538,
"start line": 10,
"target node": 539,
"thread": 4
},
{
"assumption": "i == 3;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 539,
"start line": 291,
"target node": 540,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 540,
"start line": 291,
"target node": 541,
"thread": 4
},
{
"file": 16,
"source": "tmp = ioread8(smc->hw.iop + (unsigned long)(i + 256));",
"source node": 541,
"start line": 292,
"target node": 542,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_phys_addr.a[i] = bitrev8((int)((unsigned char)tmp));",
"source node": 542,
"start line": 292,
"target node": 543,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 543,
"start line": 10,
"target node": 544,
"thread": 4
},
{
"assumption": "i == 4;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 544,
"start line": 291,
"target node": 545,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 545,
"start line": 291,
"target node": 546,
"thread": 4
},
{
"file": 16,
"source": "tmp = ioread8(smc->hw.iop + (unsigned long)(i + 256));",
"source node": 546,
"start line": 292,
"target node": 547,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_phys_addr.a[i] = bitrev8((int)((unsigned char)tmp));",
"source node": 547,
"start line": 292,
"target node": 548,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 548,
"start line": 10,
"target node": 549,
"thread": 4
},
{
"assumption": "i == 5;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 549,
"start line": 291,
"target node": 550,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 550,
"start line": 291,
"target node": 551,
"thread": 4
},
{
"file": 16,
"source": "tmp = ioread8(smc->hw.iop + (unsigned long)(i + 256));",
"source node": 551,
"start line": 292,
"target node": 552,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_phys_addr.a[i] = bitrev8((int)((unsigned char)tmp));",
"source node": 552,
"start line": 292,
"target node": 553,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 553,
"start line": 10,
"target node": 554,
"thread": 4
},
{
"assumption": "i == 6;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 554,
"start line": 291,
"target node": 555,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i > 5",
"source node": 555,
"start line": 291,
"target node": 556,
"thread": 4
},
{
"file": 16,
"source": "ConnectorType = (char)ioread8(smc->hw.iop + 264UL);",
"source node": 556,
"start line": 297,
"target node": 557,
"thread": 4
},
{
"file": 16,
"source": "PmdType = (char)ioread8(smc->hw.iop + 265UL);",
"source node": 557,
"start line": 298,
"target node": 558,
"thread": 4
},
{
"file": 16,
"source": "smc->y[1].pmd_type[0] = (u_char)ConnectorType;",
"source node": 558,
"start line": 300,
"target node": 559,
"thread": 4
},
{
"file": 16,
"source": "smc->y[0].pmd_type[0] = tmp___2;",
"source node": 559,
"start line": 300,
"target node": 560,
"thread": 4
},
{
"file": 16,
"source": "smc->y[1].pmd_type[1] = (u_char)PmdType;",
"source node": 560,
"start line": 302,
"target node": 561,
"thread": 4
},
{
"file": 16,
"source": "smc->y[0].pmd_type[1] = tmp___3;",
"source node": 561,
"start line": 302,
"target node": 562,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "((unsigned long)mac_addr) == ((unsigned long)((u_char *)0U))",
"source node": 562,
"start line": 305,
"target node": 563,
"thread": 4
},
{
"file": 16,
"source": "smc->hw.fddi_home_addr = smc->hw.fddi_phys_addr;",
"source node": 563,
"start line": 312,
"target node": 564,
"thread": 4
},
{
"assumption": "i == 0;",
"assumption scope": 37,
"file": 16,
"source": "i = 0;",
"source node": 564,
"start line": 314,
"target node": 565,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 565,
"start line": 314,
"target node": 566,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_canon_addr.a[i] = bitrev8((int)smc->hw.fddi_phys_addr.a[i]);",
"source node": 566,
"start line": 315,
"target node": 567,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 567,
"start line": 10,
"target node": 568,
"thread": 4
},
{
"assumption": "i == 1;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 568,
"start line": 314,
"target node": 569,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 569,
"start line": 314,
"target node": 570,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_canon_addr.a[i] = bitrev8((int)smc->hw.fddi_phys_addr.a[i]);",
"source node": 570,
"start line": 315,
"target node": 571,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 571,
"start line": 10,
"target node": 572,
"thread": 4
},
{
"assumption": "i == 2;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 572,
"start line": 314,
"target node": 573,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 573,
"start line": 314,
"target node": 574,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_canon_addr.a[i] = bitrev8((int)smc->hw.fddi_phys_addr.a[i]);",
"source node": 574,
"start line": 315,
"target node": 575,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 575,
"start line": 10,
"target node": 576,
"thread": 4
},
{
"assumption": "i == 3;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 576,
"start line": 314,
"target node": 577,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 577,
"start line": 314,
"target node": 578,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_canon_addr.a[i] = bitrev8((int)smc->hw.fddi_phys_addr.a[i]);",
"source node": 578,
"start line": 315,
"target node": 579,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 579,
"start line": 10,
"target node": 580,
"thread": 4
},
{
"assumption": "i == 4;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 580,
"start line": 314,
"target node": 581,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 581,
"start line": 314,
"target node": 582,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_canon_addr.a[i] = bitrev8((int)smc->hw.fddi_phys_addr.a[i]);",
"source node": 582,
"start line": 315,
"target node": 583,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 583,
"start line": 10,
"target node": 584,
"thread": 4
},
{
"assumption": "i == 5;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 584,
"start line": 314,
"target node": 585,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i <= 5",
"source node": 585,
"start line": 314,
"target node": 586,
"thread": 4
},
{
"enter": 38,
"file": 16,
"source": "smc->hw.fddi_canon_addr.a[i] = bitrev8((int)smc->hw.fddi_phys_addr.a[i]);",
"source node": 586,
"start line": 315,
"target node": 587,
"thread": 4
},
{
"file": 7,
"return": 38,
"source": "return (unsigned char)byte_rev_table[(int)byte];",
"source node": 587,
"start line": 10,
"target node": 588,
"thread": 4
},
{
"assumption": "i == 6;",
"assumption scope": 37,
"file": 16,
"source": "i = i + 1;",
"source node": 588,
"start line": 314,
"target node": 589,
"thread": 4
},
{
"condition": true,
"file": 16,
"source": "i > 5",
"source node": 589,
"start line": 314,
"target node": 590,
"thread": 4
},
{
"file": 16,
"return": 37,
"source": "return;",
"source node": 590,
"start line": 321,
"target node": 591,
"thread": 4
},
{
"file": 5,
"source": "descriptor___3.modname = \"skfp\";",
"source node": 591,
"start line": 437,
"target node": 592,
"thread": 4
},
{
"file": 5,
"source": "descriptor___3.function = \"skfp_driver_init\";",
"source node": 592,
"start line": 437,
"target node": 593,
"thread": 4
},
{
"file": 5,
"source": "descriptor___3.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 593,
"start line": 437,
"target node": 594,
"thread": 4
},
{
"file": 5,
"source": "descriptor___3.format = \"HW-Addr: %pMF\\n\";",
"source node": 594,
"start line": 437,
"target node": 595,
"thread": 4
},
{
"file": 5,
"source": "descriptor___3.lineno = 437U;",
"source node": 595,
"start line": 437,
"target node": 596,
"thread": 4
},
{
"file": 5,
"source": "descriptor___3.flags = 0U;",
"source node": 596,
"start line": 437,
"target node": 597,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor___3.flags &1L, 0L) != 0L",
"source node": 597,
"start line": 437,
"target node": 598,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 598,
"start line": 26,
"target node": 599,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor___3, \"HW-Addr: %pMF\\n\", (u_char *)(&smc->hw.fddi_canon_addr.a));",
"source node": 599,
"start line": 437,
"target node": 600,
"thread": 4
},
{
"file": 5,
"source": "memcpy((void *)dev->dev_addr, (void const *)(&smc->hw.fddi_canon_addr.a), 6UL);",
"source node": 600,
"start line": 438,
"target node": 601,
"thread": 4
},
{
"enter": 39,
"file": 5,
"source": "smt_reset_defaults(smc, 0);",
"source node": 601,
"start line": 440,
"target node": 602,
"thread": 4
},
{
"file": 13,
"source": "struct smt_config *smt;",
"source node": 602,
"start line": 84,
"target node": 603,
"thread": 4
},
{
"file": 13,
"source": "int i;",
"source node": 603,
"start line": 85,
"target node": 604,
"thread": 4
},
{
"file": 13,
"source": "u_long smt_boot_time;",
"source node": 604,
"start line": 86,
"target node": 605,
"thread": 4
},
{
"enter": 40,
"file": 13,
"source": "smt_init_mib(smc, level);",
"source node": 605,
"start line": 89,
"target node": 606,
"thread": 4
},
{
"file": 13,
"source": "struct fddi_mib *mib;",
"source node": 606,
"start line": 166,
"target node": 607,
"thread": 4
},
{
"file": 13,
"source": "struct fddi_mib_p *pm;",
"source node": 607,
"start line": 167,
"target node": 608,
"thread": 4
},
{
"file": 13,
"source": "int port;",
"source node": 608,
"start line": 168,
"target node": 609,
"thread": 4
},
{
"file": 13,
"source": "int path;",
"source node": 609,
"start line": 169,
"target node": 610,
"thread": 4
},
{
"file": 13,
"source": "mib = &smc->mib;",
"source node": 610,
"start line": 171,
"target node": 611,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "level == 0",
"source node": 611,
"start line": 172,
"target node": 612,
"thread": 4
},
{
"file": 13,
"source": "memset((void *)((char *)smc + 4968U), 0, 3080UL);",
"source node": 612,
"start line": 177,
"target node": 613,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTOpVersionId = 2U;",
"source node": 613,
"start line": 187,
"target node": 614,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTHiVersionId = 2U;",
"source node": 614,
"start line": 188,
"target node": 615,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTLoVersionId = 2U;",
"source node": 615,
"start line": 189,
"target node": 616,
"thread": 4
},
{
"file": 13,
"source": "memcpy((void *)(&mib->fddiSMTManufacturerData), (void const *)(&man_data), 32UL);",
"source node": 616,
"start line": 190,
"target node": 617,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "level == 0",
"source node": 617,
"start line": 191,
"target node": 618,
"thread": 4
},
{
"file": 13,
"source": "strcpy((char *)(&mib->fddiSMTUserData), \"SK-NET FDDI V2.0 Userdata\");",
"source node": 618,
"start line": 192,
"target node": 619,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTMIBVersionId = 1U;",
"source node": 619,
"start line": 194,
"target node": 620,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTMac_Ct = 1U;",
"source node": 620,
"start line": 195,
"target node": 621,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTConnectionPolicy = 32801U;",
"source node": 621,
"start line": 196,
"target node": 622,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTAvailablePaths = 3U;",
"source node": 622,
"start line": 202,
"target node": 623,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTConfigCapabilities = 0U;",
"source node": 623,
"start line": 204,
"target node": 624,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTTT_Notify = 10U;",
"source node": 624,
"start line": 205,
"target node": 625,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTStatRptPolicy = 1U;",
"source node": 625,
"start line": 206,
"target node": 626,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTTrace_MaxExpiration = 87500000UL;",
"source node": 626,
"start line": 207,
"target node": 627,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTMACIndexes = 1U;",
"source node": 627,
"start line": 208,
"target node": 628,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTStationStatus = 1U;",
"source node": 628,
"start line": 209,
"target node": 629,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACIndex = 1U;",
"source node": 629,
"start line": 211,
"target node": 630,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACFrameStatusFunctions = 0U;",
"source node": 630,
"start line": 212,
"target node": 631,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACRequestedPaths = 7U;",
"source node": 631,
"start line": 213,
"target node": 632,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACAvailablePaths = 1U;",
"source node": 632,
"start line": 217,
"target node": 633,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACCurrentPath = 3U;",
"source node": 633,
"start line": 218,
"target node": 634,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACT_MaxCapabilitiy = 0xffffffffffe0875cUL;",
"source node": 634,
"start line": 219,
"target node": 635,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACTVXCapabilitiy = 0xffffffffffff0218UL;",
"source node": 635,
"start line": 220,
"target node": 636,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "level == 0",
"source node": 636,
"start line": 221,
"target node": 637,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACTvxValue = 0xffffffffffff7c2aUL;",
"source node": 637,
"start line": 222,
"target node": 638,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACTvxValueMIB = 0xffffffffffff7c2aUL;",
"source node": 638,
"start line": 223,
"target node": 639,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACT_Req = 0xffffffffffe0875cUL;",
"source node": 639,
"start line": 224,
"target node": 640,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACT_ReqMIB = 0xffffffffffe0875cUL;",
"source node": 640,
"start line": 225,
"target node": 641,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACT_Max = 0xffffffffffe0875cUL;",
"source node": 641,
"start line": 226,
"target node": 642,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACT_MaxMIB = 0xffffffffffe0875cUL;",
"source node": 642,
"start line": 227,
"target node": 643,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACT_Min = 0xffffffffffff3cb0UL;",
"source node": 643,
"start line": 228,
"target node": 644,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACHardwarePresent = 1U;",
"source node": 644,
"start line": 230,
"target node": 645,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACMA_UnitdataEnable = 1U;",
"source node": 645,
"start line": 231,
"target node": 646,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACFrameErrorThreshold = 1U;",
"source node": 646,
"start line": 232,
"target node": 647,
"thread": 4
},
{
"file": 13,
"source": "mib->m[0].fddiMACNotCopiedThreshold = 1U;",
"source node": 647,
"start line": 233,
"target node": 648,
"thread": 4
},
{
"assumption": "path == 0;",
"assumption scope": 40,
"file": 13,
"source": "path = 0;",
"source node": 648,
"start line": 237,
"target node": 649,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "path <= 1",
"source node": 649,
"start line": 237,
"target node": 650,
"thread": 4
},
{
"file": 13,
"source": "mib->a[path].fddiPATHIndex = (unsigned int)((ResId)path) + 1U;",
"source node": 650,
"start line": 238,
"target node": 651,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "level == 0",
"source node": 651,
"start line": 239,
"target node": 652,
"thread": 4
},
{
"file": 13,
"source": "mib->a[path].fddiPATHTVXLowerBound = 0xffffffffffff7c2aUL;",
"source node": 652,
"start line": 240,
"target node": 653,
"thread": 4
},
{
"file": 13,
"source": "mib->a[path].fddiPATHT_MaxLowerBound = 0xffffffffffe0875cUL;",
"source node": 653,
"start line": 242,
"target node": 654,
"thread": 4
},
{
"file": 13,
"source": "mib->a[path].fddiPATHMaxT_Req = 0xffffffffffe0875cUL;",
"source node": 654,
"start line": 244,
"target node": 655,
"thread": 4
},
{
"assumption": "path == 1;",
"assumption scope": 40,
"file": 13,
"source": "path = path + 1;",
"source node": 655,
"start line": 237,
"target node": 656,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "path <= 1",
"source node": 656,
"start line": 237,
"target node": 657,
"thread": 4
},
{
"file": 13,
"source": "mib->a[path].fddiPATHIndex = (unsigned int)((ResId)path) + 1U;",
"source node": 657,
"start line": 238,
"target node": 658,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "level == 0",
"source node": 658,
"start line": 239,
"target node": 659,
"thread": 4
},
{
"file": 13,
"source": "mib->a[path].fddiPATHTVXLowerBound = 0xffffffffffff7c2aUL;",
"source node": 659,
"start line": 240,
"target node": 660,
"thread": 4
},
{
"file": 13,
"source": "mib->a[path].fddiPATHT_MaxLowerBound = 0xffffffffffe0875cUL;",
"source node": 660,
"start line": 242,
"target node": 661,
"thread": 4
},
{
"file": 13,
"source": "mib->a[path].fddiPATHMaxT_Req = 0xffffffffffe0875cUL;",
"source node": 661,
"start line": 244,
"target node": 662,
"thread": 4
},
{
"assumption": "path == 2;",
"assumption scope": 40,
"file": 13,
"source": "path = path + 1;",
"source node": 662,
"start line": 237,
"target node": 663,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "path > 1",
"source node": 663,
"start line": 237,
"target node": 664,
"thread": 4
},
{
"file": 13,
"source": "pm = (struct fddi_mib_p *)(&mib->p);",
"source node": 664,
"start line": 253,
"target node": 665,
"thread": 4
},
{
"assumption": "port == 0;",
"assumption scope": 40,
"file": 13,
"source": "port = 0;",
"source node": 665,
"start line": 254,
"target node": 666,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "port <= 1",
"source node": 666,
"start line": 254,
"target node": 667,
"thread": 4
},
{
"file": 13,
"source": "smc->y[port].mib = (struct fddi_mib_p *)0;",
"source node": 667,
"start line": 260,
"target node": 668,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTPORTIndexes[port] = (unsigned int)((u_short)port) + 1U;",
"source node": 668,
"start line": 261,
"target node": 669,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTIndex = (unsigned int)((ResId)port) + 1U;",
"source node": 669,
"start line": 263,
"target node": 670,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTHardwarePresent = 1U;",
"source node": 670,
"start line": 264,
"target node": 671,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "level == 0",
"source node": 671,
"start line": 265,
"target node": 672,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTLer_Alarm = 8U;",
"source node": 672,
"start line": 266,
"target node": 673,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTLer_Cutoff = 7U;",
"source node": 673,
"start line": 267,
"target node": 674,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTRequestedPaths[1] = 0U;",
"source node": 674,
"start line": 273,
"target node": 675,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTRequestedPaths[2] = 0U;",
"source node": 675,
"start line": 274,
"target node": 676,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTRequestedPaths[3] = 0U;",
"source node": 676,
"start line": 275,
"target node": 677,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTAvailablePaths = 1U;",
"source node": 677,
"start line": 276,
"target node": 678,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTPMDClass = 0U;",
"source node": 678,
"start line": 277,
"target node": 679,
"thread": 4
},
{
"file": 13,
"source": "pm = pm + 1;",
"source node": 679,
"start line": 278,
"target node": 680,
"thread": 4
},
{
"assumption": "port == 1;",
"assumption scope": 40,
"file": 13,
"source": "port = port + 1;",
"source node": 680,
"start line": 254,
"target node": 681,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "port <= 1",
"source node": 681,
"start line": 254,
"target node": 682,
"thread": 4
},
{
"file": 13,
"source": "smc->y[port].mib = (struct fddi_mib_p *)0;",
"source node": 682,
"start line": 260,
"target node": 683,
"thread": 4
},
{
"file": 13,
"source": "mib->fddiSMTPORTIndexes[port] = (unsigned int)((u_short)port) + 1U;",
"source node": 683,
"start line": 261,
"target node": 684,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTIndex = (unsigned int)((ResId)port) + 1U;",
"source node": 684,
"start line": 263,
"target node": 685,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTHardwarePresent = 1U;",
"source node": 685,
"start line": 264,
"target node": 686,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "level == 0",
"source node": 686,
"start line": 265,
"target node": 687,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTLer_Alarm = 8U;",
"source node": 687,
"start line": 266,
"target node": 688,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTLer_Cutoff = 7U;",
"source node": 688,
"start line": 267,
"target node": 689,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTRequestedPaths[1] = 0U;",
"source node": 689,
"start line": 273,
"target node": 690,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTRequestedPaths[2] = 0U;",
"source node": 690,
"start line": 274,
"target node": 691,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTRequestedPaths[3] = 0U;",
"source node": 691,
"start line": 275,
"target node": 692,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTAvailablePaths = 1U;",
"source node": 692,
"start line": 276,
"target node": 693,
"thread": 4
},
{
"file": 13,
"source": "pm->fddiPORTPMDClass = 0U;",
"source node": 693,
"start line": 277,
"target node": 694,
"thread": 4
},
{
"file": 13,
"source": "pm = pm + 1;",
"source node": 694,
"start line": 278,
"target node": 695,
"thread": 4
},
{
"assumption": "port == 2;",
"assumption scope": 40,
"file": 13,
"source": "port = port + 1;",
"source node": 695,
"start line": 254,
"target node": 696,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "port > 1",
"source node": 696,
"start line": 254,
"target node": 697,
"thread": 4
},
{
"enter": 41,
"file": 13,
"source": "smt_set_mac_opvalues(smc);",
"source node": 697,
"start line": 281,
"target node": 698,
"thread": 4
},
{
"file": 13,
"source": "int st;",
"source node": 698,
"start line": 286,
"target node": 699,
"thread": 4
},
{
"file": 13,
"source": "int st2;",
"source node": 699,
"start line": 287,
"target node": 700,
"thread": 4
},
{
"enter": 42,
"file": 13,
"source": "st = set_min_max(1, smc->mib.m[0].fddiMACTvxValueMIB, smc->mib.a[0].fddiPATHTVXLowerBound, &smc->mib.m[0].fddiMACTvxValue);",
"source node": 700,
"start line": 289,
"target node": 701,
"thread": 4
},
{
"file": 13,
"source": "u_long old;",
"source node": 701,
"start line": 347,
"target node": 702,
"thread": 4
},
{
"file": 13,
"source": "old = *oper;",
"source node": 702,
"start line": 348,
"target node": 703,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "(limit > mib) != maxflag",
"source node": 703,
"start line": 349,
"target node": 704,
"thread": 4
},
{
"file": 13,
"source": "*oper = limit;",
"source node": 704,
"start line": 350,
"target node": 705,
"thread": 4
},
{
"file": 13,
"return": 42,
"source": "return old != *oper;",
"source node": 705,
"start line": 353,
"target node": 706,
"thread": 4
},
{
"enter": 42,
"file": 13,
"source": "st = st | set_min_max(0, smc->mib.m[0].fddiMACT_MaxMIB, smc->mib.a[0].fddiPATHT_MaxLowerBound, &smc->mib.m[0].fddiMACT_Max);",
"source node": 706,
"start line": 292,
"target node": 707,
"thread": 4
},
{
"file": 13,
"source": "u_long old;",
"source node": 707,
"start line": 347,
"target node": 708,
"thread": 4
},
{
"file": 13,
"source": "old = *oper;",
"source node": 708,
"start line": 348,
"target node": 709,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "(limit > mib) != maxflag",
"source node": 709,
"start line": 349,
"target node": 710,
"thread": 4
},
{
"file": 13,
"source": "*oper = limit;",
"source node": 710,
"start line": 350,
"target node": 711,
"thread": 4
},
{
"file": 13,
"return": 42,
"source": "return old != *oper;",
"source node": 711,
"start line": 353,
"target node": 712,
"thread": 4
},
{
"enter": 42,
"file": 13,
"source": "st2 = set_min_max(0, smc->mib.m[0].fddiMACT_ReqMIB, smc->mib.a[0].fddiPATHMaxT_Req, &smc->mib.m[0].fddiMACT_Req);",
"source node": 712,
"start line": 295,
"target node": 713,
"thread": 4
},
{
"file": 13,
"source": "u_long old;",
"source node": 713,
"start line": 347,
"target node": 714,
"thread": 4
},
{
"file": 13,
"source": "old = *oper;",
"source node": 714,
"start line": 348,
"target node": 715,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "(limit > mib) != maxflag",
"source node": 715,
"start line": 349,
"target node": 716,
"thread": 4
},
{
"file": 13,
"source": "*oper = limit;",
"source node": 716,
"start line": 350,
"target node": 717,
"thread": 4
},
{
"file": 13,
"return": 42,
"source": "return old != *oper;",
"source node": 717,
"start line": 353,
"target node": 718,
"thread": 4
},
{
"file": 13,
"source": "st = st | st2;",
"source node": 718,
"start line": 295,
"target node": 719,
"thread": 4
},
{
"file": 13,
"return": 41,
"source": "return st;",
"source node": 719,
"start line": 306,
"target node": 720,
"thread": 4
},
{
"file": 13,
"return": 40,
"source": "return;",
"source node": 720,
"start line": 282,
"target node": 721,
"thread": 4
},
{
"file": 13,
"source": "smc->os.smc_version = 1UL;",
"source node": 721,
"start line": 91,
"target node": 722,
"thread": 4
},
{
"enter": 43,
"file": 13,
"source": "smt_boot_time = smt_get_time();",
"source node": 722,
"start line": 92,
"target node": 723,
"thread": 4
},
{
"file": 5,
"return": 43,
"source": "return (u_long)jiffies;",
"source node": 723,
"start line": 2014,
"target node": 724,
"thread": 4
},
{
"assumption": "i == 0;",
"assumption scope": 39,
"file": 13,
"source": "i = 0;",
"source node": 724,
"start line": 93,
"target node": 725,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "i <= 0",
"source node": 725,
"start line": 93,
"target node": 726,
"thread": 4
},
{
"file": 13,
"source": "smc->sm.last_tok_time[i] = smt_boot_time;",
"source node": 726,
"start line": 94,
"target node": 727,
"thread": 4
},
{
"assumption": "i == 1;",
"assumption scope": 39,
"file": 13,
"source": "i = i + 1;",
"source node": 727,
"start line": 93,
"target node": 728,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "i > 0",
"source node": 728,
"start line": 93,
"target node": 729,
"thread": 4
},
{
"file": 13,
"source": "smt = &smc->s;",
"source node": 729,
"start line": 95,
"target node": 730,
"thread": 4
},
{
"file": 13,
"source": "smt->attach_s = 0U;",
"source node": 730,
"start line": 96,
"target node": 731,
"thread": 4
},
{
"file": 13,
"source": "smt->build_ring_map = 1U;",
"source node": 731,
"start line": 97,
"target node": 732,
"thread": 4
},
{
"file": 13,
"source": "smt->sas = 0U;",
"source node": 732,
"start line": 98,
"target node": 733,
"thread": 4
},
{
"file": 13,
"source": "smt->numphys = 2U;",
"source node": 733,
"start line": 99,
"target node": 734,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_tb_min = 5000UL;",
"source node": 734,
"start line": 100,
"target node": 735,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_tb_max = 50000UL;",
"source node": 735,
"start line": 101,
"target node": 736,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_c_min = 1600UL;",
"source node": 736,
"start line": 102,
"target node": 737,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_t_out = 105000UL;",
"source node": 737,
"start line": 103,
"target node": 738,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_tl_min = 30UL;",
"source node": 738,
"start line": 104,
"target node": 739,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_lc_short = 55000UL;",
"source node": 739,
"start line": 105,
"target node": 740,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_lc_medium = 520000UL;",
"source node": 740,
"start line": 106,
"target node": 741,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_lc_long = 5050000UL;",
"source node": 741,
"start line": 107,
"target node": 742,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_lc_extended = 50050000UL;",
"source node": 742,
"start line": 108,
"target node": 743,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_t_next_9 = 210000UL;",
"source node": 743,
"start line": 109,
"target node": 744,
"thread": 4
},
{
"file": 13,
"source": "smt->pcm_ns_max = 1310UL;",
"source node": 744,
"start line": 110,
"target node": 745,
"thread": 4
},
{
"file": 13,
"source": "smt->ecm_i_max = 25000UL;",
"source node": 745,
"start line": 111,
"target node": 746,
"thread": 4
},
{
"file": 13,
"source": "smt->ecm_in_max = 40000UL;",
"source node": 746,
"start line": 112,
"target node": 747,
"thread": 4
},
{
"file": 13,
"source": "smt->ecm_td_min = 5000UL;",
"source node": 747,
"start line": 113,
"target node": 748,
"thread": 4
},
{
"file": 13,
"source": "smt->ecm_test_done = 1000000UL;",
"source node": 748,
"start line": 114,
"target node": 749,
"thread": 4
},
{
"file": 13,
"source": "smt->ecm_check_poll = 1000000UL;",
"source node": 749,
"start line": 115,
"target node": 750,
"thread": 4
},
{
"file": 13,
"source": "smt->rmt_t_non_op = 1000000UL;",
"source node": 750,
"start line": 116,
"target node": 751,
"thread": 4
},
{
"file": 13,
"source": "smt->rmt_t_stuck = 8000000UL;",
"source node": 751,
"start line": 117,
"target node": 752,
"thread": 4
},
{
"file": 13,
"source": "smt->rmt_t_direct = 370000UL;",
"source node": 752,
"start line": 118,
"target node": 753,
"thread": 4
},
{
"file": 13,
"source": "smt->rmt_t_jam = 370000UL;",
"source node": 753,
"start line": 119,
"target node": 754,
"thread": 4
},
{
"file": 13,
"source": "smt->rmt_t_announce = 2500000UL;",
"source node": 754,
"start line": 120,
"target node": 755,
"thread": 4
},
{
"file": 13,
"source": "smt->rmt_t_poll = 50000UL;",
"source node": 755,
"start line": 121,
"target node": 756,
"thread": 4
},
{
"file": 13,
"source": "smt->rmt_dup_mac_behavior = 0UL;",
"source node": 756,
"start line": 122,
"target node": 757,
"thread": 4
},
{
"file": 13,
"source": "smt->mac_d_max = 1617UL;",
"source node": 757,
"start line": 123,
"target node": 758,
"thread": 4
},
{
"file": 13,
"source": "smt->lct_short = 1UL;",
"source node": 758,
"start line": 125,
"target node": 759,
"thread": 4
},
{
"file": 13,
"source": "smt->lct_medium = 3UL;",
"source node": 759,
"start line": 126,
"target node": 760,
"thread": 4
},
{
"file": 13,
"source": "smt->lct_long = 5UL;",
"source node": 760,
"start line": 127,
"target node": 761,
"thread": 4
},
{
"file": 13,
"source": "smt->lct_extended = 50UL;",
"source node": 761,
"start line": 128,
"target node": 762,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "level == 0",
"source node": 762,
"start line": 132,
"target node": 763,
"thread": 4
},
{
"file": 13,
"source": "smc->ess.sync_bw_available = 0U;",
"source node": 763,
"start line": 133,
"target node": 764,
"thread": 4
},
{
"file": 13,
"source": "smc->mib.fddiESSPayload = 0UL;",
"source node": 764,
"start line": 134,
"target node": 765,
"thread": 4
},
{
"file": 13,
"source": "smc->mib.fddiESSOverhead = 0UL;",
"source node": 765,
"start line": 135,
"target node": 766,
"thread": 4
},
{
"file": 13,
"source": "smc->mib.fddiESSMaxTNeg = 0xfffffffffffb3b4cUL;",
"source node": 766,
"start line": 136,
"target node": 767,
"thread": 4
},
{
"file": 13,
"source": "smc->mib.fddiESSMinSegmentSize = 1UL;",
"source node": 767,
"start line": 137,
"target node": 768,
"thread": 4
},
{
"file": 13,
"source": "smc->mib.fddiESSCategory = 1UL;",
"source node": 768,
"start line": 138,
"target node": 769,
"thread": 4
},
{
"file": 13,
"source": "smc->mib.fddiESSSynchTxMode = 0;",
"source node": 769,
"start line": 139,
"target node": 770,
"thread": 4
},
{
"file": 13,
"source": "smc->ess.raf_act_timer_poll = 0;",
"source node": 770,
"start line": 140,
"target node": 771,
"thread": 4
},
{
"file": 13,
"source": "smc->ess.timer_count = 7;",
"source node": 771,
"start line": 141,
"target node": 772,
"thread": 4
},
{
"file": 13,
"source": "smc->ess.local_sba_active = 0U;",
"source node": 772,
"start line": 143,
"target node": 773,
"thread": 4
},
{
"file": 13,
"source": "smc->ess.sba_reply_pend = (Mbuf *)0;",
"source node": 773,
"start line": 144,
"target node": 774,
"thread": 4
},
{
"condition": true,
"file": 13,
"source": "level == 0",
"source node": 774,
"start line": 151,
"target node": 775,
"thread": 4
},
{
"file": 13,
"source": "smc->hw.pci_fix_value = 0UL;",
"source node": 775,
"start line": 152,
"target node": 776,
"thread": 4
},
{
"file": 13,
"return": 39,
"source": "return;",
"source node": 776,
"start line": 153,
"target node": 777,
"thread": 4
},
{
"file": 5,
"return": 22,
"source": "return 0;",
"source node": 777,
"start line": 442,
"target node": 778,
"thread": 4
},
{
"condition": true,
"file": 5,
"source": "err == 0",
"source node": 778,
"start line": 280,
"target node": 779,
"thread": 4
},
{
"enter": 45,
"file": 5,
"source": "err = ldv_emg_register_netdev(dev);",
"source node": 779,
"start line": 283,
"target node": 780,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "struct net_device *ldv_8_netdev_net_device;",
"source node": 780,
"start line": 278,
"target node": 781,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "int ldv_8_ret_default;",
"source node": 781,
"start line": 279,
"target node": 782,
"thread": 4
},
{
"action": 11,
"file": 0,
"source": "ldv_8_netdev_net_device = arg0;",
"source node": 782,
"start line": 288,
"target node": 783,
"thread": 4
},
{
"action": 12,
"enter": 47,
"file": 5,
"original file": 0,
"original start line": 293,
"source": "ldv_8_ret_default = skfp_open(ldv_8_netdev_net_device);",
"source node": 783,
"start line": 484,
"target node": 784,
"thread": 4
},
{
"file": 5,
"source": "struct s_smc *smc;",
"source node": 784,
"start line": 484,
"target node": 785,
"thread": 4
},
{
"file": 5,
"source": "int err;",
"source node": 785,
"start line": 486,
"target node": 786,
"thread": 4
},
{
"file": 5,
"source": "struct _ddebug descriptor;",
"source node": 786,
"start line": 487,
"target node": 787,
"thread": 4
},
{
"enter": 18,
"file": 5,
"source": "smc = (struct s_smc *)netdev_priv((struct net_device const *)dev);",
"source node": 787,
"start line": 484,
"target node": 788,
"thread": 4
},
{
"file": 24,
"return": 18,
"source": "return (void *)((char *)dev + 3200UL);",
"source node": 788,
"start line": 1605,
"target node": 789,
"thread": 4
},
{
"file": 5,
"source": "descriptor.modname = \"skfp\";",
"source node": 789,
"start line": 487,
"target node": 790,
"thread": 4
},
{
"file": 5,
"source": "descriptor.function = \"skfp_open\";",
"source node": 790,
"start line": 487,
"target node": 791,
"thread": 4
},
{
"file": 5,
"source": "descriptor.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 791,
"start line": 487,
"target node": 792,
"thread": 4
},
{
"file": 5,
"source": "descriptor.format = \"entering skfp_open\\n\";",
"source node": 792,
"start line": 487,
"target node": 793,
"thread": 4
},
{
"file": 5,
"source": "descriptor.lineno = 487U;",
"source node": 793,
"start line": 487,
"target node": 794,
"thread": 4
},
{
"file": 5,
"source": "descriptor.flags = 0U;",
"source node": 794,
"start line": 487,
"target node": 795,
"thread": 4
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor.flags &1L, 0L) != 0L",
"source node": 795,
"start line": 487,
"target node": 796,
"thread": 4
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 796,
"start line": 26,
"target node": 797,
"thread": 4
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor, \"entering skfp_open\\n\");",
"source node": 797,
"start line": 487,
"target node": 798,
"thread": 4
},
{
"enter": 49,
"file": 5,
"source": "err = ldv_emg_request_irq((unsigned int)dev->irq, &skfp_interrupt, 128UL, (char const *)(&dev->name), (void *)dev);",
"source node": 798,
"start line": 489,
"target node": 799,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "irqreturn_t (*ldv_9_callback_handler)(int, void *);",
"source node": 799,
"start line": 337,
"target node": 800,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "void *ldv_9_data_data;",
"source node": 800,
"start line": 338,
"target node": 801,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "int ldv_9_line_line;",
"source node": 801,
"start line": 339,
"target node": 802,
"thread": 4
},
{
"action": 2,
"file": 0,
"source": "irqreturn_t (*ldv_9_thread_thread)(int, void *);",
"source node": 802,
"start line": 340,
"target node": 803,
"thread": 4
},
{
"action": 13,
"file": 0,
"source": "ldv_9_line_line = (int)arg0;",
"source node": 803,
"start line": 346,
"target node": 804,
"thread": 4
},
{
"action": 13,
"file": 0,
"source": "ldv_9_callback_handler = arg1;",
"source node": 804,
"start line": 347,
"target node": 805,
"thread": 4
},
{
"action": 13,
"file": 0,
"source": "ldv_9_thread_thread = (irqreturn_t (*)(int, void *))0;",
"source node": 805,
"start line": 348,
"target node": 806,
"thread": 4
},
{
"action": 13,
"file": 0,
"source": "ldv_9_data_data = arg4;",
"source node": 806,
"start line": 349,
"target node": 807,
"thread": 4
},
{
"action": 14,
"enter": 50,
"file": 0,
"source": "ldv_dispatch_irq_register_9_3(ldv_9_line_line, ldv_9_callback_handler, ldv_9_thread_thread, ldv_9_data_data);",
"source node": 807,
"start line": 353,
"target node": 808,
"thread": 4
},
{
"file": 0,
"source": "struct ldv_struct_interrupt_scenario_2 *cf_arg_2;",
"source node": 808,
"start line": 155,
"target node": 809,
"thread": 4
},
{
"enter": 2,
"file": 0,
"source": "cf_arg_2 = (struct ldv_struct_interrupt_scenario_2 *)ldv_xmalloc(40UL);",
"source node": 809,
"start line": 154,
"target node": 810,
"thread": 4
},
{
"file": 19,
"source": "void *res;",
"source node": 810,
"start line": 68,
"target node": 811,
"thread": 4
},
{
"file": 19,
"source": "res = malloc(size);",
"source node": 811,
"start line": 68,
"target node": 812,
"thread": 4
},
{
"condition": true,
"file": 19,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 812,
"start line": 69,
"target node": 813,
"thread": 4
},
{
"condition": true,
"enter": 3,
"file": 19,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 813,
"start line": 70,
"target node": 814,
"thread": 4
},
{
"file": 20,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 814,
"start line": 22,
"target node": 815,
"thread": 4
},
{
"file": 19,
"return": 2,
"source": "return res;",
"source node": 815,
"start line": 71,
"target node": 816,
"thread": 4
},
{
"file": 0,
"source": "cf_arg_2->arg0 = arg0;",
"source node": 816,
"start line": 155,
"target node": 817,
"thread": 4
},
{
"file": 0,
"source": "cf_arg_2->arg1 = arg1;",
"source node": 817,
"start line": 156,
"target node": 818,
"thread": 4
},
{
"file": 0,
"source": "cf_arg_2->arg2 = arg2;",
"source node": 818,
"start line": 157,
"target node": 819,
"thread": 4
},
{
"file": 0,
"source": "cf_arg_2->arg3 = arg3;",
"source node": 819,
"start line": 158,
"target node": 820,
"thread": 4
},
{
"enter": 51,
"file": 0,
"source": "ldv_interrupt_scenario_2((void *)cf_arg_2);",
"source node": 820,
"start line": 159,
"target node": 821,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "irqreturn_t (*ldv_2_callback_handler)(int, void *);",
"source node": 821,
"start line": 465,
"target node": 822,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "void *ldv_2_data_data;",
"source node": 822,
"start line": 466,
"target node": 823,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "int ldv_2_line_line;",
"source node": 823,
"start line": 467,
"target node": 824,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "enum irqreturn ldv_2_ret_val_default;",
"source node": 824,
"start line": 468,
"target node": 825,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "irqreturn_t (*ldv_2_thread_thread)(int, void *);",
"source node": 825,
"start line": 469,
"target node": 826,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "struct ldv_struct_interrupt_scenario_2 *data;",
"source node": 826,
"start line": 470,
"target node": 827,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "data = (struct ldv_struct_interrupt_scenario_2 *)arg0;",
"source node": 827,
"start line": 472,
"target node": 828,
"thread": 2
},
{
"action": 15,
"condition": true,
"file": 0,
"source": "((unsigned long)data) != ((unsigned long)((struct ldv_struct_interrupt_scenario_2 *)0))",
"source node": 828,
"start line": 477,
"target node": 829,
"thread": 2
},
{
"action": 15,
"file": 0,
"source": "ldv_2_line_line = data->arg0;",
"source node": 829,
"start line": 478,
"target node": 830,
"thread": 2
},
{
"action": 15,
"file": 0,
"source": "ldv_2_callback_handler = data->arg1;",
"source node": 830,
"start line": 479,
"target node": 831,
"thread": 2
},
{
"action": 15,
"file": 0,
"source": "ldv_2_thread_thread = data->arg2;",
"source node": 831,
"start line": 480,
"target node": 832,
"thread": 2
},
{
"action": 15,
"file": 0,
"source": "ldv_2_data_data = data->arg3;",
"source node": 832,
"start line": 481,
"target node": 833,
"thread": 2
},
{
"action": 15,
"enter": 5,
"file": 0,
"source": "ldv_free((void *)data);",
"source node": 833,
"start line": 482,
"target node": 834,
"thread": 2
},
{
"file": 19,
"source": "free(s);",
"source node": 834,
"start line": 63,
"target node": 835,
"thread": 2
},
{
"file": 19,
"return": 5,
"source": "return;",
"source node": 835,
"start line": 64,
"target node": 836,
"thread": 2
},
{
"action": 16,
"file": 0,
"source": "ldv_switch_to_interrupt_context();",
"source node": 836,
"start line": 488,
"target node": 837,
"thread": 2
},
{
"action": 16,
"enter": 53,
"file": 5,
"original file": 0,
"original start line": 490,
"source": "ldv_2_ret_val_default = skfp_interrupt(ldv_2_line_line, ldv_2_data_data);",
"source node": 837,
"start line": 608,
"target node": 838,
"thread": 2
},
{
"file": 5,
"source": "struct net_device *dev;",
"source node": 838,
"start line": 608,
"target node": 839,
"thread": 2
},
{
"file": 5,
"source": "struct s_smc *smc;",
"source node": 839,
"start line": 609,
"target node": 840,
"thread": 2
},
{
"file": 5,
"source": "skfddi_priv *bp;",
"source node": 840,
"start line": 610,
"target node": 841,
"thread": 2
},
{
"file": 5,
"source": "dev = (struct net_device *)dev_id;",
"source node": 841,
"start line": 608,
"target node": 842,
"thread": 2
},
{
"enter": 18,
"file": 5,
"source": "smc = (struct s_smc *)netdev_priv((struct net_device const *)dev);",
"source node": 842,
"start line": 612,
"target node": 843,
"thread": 2
},
{
"file": 24,
"return": 18,
"source": "return (void *)((char *)dev + 3200UL);",
"source node": 843,
"start line": 1605,
"target node": 844,
"thread": 2
},
{
"file": 5,
"source": "bp = &smc->os;",
"source node": 844,
"start line": 613,
"target node": 845,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "ioread32(smc->hw.iop + 12UL) != 0U",
"source node": 845,
"start line": 616,
"target node": 846,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "(((u_long)ioread32(smc->hw.iop + 8UL)) &(smc->hw.is_imask)) != 0UL",
"source node": 846,
"start line": 621,
"target node": 847,
"thread": 2
},
{
"file": 5,
"source": "iowrite32(0U, smc->hw.iop + 12UL);",
"source node": 847,
"start line": 625,
"target node": 848,
"thread": 2
},
{
"enter": 54,
"file": 5,
"source": "spin_lock(&bp->DriverLock);",
"source node": 848,
"start line": 626,
"target node": 849,
"thread": 2
},
{
"file": 26,
"source": "_raw_spin_lock(&lock->__annonCompField19.rlock);",
"source node": 849,
"start line": 303,
"target node": 850,
"thread": 2
},
{
"file": 26,
"return": 54,
"source": "return;",
"source node": 850,
"start line": 304,
"target node": 851,
"thread": 2
},
{
"enter": 55,
"file": 5,
"source": "fddi_isr(smc);",
"source node": 851,
"start line": 629,
"target node": 852,
"thread": 2
},
{
"file": 29,
"source": "u_long is;",
"source node": 852,
"start line": 711,
"target node": 853,
"thread": 2
},
{
"file": 29,
"source": "u_short stu;",
"source node": 853,
"start line": 712,
"target node": 854,
"thread": 2
},
{
"file": 29,
"source": "u_short stl;",
"source node": 854,
"start line": 713,
"target node": 855,
"thread": 2
},
{
"file": 29,
"source": "Mbuf *mb;",
"source node": 855,
"start line": 714,
"target node": 856,
"thread": 2
},
{
"file": 29,
"source": "smc->os.hwm.isr_flag = 1;",
"source node": 856,
"start line": 732,
"target node": 857,
"thread": 2
},
{
"file": 29,
"source": "is = (u_long)ioread32(smc->hw.iop + 8UL) &8368179UL;",
"source node": 857,
"start line": 742,
"target node": 858,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "is != 0UL",
"source node": 858,
"start line": 742,
"target node": 859,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(is &8359953UL) != 0UL",
"source node": 859,
"start line": 746,
"target node": 860,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(is &1048576UL) == 0UL",
"source node": 860,
"start line": 748,
"target node": 861,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(is &524288UL) == 0UL",
"source node": 861,
"start line": 751,
"target node": 862,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(is &65536UL) != 0UL",
"source node": 862,
"start line": 754,
"target node": 863,
"thread": 2
},
{
"file": 29,
"source": "stu = (u_short)ioread16(smc->hw.iop + 1024UL);",
"source node": 863,
"start line": 755,
"target node": 864,
"thread": 2
},
{
"file": 29,
"source": "stl = (u_short)ioread16(smc->hw.iop + 1028UL);",
"source node": 864,
"start line": 756,
"target node": 865,
"thread": 2
},
{
"enter": 56,
"file": 29,
"source": "mac1_irq(smc, (int)stu, (int)stl);",
"source node": 865,
"start line": 758,
"target node": 866,
"thread": 2
},
{
"file": 16,
"source": "int restart_tx;",
"source node": 866,
"start line": 188,
"target node": 867,
"thread": 2
},
{
"assumption": "restart_tx == 0;",
"assumption scope": 56,
"file": 16,
"source": "restart_tx = 0;",
"source node": 867,
"start line": 188,
"target node": 868,
"thread": 2
},
{
"condition": true,
"file": 16,
"source": "(((int)stl) &1792) != 0",
"source node": 868,
"start line": 194,
"target node": 869,
"thread": 2
},
{
"file": 16,
"source": "printk(\"\\016SMT PANIC: code: %d, msg: %s\\n\", 134, (char *)\"ST1L.FM_SPCEPDx parity error\");",
"source node": 869,
"start line": 197,
"target node": 870,
"thread": 2
},
{
"condition": true,
"file": 16,
"source": "(((int)stl) &28672) != 0",
"source node": 870,
"start line": 202,
"target node": 871,
"thread": 2
},
{
"file": 16,
"source": "printk(\"\\016SMT PANIC: code: %d, msg: %s\\n\", 133, (char *)\"ST1L.FM_STBURx tx buffer underrun\");",
"source node": 871,
"start line": 205,
"target node": 872,
"thread": 2
},
{
"condition": true,
"file": 16,
"source": "(((int)stu) &38912) == 0",
"source node": 872,
"start line": 208,
"target node": 873,
"thread": 2
},
{
"condition": true,
"file": 16,
"source": "(((int)stl) &3) == 0",
"source node": 873,
"start line": 208,
"target node": 874,
"thread": 2
},
{
"condition": true,
"file": 16,
"source": "(((int)stu) &3) != 0",
"source node": 874,
"start line": 222,
"target node": 875,
"thread": 2
},
{
"assumption": "restart_tx == 1;",
"assumption scope": 56,
"file": 16,
"source": "restart_tx = 1;",
"source node": 875,
"start line": 224,
"target node": 876,
"thread": 2
},
{
"condition": true,
"file": 16,
"source": "restart_tx != 0",
"source node": 876,
"start line": 227,
"target node": 877,
"thread": 2
},
{
"enter": 57,
"file": 16,
"source": "llc_restart_tx(smc);",
"source node": 877,
"start line": 228,
"target node": 878,
"thread": 2
},
{
"file": 5,
"source": "skfddi_priv *bp;",
"source node": 878,
"start line": 1278,
"target node": 879,
"thread": 2
},
{
"file": 5,
"source": "struct _ddebug descriptor;",
"source node": 879,
"start line": 1279,
"target node": 880,
"thread": 2
},
{
"file": 5,
"source": "bp = &smc->os;",
"source node": 880,
"start line": 1278,
"target node": 881,
"thread": 2
},
{
"file": 5,
"source": "descriptor.modname = \"skfp\";",
"source node": 881,
"start line": 1280,
"target node": 882,
"thread": 2
},
{
"file": 5,
"source": "descriptor.function = \"llc_restart_tx\";",
"source node": 882,
"start line": 1280,
"target node": 883,
"thread": 2
},
{
"file": 5,
"source": "descriptor.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 883,
"start line": 1280,
"target node": 884,
"thread": 2
},
{
"file": 5,
"source": "descriptor.format = \"[llc_restart_tx]\\n\";",
"source node": 884,
"start line": 1280,
"target node": 885,
"thread": 2
},
{
"file": 5,
"source": "descriptor.lineno = 1280U;",
"source node": 885,
"start line": 1280,
"target node": 886,
"thread": 2
},
{
"file": 5,
"source": "descriptor.flags = 0U;",
"source node": 886,
"start line": 1280,
"target node": 887,
"thread": 2
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor.flags &1L, 0L) != 0L",
"source node": 887,
"start line": 1280,
"target node": 888,
"thread": 2
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 888,
"start line": 26,
"target node": 889,
"thread": 2
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor, \"[llc_restart_tx]\\n\");",
"source node": 889,
"start line": 1280,
"target node": 890,
"thread": 2
},
{
"enter": 58,
"file": 5,
"source": "spin_unlock(&bp->DriverLock);",
"source node": 890,
"start line": 1283,
"target node": 891,
"thread": 2
},
{
"file": 26,
"source": "_raw_spin_unlock(&lock->__annonCompField19.rlock);",
"source node": 891,
"start line": 343,
"target node": 892,
"thread": 2
},
{
"file": 26,
"return": 58,
"source": "return;",
"source node": 892,
"start line": 344,
"target node": 893,
"thread": 2
},
{
"enter": 59,
"file": 5,
"source": "send_queued_packets(smc);",
"source node": 893,
"start line": 1284,
"target node": 894,
"thread": 2
},
{
"file": 5,
"source": "skfddi_priv *bp;",
"source node": 894,
"start line": 1106,
"target node": 895,
"thread": 2
},
{
"file": 5,
"source": "struct sk_buff *skb;",
"source node": 895,
"start line": 1107,
"target node": 896,
"thread": 2
},
{
"file": 5,
"source": "unsigned char fc;",
"source node": 896,
"start line": 1108,
"target node": 897,
"thread": 2
},
{
"file": 5,
"source": "int queue;",
"source node": 897,
"start line": 1109,
"target node": 898,
"thread": 2
},
{
"file": 5,
"source": "struct s_smt_fp_txd *txd;",
"source node": 898,
"start line": 1110,
"target node": 899,
"thread": 2
},
{
"file": 5,
"source": "dma_addr_t dma_address;",
"source node": 899,
"start line": 1111,
"target node": 900,
"thread": 2
},
{
"file": 5,
"source": "unsigned long Flags;",
"source node": 900,
"start line": 1112,
"target node": 901,
"thread": 2
},
{
"file": 5,
"source": "int frame_status;",
"source node": 901,
"start line": 1113,
"target node": 902,
"thread": 2
},
{
"file": 5,
"source": "struct _ddebug descriptor;",
"source node": 902,
"start line": 1114,
"target node": 903,
"thread": 2
},
{
"file": 5,
"source": "struct _ddebug descriptor___0;",
"source node": 903,
"start line": 1116,
"target node": 904,
"thread": 2
},
{
"file": 5,
"source": "struct _ddebug descriptor___1;",
"source node": 904,
"start line": 1119,
"target node": 905,
"thread": 2
},
{
"file": 5,
"source": "struct _ddebug descriptor___2;",
"source node": 905,
"start line": 1121,
"target node": 906,
"thread": 2
},
{
"file": 5,
"source": "struct _ddebug descriptor___3;",
"source node": 906,
"start line": 1123,
"target node": 907,
"thread": 2
},
{
"file": 5,
"source": "bp = &smc->os;",
"source node": 907,
"start line": 1106,
"target node": 908,
"thread": 2
},
{
"file": 5,
"source": "descriptor.modname = \"skfp\";",
"source node": 908,
"start line": 1116,
"target node": 909,
"thread": 2
},
{
"file": 5,
"source": "descriptor.function = \"send_queued_packets\";",
"source node": 909,
"start line": 1116,
"target node": 910,
"thread": 2
},
{
"file": 5,
"source": "descriptor.filename = \"drivers/net/fddi/skfp/skfddi.c\";",
"source node": 910,
"start line": 1116,
"target node": 911,
"thread": 2
},
{
"file": 5,
"source": "descriptor.format = \"send queued packets\\n\";",
"source node": 911,
"start line": 1116,
"target node": 912,
"thread": 2
},
{
"file": 5,
"source": "descriptor.lineno = 1116U;",
"source node": 912,
"start line": 1116,
"target node": 913,
"thread": 2
},
{
"file": 5,
"source": "descriptor.flags = 0U;",
"source node": 913,
"start line": 1116,
"target node": 914,
"thread": 2
},
{
"condition": true,
"enter": 16,
"file": 5,
"source": "__builtin_expect((long)descriptor.flags &1L, 0L) != 0L",
"source node": 914,
"start line": 1116,
"target node": 915,
"thread": 2
},
{
"file": 22,
"return": 16,
"source": "return exp;",
"source node": 915,
"start line": 26,
"target node": 916,
"thread": 2
},
{
"file": 5,
"source": "__dynamic_pr_debug(&descriptor, \"send queued packets\\n\");",
"source node": 916,
"start line": 1116,
"target node": 917,
"thread": 2
},
{
"file": 5,
"source": "skb = skb_dequeue(&bp->SendSkbQueue);",
"source node": 917,
"start line": 1119,
"target node": 918,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "((unsigned long)skb) != ((unsigned long)((struct sk_buff *)0))",
"source node": 918,
"start line": 1121,
"target node": 919,
"thread": 2
},
{
"enter": 20,
"file": 5,
"source": "Flags = _raw_spin_lock_irqsave(spinlock_check(&bp->DriverLock));",
"source node": 919,
"start line": 1126,
"target node": 920,
"thread": 2
},
{
"file": 26,
"return": 20,
"source": "return &lock->__annonCompField19.rlock;",
"source node": 920,
"start line": 292,
"target node": 921,
"thread": 2
},
{
"file": 5,
"source": "fc = *(skb->data);",
"source node": 921,
"start line": 1127,
"target node": 922,
"thread": 2
},
{
"file": 5,
"source": "queue = (int)((signed char)fc) >= 0;",
"source node": 922,
"start line": 1128,
"target node": 923,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "(((int)fc) &-136) == 80",
"source node": 923,
"start line": 1132,
"target node": 924,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "((unsigned int)(smc->ess.sync_bw_available)) == 0U",
"source node": 924,
"start line": 1134,
"target node": 925,
"thread": 2
},
{
"file": 5,
"source": "fc = (unsigned int)fc &127U;",
"source node": 925,
"start line": 1135,
"target node": 926,
"thread": 2
},
{
"enter": 60,
"file": 5,
"source": "frame_status = hwm_tx_init(smc, (int)fc, 1, (int)skb->len, queue);",
"source node": 926,
"start line": 1146,
"target node": 927,
"thread": 2
},
{
"file": 29,
"source": "smc->os.hwm.tx_p = smc->hw.fp.tx[frame_status &1];",
"source node": 927,
"start line": 1554,
"target node": 928,
"thread": 2
},
{
"file": 29,
"source": "smc->os.hwm.tx_descr = (((unsigned long)(frame_len + -1) &3UL) << 27) | 1073741824UL;",
"source node": 928,
"start line": 1555,
"target node": 929,
"thread": 2
},
{
"file": 29,
"source": "smc->os.hwm.tx_len = frame_len;",
"source node": 929,
"start line": 1556,
"target node": 930,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(((int)fc) &-136) == 80",
"source node": 930,
"start line": 1558,
"target node": 931,
"thread": 2
},
{
"file": 29,
"source": "frame_status = frame_status | 32;",
"source node": 931,
"start line": 1559,
"target node": 932,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "((unsigned int)(smc->hw.mac_ring_is_up)) == 0U",
"source node": 932,
"start line": 1577,
"target node": 933,
"thread": 2
},
{
"file": 29,
"source": "frame_status = frame_status &-33;",
"source node": 933,
"start line": 1578,
"target node": 934,
"thread": 2
},
{
"file": 29,
"source": "frame_status = frame_status | 64;",
"source node": 934,
"start line": 1579,
"target node": 935,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "frag_count <= __CPAchecker_TMP_0",
"source node": 935,
"start line": 1582,
"target node": 936,
"thread": 2
},
{
"file": 29,
"return": 60,
"source": "return frame_status;",
"source node": 936,
"start line": 1598,
"target node": 937,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "(frame_status &36) != 0",
"source node": 937,
"start line": 1148,
"target node": 938,
"thread": 2
},
{
"file": 5,
"source": "bp->QueueSkb = bp->QueueSkb + 1UL;",
"source node": 938,
"start line": 1169,
"target node": 939,
"thread": 2
},
{
"enter": 61,
"file": 5,
"source": "CheckSourceAddress(skb->data, (unsigned char *)(&smc->hw.fddi_canon_addr.a));",
"source node": 939,
"start line": 1172,
"target node": 940,
"thread": 2
},
{
"file": 5,
"source": "unsigned char SRBit;",
"source node": 940,
"start line": 1207,
"target node": 941,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "(((unsigned long)(*(frame + 7UL))) &18446744073709551614UL) == 0UL",
"source node": 941,
"start line": 1209,
"target node": 942,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "((unsigned int)(*(frame + 11UL))) == 0U",
"source node": 942,
"start line": 1212,
"target node": 943,
"thread": 2
},
{
"file": 5,
"source": "SRBit = (unsigned int)*(frame + 7UL) &1U;",
"source node": 943,
"start line": 1214,
"target node": 944,
"thread": 2
},
{
"file": 5,
"source": "memcpy((void *)(frame + 7UL), (void const *)hw_addr, 6UL);",
"source node": 944,
"start line": 1215,
"target node": 945,
"thread": 2
},
{
"file": 5,
"source": "*(frame + 8UL) = (int)*(frame + 8UL) | (int)SRBit;",
"source node": 945,
"start line": 1216,
"target node": 946,
"thread": 2
},
{
"file": 5,
"return": 61,
"source": "return;",
"source node": 946,
"start line": 1217,
"target node": 947,
"thread": 2
},
{
"file": 5,
"source": "txd = (struct s_smt_fp_txd *)smc->hw.fp.tx_q[queue].tx_curr_put;",
"source node": 947,
"start line": 1174,
"target node": 948,
"thread": 2
},
{
"enter": 62,
"file": 5,
"source": "dma_address = pci_map_single(&bp->pdev, (void *)skb->data, (size_t)skb->len, 1);",
"source node": 948,
"start line": 1176,
"target node": 949,
"thread": 2
},
{
"condition": true,
"file": 27,
"source": "((unsigned long)hwdev) == ((unsigned long)((struct pci_dev *)0))",
"source node": 949,
"start line": 32,
"target node": 950,
"thread": 2
},
{
"file": 27,
"source": "(struct device *)0",
"source node": 950,
"start line": 32,
"target node": 951,
"thread": 2
},
{
"enter": 63,
"file": 27,
"return": 62,
"source": "return dma_map_single_attrs((unsigned long)hwdev != (unsigned long)((struct pci_dev *)0) ? &hwdev->dev : (struct device *)0, ptr, size, (enum dma_data_direction)direction, (struct dma_attrs *)0);",
"source node": 951,
"start line": 32,
"target node": 952,
"thread": 2
},
{
"enter": 64,
"file": 0,
"note": "Map page",
"source": "ldv_dma_map_single_attrs();",
"source node": 952,
"start line": 1007,
"target node": 953,
"thread": 2
},
{
"enter": 65,
"file": 18,
"note": "Check that previous dma_mapping call was checked",
"source": "ldv_assert_linux_drivers_base_dma_mapping__double_map(ldv_dma_calls == 0);",
"source node": 953,
"start line": 49,
"target node": 954,
"thread": 2
},
{
"assumption": "expr == 1;",
"assumption scope": 65,
"condition": true,
"file": 31,
"source": "expr != 0",
"source node": 954,
"start line": 4,
"target node": 955,
"thread": 2
},
{
"file": 31,
"return": 65,
"source": "return;",
"source node": 955,
"start line": 6,
"target node": 956,
"thread": 2
},
{
"assumption": "ldv_dma_calls == 1;",
"assumption scope": 64,
"file": 18,
"note": "Increase map counter",
"source": "ldv_dma_calls = ldv_dma_calls + 1;",
"source node": 956,
"start line": 51,
"target node": 957,
"thread": 2
},
{
"file": 18,
"return": 64,
"source": "return;",
"source node": 957,
"start line": 52,
"target node": 958,
"thread": 2
},
{
"enter": 10,
"file": 0,
"return": 63,
"source": "return (dma_addr_t)ldv_undef_int();",
"source node": 958,
"start line": 1008,
"target node": 959,
"thread": 2
},
{
"file": 21,
"return": 10,
"source": "return __VERIFIER_nondet_int();",
"source node": 959,
"start line": 41,
"target node": 960,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "(frame_status &32) != 0",
"source node": 960,
"start line": 1178,
"target node": 961,
"thread": 2
},
{
"file": 5,
"source": "txd->txd_os.skb = skb;",
"source node": 961,
"start line": 1179,
"target node": 962,
"thread": 2
},
{
"file": 5,
"source": "txd->txd_os.dma_addr = dma_address;",
"source node": 962,
"start line": 1180,
"target node": 963,
"thread": 2
},
{
"enter": 66,
"file": 5,
"source": "hwm_tx_frag(smc, (char *)skb->data, (u_long)dma_address, (int)skb->len, frame_status | 26);",
"source node": 963,
"start line": 1182,
"target node": 964,
"thread": 2
},
{
"file": 29,
"source": "struct s_smt_fp_txd volatile *t;",
"source node": 964,
"start line": 1630,
"target node": 965,
"thread": 2
},
{
"file": 29,
"source": "struct s_smt_tx_queue *queue;",
"source node": 965,
"start line": 1631,
"target node": 966,
"thread": 2
},
{
"file": 29,
"source": "__le32 tbctrl;",
"source node": 966,
"start line": 1632,
"target node": 967,
"thread": 2
},
{
"file": 29,
"source": "queue = smc->os.hwm.tx_p;",
"source node": 967,
"start line": 1635,
"target node": 968,
"thread": 2
},
{
"file": 29,
"source": "t = queue->tx_curr_put;",
"source node": 968,
"start line": 1643,
"target node": 969,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(frame_status &32) != 0",
"source node": 969,
"start line": 1646,
"target node": 970,
"thread": 2
},
{
"file": 29,
"source": "t->txd_virt = virt;",
"source node": 970,
"start line": 1649,
"target node": 971,
"thread": 2
},
{
"file": 29,
"source": "t->txd_txdscr = (unsigned int)smc->os.hwm.tx_descr;",
"source node": 971,
"start line": 1650,
"target node": 972,
"thread": 2
},
{
"file": 29,
"source": "t->txd_tbadr = (unsigned int)phys;",
"source node": 972,
"start line": 1651,
"target node": 973,
"thread": 2
},
{
"file": 29,
"source": "tbctrl = ((((unsigned int)frame_status &26U) << 26) | (unsigned int)len) | 2153054208U;",
"source node": 973,
"start line": 1652,
"target node": 974,
"thread": 2
},
{
"file": 29,
"source": "t->txd_tbctrl = tbctrl;",
"source node": 974,
"start line": 1655,
"target node": 975,
"thread": 2
},
{
"file": 29,
"source": "iowrite32(16U, queue->tx_bmu_ctl);",
"source node": 975,
"start line": 1659,
"target node": 976,
"thread": 2
},
{
"file": 29,
"source": "queue->tx_free = (u_short)((int)queue->tx_free - 1);",
"source node": 976,
"start line": 1669,
"target node": 977,
"thread": 2
},
{
"file": 29,
"source": "queue->tx_used = (u_short)((int)queue->tx_used + 1);",
"source node": 977,
"start line": 1670,
"target node": 978,
"thread": 2
},
{
"file": 29,
"source": "queue->tx_curr_put = t->txd_next;",
"source node": 978,
"start line": 1671,
"target node": 979,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(frame_status &8) != 0",
"source node": 979,
"start line": 1672,
"target node": 980,
"thread": 2
},
{
"file": 29,
"source": "smc->mib.m[0].fddiMACTransmit_Ct = smc->mib.m[0].fddiMACTransmit_Ct + 1UL;",
"source node": 980,
"start line": 1673,
"target node": 981,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(frame_status &4) != 0",
"source node": 981,
"start line": 1676,
"target node": 982,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(frame_status &16) == 0",
"source node": 982,
"start line": 1678,
"target node": 983,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "((unsigned long)(smc->os.hwm.tx_mb)) != ((unsigned long)((Mbuf *)0))",
"source node": 983,
"start line": 1694,
"target node": 984,
"thread": 2
},
{
"file": 29,
"source": "memcpy((void *)smc->os.hwm.tx_data, (void const *)virt, (size_t)len);",
"source node": 984,
"start line": 1697,
"target node": 985,
"thread": 2
},
{
"file": 29,
"source": "smc->os.hwm.tx_data = smc->os.hwm.tx_data + (unsigned long)len;",
"source node": 985,
"start line": 1698,
"target node": 986,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(frame_status &8) == 0",
"source node": 986,
"start line": 1700,
"target node": 987,
"thread": 2
},
{
"file": 29,
"return": 66,
"source": "return;",
"source node": 987,
"start line": 1726,
"target node": 988,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "(frame_status &32) != 0",
"source node": 988,
"start line": 1185,
"target node": 989,
"thread": 2
},
{
"enter": 67,
"file": 5,
"source": "spin_unlock_irqrestore(&bp->DriverLock, Flags);",
"source node": 989,
"start line": 1190,
"target node": 990,
"thread": 2
},
{
"file": 26,
"source": "_raw_spin_unlock_irqrestore(&lock->__annonCompField19.rlock, flags);",
"source node": 990,
"start line": 358,
"target node": 991,
"thread": 2
},
{
"file": 26,
"return": 67,
"source": "return;",
"source node": 991,
"start line": 359,
"target node": 992,
"thread": 2
},
{
"file": 5,
"source": "skb = skb_dequeue(&bp->SendSkbQueue);",
"source node": 992,
"start line": 1119,
"target node": 993,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "((unsigned long)skb) != ((unsigned long)((struct sk_buff *)0))",
"source node": 993,
"start line": 1121,
"target node": 994,
"thread": 2
},
{
"enter": 20,
"file": 5,
"source": "Flags = _raw_spin_lock_irqsave(spinlock_check(&bp->DriverLock));",
"source node": 994,
"start line": 1126,
"target node": 995,
"thread": 2
},
{
"file": 26,
"return": 20,
"source": "return &lock->__annonCompField19.rlock;",
"source node": 995,
"start line": 292,
"target node": 996,
"thread": 2
},
{
"file": 5,
"source": "fc = *(skb->data);",
"source node": 996,
"start line": 1127,
"target node": 997,
"thread": 2
},
{
"file": 5,
"source": "queue = (int)((signed char)fc) >= 0;",
"source node": 997,
"start line": 1128,
"target node": 998,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "(((int)fc) &-136) == 80",
"source node": 998,
"start line": 1132,
"target node": 999,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "((unsigned int)(smc->ess.sync_bw_available)) == 0U",
"source node": 999,
"start line": 1134,
"target node": 1000,
"thread": 2
},
{
"file": 5,
"source": "fc = (unsigned int)fc &127U;",
"source node": 1000,
"start line": 1135,
"target node": 1001,
"thread": 2
},
{
"enter": 60,
"file": 5,
"source": "frame_status = hwm_tx_init(smc, (int)fc, 1, (int)skb->len, queue);",
"source node": 1001,
"start line": 1146,
"target node": 1002,
"thread": 2
},
{
"file": 29,
"source": "smc->os.hwm.tx_p = smc->hw.fp.tx[frame_status &1];",
"source node": 1002,
"start line": 1554,
"target node": 1003,
"thread": 2
},
{
"file": 29,
"source": "smc->os.hwm.tx_descr = (((unsigned long)(frame_len + -1) &3UL) << 27) | 1073741824UL;",
"source node": 1003,
"start line": 1555,
"target node": 1004,
"thread": 2
},
{
"file": 29,
"source": "smc->os.hwm.tx_len = frame_len;",
"source node": 1004,
"start line": 1556,
"target node": 1005,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "(((int)fc) &-136) == 80",
"source node": 1005,
"start line": 1558,
"target node": 1006,
"thread": 2
},
{
"file": 29,
"source": "frame_status = frame_status | 32;",
"source node": 1006,
"start line": 1559,
"target node": 1007,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "((unsigned int)(smc->hw.mac_ring_is_up)) == 0U",
"source node": 1007,
"start line": 1577,
"target node": 1008,
"thread": 2
},
{
"file": 29,
"source": "frame_status = frame_status &-33;",
"source node": 1008,
"start line": 1578,
"target node": 1009,
"thread": 2
},
{
"file": 29,
"source": "frame_status = frame_status | 64;",
"source node": 1009,
"start line": 1579,
"target node": 1010,
"thread": 2
},
{
"condition": true,
"file": 29,
"source": "frag_count <= __CPAchecker_TMP_0",
"source node": 1010,
"start line": 1582,
"target node": 1011,
"thread": 2
},
{
"file": 29,
"return": 60,
"source": "return frame_status;",
"source node": 1011,
"start line": 1598,
"target node": 1012,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "(frame_status &36) != 0",
"source node": 1012,
"start line": 1148,
"target node": 1013,
"thread": 2
},
{
"file": 5,
"source": "bp->QueueSkb = bp->QueueSkb + 1UL;",
"source node": 1013,
"start line": 1169,
"target node": 1014,
"thread": 2
},
{
"enter": 61,
"file": 5,
"source": "CheckSourceAddress(skb->data, (unsigned char *)(&smc->hw.fddi_canon_addr.a));",
"source node": 1014,
"start line": 1172,
"target node": 1015,
"thread": 2
},
{
"file": 5,
"source": "unsigned char SRBit;",
"source node": 1015,
"start line": 1207,
"target node": 1016,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "(((unsigned long)(*(frame + 7UL))) &18446744073709551614UL) == 0UL",
"source node": 1016,
"start line": 1209,
"target node": 1017,
"thread": 2
},
{
"condition": true,
"file": 5,
"source": "((unsigned int)(*(frame + 11UL))) == 0U",
"source node": 1017,
"start line": 1212,
"target node": 1018,
"thread": 2
},
{
"file": 5,
"source": "SRBit = (unsigned int)*(frame + 7UL) &1U;",
"source node": 1018,
"start line": 1214,
"target node": 1019,
"thread": 2
},
{
"file": 5,
"source": "memcpy((void *)(frame + 7UL), (void const *)hw_addr, 6UL);",
"source node": 1019,
"start line": 1215,
"target node": 1020,
"thread": 2
},
{
"file": 5,
"source": "*(frame + 8UL) = (int)*(frame + 8UL) | (int)SRBit;",
"source node": 1020,
"start line": 1216,
"target node": 1021,
"thread": 2
},
{
"file": 5,
"return": 61,
"source": "return;",
"source node": 1021,
"start line": 1217,
"target node": 1022,
"thread": 2
},
{
"file": 5,
"source": "txd = (struct s_smt_fp_txd *)smc->hw.fp.tx_q[queue].tx_curr_put;",
"source node": 1022,
"start line": 1174,
"target node": 1023,
"thread": 2
},
{
"enter": 62,
"file": 5,
"source": "dma_address = pci_map_single(&bp->pdev, (void *)skb->data, (size_t)skb->len, 1);",
"source node": 1023,
"start line": 1176,
"target node": 1024,
"thread": 2
},
{
"condition": true,
"file": 27,
"source": "((unsigned long)hwdev) == ((unsigned long)((struct pci_dev *)0))",
"source node": 1024,
"start line": 32,
"target node": 1025,
"thread": 2
},
{
"file": 27,
"source": "(struct device *)0",
"source node": 1025,
"start line": 32,
"target node": 1026,
"thread": 2
},
{
"enter": 64,
"file": 27,
"source": "ldv_dma_map_single_attrs();",
"source node": 1026,
"start line": 32,
"target node": 1027,
"thread": 2,
"warn": "Check that previous dma_mapping call was checked"
},
{
"enter": 65,
"file": 18,
"note": "Check that previous dma_mapping call was checked",
"source": "ldv_assert_linux_drivers_base_dma_mapping__double_map(ldv_dma_calls == 0);",
"source node": 1027,
"start line": 49,
"target node": 1028,
"thread": 2
},
{
"assumption": "expr == 0;",
"assumption scope": 65,
"condition": true,
"file": 31,
"source": "expr == 0",
"source node": 1028,
"start line": 4,
"target node": 1029,
"thread": 2
},
{
"file": 31,
"source": "__VERIFIER_error();",
"source node": 1029,
"start line": 5,
"target node": 1030,
"thread": 2
}
],
"entry node": 0,
"files": [
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/avtg/drivers/net/fddi/skfp/skfp.ko/linux:drivers:base:dma-mapping/weaver/.tmp_skfddi.c.aux",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/include/linux/export.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/arch/x86/include/asm/paravirt_types.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/include/linux/jiffies.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/arch/x86/include/asm/dma-mapping.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/skfddi.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/h/smc.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/include/linux/bitrev.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/fplustm.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/smt.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/cfm.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/pcmplc.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/pmf.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/smtdef.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/smtinit.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/srf.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/drvfbi.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/ess.c",
"/work/ssd/klever/linux/drivers/base/dma-mapping.c",
"/work/ssd/klever/verifier/memory.c",
"/work/ssd/klever/linux/err.c",
"/work/ssd/klever/verifier/nondet.c",
"/work/ssd/klever/verifier/gcc.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/arch/x86/include/asm/io.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/include/linux/netdevice.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/include/linux/skbuff.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/include/linux/spinlock.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/include/asm-generic/pci-dma-compat.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/include/linux/dma-mapping.h",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/hwmtm.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/lkbce/drivers/net/fddi/skfp/hwt.c",
"/work/ssd/klever/native-scheduler-work-dir/scheduler/jobs/e1054498015c315dd878acc077f1bb9c/klever-core-work-dir/drivers/net/fddi/skfp/skfp.ko/linux-drivers-base-dma-mapping/vtg/drivers/net/fddi/skfp/skfp.ko/linux:drivers:base:dma-mapping/rsb/bug kind funcs.c"
],
"funcs": [
"ldv_main_13",
"ldv_dispatch_insmod_register_13_3",
"ldv_xmalloc",
"ldv_is_err",
"ldv_insmod_5",
"ldv_free",
"ldv_insmod_skfddi_pci_driver_init_5_6",
"skfddi_pci_driver_init",
"ldv___pci_register_driver_18",
"ldv_emg___pci_register_driver",
"ldv_undef_int",
"ldv_dispatch_register_12_3",
"ldv_pci_scenario_4",
"ldv_xmalloc_unknown_size",
"ldv_pci_scenario_probe_4_17",
"skfp_init_one",
"__builtin_expect",
"ioremap",
"netdev_priv",
"skb_queue_head_init",
"spinlock_check",
"__skb_queue_head_init",
"skfp_driver_init",
"pci_alloc_consistent",
"dma_alloc_attrs",
"get_dma_ops",
"is_device_dma_capable",
"dma_alloc_coherent_gfp_flags",
"dma_alloc_coherent_mask",
"mac_drv_check_space",
"card_stop",
"smt_stop_watchdog",
"hwt_quick_read",
"hwt_wait_time",
"mac_drv_init",
"mac_drv_get_desc_mem",
"mac_drv_get_space",
"read_address",
"bitrev8",
"smt_reset_defaults",
"smt_init_mib",
"smt_set_mac_opvalues",
"set_min_max",
"smt_get_time",
"ldv_register_netdev_12",
"ldv_emg_register_netdev",
"ldv_register_netdev_open_8_6",
"skfp_open",
"ldv_request_irq_16",
"ldv_emg_request_irq",
"ldv_dispatch_irq_register_9_3",
"ldv_interrupt_scenario_2",
"ldv_interrupt_scenario_handler_2_5",
"skfp_interrupt",
"spin_lock",
"fddi_isr",
"mac1_irq",
"llc_restart_tx",
"spin_unlock",
"send_queued_packets",
"hwm_tx_init",
"CheckSourceAddress",
"pci_map_single",
"dma_map_single_attrs",
"ldv_dma_map_single_attrs",
"ldv_assert_linux_drivers_base_dma_mapping__double_map",
"hwm_tx_frag",
"spin_unlock_irqrestore",
"ldv_dispatch_deregister_10_1",
"ldv_dispatch_deregister_11_1",
"ldv_dispatch_insmod_deregister_13_2",
"ldv_dispatch_irq_deregister_6_1",
"ldv_dispatch_register_8_4",
"ldv_emg_free_irq",
"ldv_emg_free_netdev",
"ldv_emg_pci_unregister_driver",
"ldv_emg_unregister_netdev",
"ldv_insmod_skfddi_pci_driver_exit_5_2",
"ldv_interrupt_scenario_thread_2_3",
"ldv_pci_scenario_release_4_2",
"ldv_pci_scenario_resume_4_5",
"ldv_pci_scenario_resume_early_4_6",
"ldv_pci_scenario_shutdown_4_3",
"ldv_pci_scenario_suspend_4_8",
"ldv_pci_scenario_suspend_late_4_7",
"ldv_random_allocationless_scenario_3",
"ldv_random_allocationless_scenario_callback_3_11",
"ldv_random_allocationless_scenario_callback_3_12",
"ldv_random_allocationless_scenario_callback_3_15",
"ldv_random_allocationless_scenario_callback_3_16",
"ldv_random_allocationless_scenario_callback_3_3",
"ldv_random_allocationless_scenario_callback_3_8",
"ldv_unregister_netdev_stop_10_2",
"main",
"ERR_PTR",
"PTR_ERR",
"IS_ERR",
"IS_ERR_OR_NULL",
"kzalloc",
"dma_mapping_error",
"ldv_dma_map_page_8",
"ldv_dma_map_page_9",
"ldv_dev_get_drvdata_10",
"ldv_dev_set_drvdata_11",
"ldv_free_netdev_13",
"ldv_unregister_netdev_14",
"ldv_free_netdev_15",
"ldv_free_irq_17",
"ldv_pci_unregister_driver_19",
"ldv_dma_map_single",
"ldv_check_final_state"
],
"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,
588
],
[
588,
589
],
[
589,
590
],
[
590,
591
],
[
591,
592
],
[
592,
593
],
[
593,
594
],
[
594,
595
],
[
595,
596
],
[
596,
597
],
[
597,
598
],
[
598,
599
],
[
599,
600
],
[
600,
601
],
[
601,
602
],
[
602,
603
],
[
603,
604
],
[
604,
605
],
[
605,
606
],
[
606,
607
],
[
607,
608
],
[
608,
609
],
[
609,
610
],
[
610,
611
],
[
611,
612
],
[
612,
613
],
[
613,
614
],
[
614,
615
],
[
615,
616
],
[
616,
617
],
[
617,
618
],
[
618,
619
],
[
619,
620
],
[
620,
621
],
[
621,
622
],
[
622,
623
],
[
623,
624
],
[
624,
625
],
[
625,
626
],
[
626,
627
],
[
627,
628
],
[
628,
629
],
[
629,
630
],
[
630,
631
],
[
631,
632
],
[
632,
633
],
[
633,
634
],
[
634,
635
],
[
635,
636
],
[
636,
637
],
[
637,
638
],
[
638,
639
],
[
639,
640
],
[
640,
641
],
[
641,
642
],
[
642,
643
],
[
643,
644
],
[
644,
645
],
[
645,
646
],
[
646,
647
],
[
647,
648
],
[
648,
649
],
[
649,
650
],
[
650,
651
],
[
651,
652
],
[
652,
653
],
[
653,
654
],
[
654,
655
],
[
655,
656
],
[
656,
657
],
[
657,
658
],
[
658,
659
],
[
659,
660
],
[
660,
661
],
[
661,
662
],
[
662,
663
],
[
663,
664
],
[
664,
665
],
[
665,
666
],
[
666,
667
],
[
667,
668
],
[
668,
669
],
[
669,
670
],
[
670,
671
],
[
671,
672
],
[
672,
673
],
[
673,
674
],
[
674,
675
],
[
675,
676
],
[
676,
677
],
[
677,
678
],
[
678,
679
],
[
679,
680
],
[
680,
681
],
[
681,
682
],
[
682,
683
],
[
683,
684
],
[
684,
685
],
[
685,
686
],
[
686,
687
],
[
687,
688
],
[
688,
689
],
[
689,
690
],
[
690,
691
],
[
691,
692
],
[
692,
693
],
[
693,
694
],
[
694,
695
],
[
695,
696
],
[
696,
697
],
[
697,
698
],
[
698,
699
],
[
699,
700
],
[
700,
701
],
[
701,
702
],
[
702,
703
],
[
703,
704
],
[
704,
705
],
[
705,
706
],
[
706,
707
],
[
707,
708
],
[
708,
709
],
[
709,
710
],
[
710,
711
],
[
711,
712
],
[
712,
713
],
[
713,
714
],
[
714,
715
],
[
715,
716
],
[
716,
717
],
[
717,
718
],
[
718,
719
],
[
719,
720
],
[
720,
721
],
[
721,
722
],
[
722,
723
],
[
723,
724
],
[
724,
725
],
[
725,
726
],
[
726,
727
],
[
727,
728
],
[
728,
729
],
[
729,
730
],
[
730,
731
],
[
731,
732
],
[
732,
733
],
[
733,
734
],
[
734,
735
],
[
735,
736
],
[
736,
737
],
[
737,
738
],
[
738,
739
],
[
739,
740
],
[
740,
741
],
[
741,
742
],
[
742,
743
],
[
743,
744
],
[
744,
745
],
[
745,
746
],
[
746,
747
],
[
747,
748
],
[
748,
749
],
[
749,
750
],
[
750,
751
],
[
751,
752
],
[
752,
753
],
[
753,
754
],
[
754,
755
],
[
755,
756
],
[
756,
757
],
[
757,
758
],
[
758,
759
],
[
759,
760
],
[
760,
761
],
[
761,
762
],
[
762,
763
],
[
763,
764
],
[
764,
765
],
[
765,
766
],
[
766,
767
],
[
767,
768
],
[
768,
769
],
[
769,
770
],
[
770,
771
],
[
771,
772
],
[
772,
773
],
[
773,
774
],
[
774,
775
],
[
775,
776
],
[
776,
777
],
[
777,
778
],
[
778,
779
],
[
779,
780
],
[
780,
781
],
[
781,
782
],
[
782,
783
],
[
783,
784
],
[
784,
785
],
[
785,
786
],
[
786,
787
],
[
787,
788
],
[
788,
789
],
[
789,
790
],
[
790,
791
],
[
791,
792
],
[
792,
793
],
[
793,
794
],
[
794,
795
],
[
795,
796
],
[
796,
797
],
[
797,
798
],
[
798,
799
],
[
799,
800
],
[
800,
801
],
[
801,
802
],
[
802,
803
],
[
803,
804
],
[
804,
805
],
[
805,
806
],
[
806,
807
],
[
807,
808
],
[
808,
809
],
[
809,
810
],
[
810,
811
],
[
811,
812
],
[
812,
813
],
[
813,
814
],
[
814,
815
],
[
815,
816
],
[
816,
817
],
[
817,
818
],
[
818,
819
],
[
819,
820
],
[
820,
821
],
[
821,
822
],
[
822,
823
],
[
823,
824
],
[
824,
825
],
[
825,
826
],
[
826,
827
],
[
827,
828
],
[
828,
829
],
[
829,
830
],
[
830,
831
],
[
831,
832
],
[
832,
833
],
[
833,
834
],
[
834,
835
],
[
835,
836
],
[
836,
837
],
[
837,
838
],
[
838,
839
],
[
839,
840
],
[
840,
841
],
[
841,
842
],
[
842,
843
],
[
843,
844
],
[
844,
845
],
[
845,
846
],
[
846,
847
],
[
847,
848
],
[
848,
849
],
[
849,
850
],
[
850,
851
],
[
851,
852
],
[
852,
853
],
[
853,
854
],
[
854,
855
],
[
855,
856
],
[
856,
857
],
[
857,
858
],
[
858,
859
],
[
859,
860
],
[
860,
861
],
[
861,
862
],
[
862,
863
],
[
863,
864
],
[
864,
865
],
[
865,
866
],
[
866,
867
],
[
867,
868
],
[
868,
869
],
[
869,
870
],
[
870,
871
],
[
871,
872
],
[
872,
873
],
[
873,
874
],
[
874,
875
],
[
875,
876
],
[
876,
877
],
[
877,
878
],
[
878,
879
],
[
879,
880
],
[
880,
881
],
[
881,
882
],
[
882,
883
],
[
883,
884
],
[
884,
885
],
[
885,
886
],
[
886,
887
],
[
887,
888
],
[
888,
889
],
[
889,
890
],
[
890,
891
],
[
891,
892
],
[
892,
893
],
[
893,
894
],
[
894,
895
],
[
895,
896
],
[
896,
897
],
[
897,
898
],
[
898,
899
],
[
899,
900
],
[
900,
901
],
[
901,
902
],
[
902,
903
],
[
903,
904
],
[
904,
905
],
[
905,
906
],
[
906,
907
],
[
907,
908
],
[
908,
909
],
[
909,
910
],
[
910,
911
],
[
911,
912
],
[
912,
913
],
[
913,
914
],
[
914,
915
],
[
915,
916
],
[
916,
917
],
[
917,
918
],
[
918,
919
],
[
919,
920
],
[
920,
921
],
[
921,
922
],
[
922,
923
],
[
923,
924
],
[
924,
925
],
[
925,
926
],
[
926,
927
],
[
927,
928
],
[
928,
929
],
[
929,
930
],
[
930,
931
],
[
931,
932
],
[
932,
933
],
[
933,
934
],
[
934,
935
],
[
935,
936
],
[
936,
937
],
[
937,
938
],
[
938,
939
],
[
939,
940
],
[
940,
941
],
[
941,
942
],
[
942,
943
],
[
943,
944
],
[
944,
945
],
[
945,
946
],
[
946,
947
],
[
947,
948
],
[
948,
949
],
[
949,
950
],
[
950,
951
],
[
951,
952
],
[
952,
953
],
[
953,
954
],
[
954,
955
],
[
955,
956
],
[
956,
957
],
[
957,
958
],
[
958,
959
],
[
959,
960
],
[
960,
961
],
[
961,
962
],
[
962,
963
],
[
963,
964
],
[
964,
965
],
[
965,
966
],
[
966,
967
],
[
967,
968
],
[
968,
969
],
[
969,
970
],
[
970,
971
],
[
971,
972
],
[
972,
973
],
[
973,
974
],
[
974,
975
],
[
975,
976
],
[
976,
977
],
[
977,
978
],
[
978,
979
],
[
979,
980
],
[
980,
981
],
[
981,
982
],
[
982,
983
],
[
983,
984
],
[
984,
985
],
[
985,
986
],
[
986,
987
],
[
987,
988
],
[
988,
989
],
[
989,
990
],
[
990,
991
],
[
991,
992
],
[
992,
993
],
[
993,
994
],
[
994,
995
],
[
995,
996
],
[
996,
997
],
[
997,
998
],
[
998,
999
],
[
999,
1000
],
[
1000,
1001
],
[
1001,
1002
],
[
1002,
1003
],
[
1003,
1004
],
[
1004,
1005
],
[
1005,
1006
],
[
1006,
1007
],
[
1007,
1008
],
[
1008,
1009
],
[
1009,
1010
],
[
1010,
1011
],
[
1011,
1012
],
[
1012,
1013
],
[
1013,
1014
],
[
1014,
1015
],
[
1015,
1016
],
[
1016,
1017
],
[
1017,
1018
],
[
1018,
1019
],
[
1019,
1020
],
[
1020,
1021
],
[
1021,
1022
],
[
1022,
1023
],
[
1023,
1024
],
[
1024,
1025
],
[
1025,
1026
],
[
1026,
1027
],
[
1027,
1028
],
[
1028,
1029
],
[
1029,
null
]
],
"violation nodes": [
1030
]
}
(2-2/2)