Project

General

Profile

Download (55.9 KB)

Bug #8046 » error-trace(1).json

Evgeny Novikov, 03/21/2017 09:23 PM

 
{
"actions": [
"Initialize rule models.",
"Start environment model scenarios.",
"Declare auxiliary variables.",
"Trigger module initialization.",
"Initialize the module after insmod with 'esb_driver_init' function. Invoke callback esb_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.",
"Fail to register the miscellaneous character driver."
],
"callback actions": [
4,
10
],
"edges": [
{
"file": 1,
"source": "extern struct module __this_module;",
"source node": 0,
"start line": 33,
"target node": 1,
"thread": 0
},
{
"file": 2,
"source": "static void *BASEADDR;",
"source node": 1,
"start line": 79,
"target node": 2,
"thread": 0
},
{
"file": 2,
"source": "static spinlock_t esb_lock = {{{{{0U}}, 3735899821U, 4294967295U, (void *)-1, {0, {0, 0}, \"esb_lock\", 0, 0UL}}}};",
"source node": 2,
"start line": 80,
"target node": 3,
"thread": 0
},
{
"file": 2,
"source": "static unsigned long timer_alive;",
"source node": 3,
"start line": 81,
"target node": 4,
"thread": 0
},
{
"file": 2,
"source": "static struct pci_dev *esb_pci;",
"source node": 4,
"start line": 82,
"target node": 5,
"thread": 0
},
{
"file": 2,
"source": "static unsigned short triggered;",
"source node": 5,
"start line": 83,
"target node": 6,
"thread": 0
},
{
"file": 2,
"source": "static char esb_expect_close;",
"source node": 6,
"start line": 84,
"target node": 7,
"thread": 0
},
{
"file": 2,
"source": "static int cards_found;",
"source node": 7,
"start line": 87,
"target node": 8,
"thread": 0
},
{
"file": 2,
"source": "static int heartbeat = 30;",
"source node": 8,
"start line": 92,
"target node": 9,
"thread": 0
},
{
"file": 2,
"source": "static bool nowayout = 1;",
"source node": 9,
"start line": 98,
"target node": 10,
"thread": 0
},
{
"file": 2,
"source": "static struct file_operations const esb_fops = #line 319 {&__this_module, &no_llseek, 0, &esb_write, 0, 0, 0, 0, &esb_ioctl, 0, 0, &esb_open, 0, &esb_release, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0};",
"source node": 10,
"start line": 319,
"target node": 11,
"thread": 0
},
{
"file": 2,
"source": "static struct miscdevice esb_miscdev = #line 328 {130, \"watchdog\", &esb_fops, {0, 0}, 0, 0, 0, (unsigned short)0};",
"source node": 11,
"start line": 328,
"target node": 12,
"thread": 0
},
{
"file": 2,
"source": "static struct pci_device_id const esb_pci_tbl[2U] = { {32902U, 9643U, 4294967295U, 4294967295U, 0U, 0U, 0UL}, {0U, 0U, 0U, 0U, 0U, 0U, 0UL}};",
"source node": 12,
"start line": 337,
"target node": 13,
"thread": 0
},
{
"file": 2,
"source": "struct pci_device_id const __mod_pci_device_table;",
"source node": 13,
"start line": 341,
"target node": 14,
"thread": 0
},
{
"file": 2,
"source": "static struct pci_driver esb_driver = #line 487 {{0, 0}, \"i6300ESB timer\", (struct pci_device_id const *)(&esb_pci_tbl), &esb_probe, &esb_remove, 0, 0, 0, 0, &esb_shutdown, 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": 14,
"start line": 487,
"target node": 15,
"thread": 0
},
{
"file": 0,
"source": "struct ldv_thread ldv_thread_1;",
"source node": 15,
"start line": 84,
"target node": 16,
"thread": 0
},
{
"file": 0,
"source": "struct ldv_thread ldv_thread_2;",
"source node": 16,
"start line": 85,
"target node": 17,
"thread": 0
},
{
"file": 0,
"source": "struct ldv_thread ldv_thread_3;",
"source node": 17,
"start line": 86,
"target node": 18,
"thread": 0
},
{
"file": 0,
"source": "struct ldv_thread ldv_thread_8;",
"source node": 18,
"start line": 87,
"target node": 19,
"thread": 0
},
{
"file": 3,
"source": "int ldv_iomem = 0;",
"source node": 19,
"start line": 22,
"target node": 20,
"thread": 0
},
{
"enter": 0,
"file": 0,
"source": "ldv_main_8((void *)0);",
"source node": 20,
"start line": 799,
"target node": 21,
"thread": 8
},
{
"action": 0,
"file": 0,
"source": "ldv_initialize();",
"source node": 21,
"start line": 562,
"target node": 22,
"thread": 8
},
{
"action": 1,
"enter": 1,
"file": 0,
"source": "ldv_dispatch_insmod_register_8_3();",
"source node": 22,
"start line": 566,
"target node": 23,
"thread": 8
},
{
"file": 0,
"source": "struct ldv_struct_main_8 *cf_arg_3;",
"source node": 23,
"start line": 324,
"target node": 24,
"thread": 8
},
{
"enter": 2,
"file": 0,
"source": "cf_arg_3 = (struct ldv_struct_main_8 *)ldv_xmalloc(4UL);",
"source node": 24,
"start line": 324,
"target node": 25,
"thread": 8
},
{
"file": 4,
"source": "void *res;",
"source node": 25,
"start line": 68,
"target node": 26,
"thread": 8
},
{
"file": 4,
"source": "res = malloc(size);",
"source node": 26,
"start line": 68,
"target node": 27,
"thread": 8
},
{
"condition": true,
"file": 4,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 27,
"start line": 69,
"target node": 28,
"thread": 8
},
{
"condition": true,
"enter": 3,
"file": 4,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 28,
"start line": 70,
"target node": 29,
"thread": 8
},
{
"file": 5,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 29,
"start line": 22,
"target node": 30,
"thread": 8
},
{
"file": 4,
"return": 2,
"source": "return res;",
"source node": 30,
"start line": 71,
"target node": 31,
"thread": 8
},
{
"enter": 4,
"file": 0,
"source": "ldv_insmod_3((void *)cf_arg_3);",
"source node": 31,
"start line": 325,
"target node": 32,
"thread": 3
},
{
"action": 2,
"file": 0,
"source": "void (*ldv_3_esb_driver_exit_default)(void);",
"source node": 32,
"start line": 464,
"target node": 33,
"thread": 3
},
{
"action": 2,
"file": 0,
"source": "int (*ldv_3_esb_driver_init_default)(void);",
"source node": 33,
"start line": 465,
"target node": 34,
"thread": 3
},
{
"action": 2,
"file": 0,
"source": "int ldv_3_ret_default;",
"source node": 34,
"start line": 466,
"target node": 35,
"thread": 3
},
{
"action": 3,
"enter": 5,
"file": 0,
"source": "ldv_free(arg0);",
"source node": 35,
"start line": 470,
"target node": 36,
"thread": 3
},
{
"file": 4,
"source": "free(s);",
"source node": 36,
"start line": 63,
"target node": 37,
"thread": 3
},
{
"file": 4,
"return": 5,
"source": "return;",
"source node": 37,
"start line": 64,
"target node": 38,
"thread": 3
},
{
"action": 4,
"enter": 8,
"file": 2,
"original file": 0,
"original start line": 485,
"source": "ldv_3_ret_default = esb_driver_init();",
"source node": 38,
"start line": 495,
"target node": 39,
"thread": 3
},
{
"enter": 10,
"file": 2,
"source": "ldv_emg___pci_register_driver(&esb_driver, &__this_module, \"i6300esb\");",
"source node": 39,
"start line": 495,
"target node": 40,
"thread": 3
},
{
"action": 2,
"file": 0,
"source": "struct pci_driver *ldv_7_pci_driver_pci_driver;",
"source node": 40,
"start line": 351,
"target node": 41,
"thread": 3
},
{
"action": 5,
"file": 0,
"source": "ldv_7_pci_driver_pci_driver = arg0;",
"source node": 41,
"start line": 357,
"target node": 42,
"thread": 3
},
{
"action": 6,
"enter": 11,
"file": 0,
"source": "ldv_dispatch_register_7_3(ldv_7_pci_driver_pci_driver);",
"source node": 42,
"start line": 361,
"target node": 43,
"thread": 3
},
{
"file": 0,
"source": "struct ldv_struct_pci_scenario_2 *cf_arg_2;",
"source node": 43,
"start line": 341,
"target node": 44,
"thread": 3
},
{
"enter": 2,
"file": 0,
"source": "cf_arg_2 = (struct ldv_struct_pci_scenario_2 *)ldv_xmalloc(16UL);",
"source node": 44,
"start line": 341,
"target node": 45,
"thread": 3
},
{
"file": 4,
"source": "void *res;",
"source node": 45,
"start line": 68,
"target node": 46,
"thread": 3
},
{
"file": 4,
"source": "res = malloc(size);",
"source node": 46,
"start line": 68,
"target node": 47,
"thread": 3
},
{
"condition": true,
"file": 4,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 47,
"start line": 69,
"target node": 48,
"thread": 3
},
{
"condition": true,
"enter": 3,
"file": 4,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 48,
"start line": 70,
"target node": 49,
"thread": 3
},
{
"file": 5,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 49,
"start line": 22,
"target node": 50,
"thread": 3
},
{
"file": 4,
"return": 2,
"source": "return res;",
"source node": 50,
"start line": 71,
"target node": 51,
"thread": 3
},
{
"file": 0,
"source": "cf_arg_2->arg0 = arg0;",
"source node": 51,
"start line": 342,
"target node": 52,
"thread": 3
},
{
"enter": 12,
"file": 0,
"source": "ldv_pci_scenario_2((void *)cf_arg_2);",
"source node": 52,
"start line": 343,
"target node": 53,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "struct pci_driver *ldv_2_container_pci_driver;",
"source node": 53,
"start line": 588,
"target node": 54,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "struct pci_device_id *ldv_2_ldv_param_17_1_default;",
"source node": 54,
"start line": 589,
"target node": 55,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "struct pci_dev *ldv_2_resource_dev;",
"source node": 55,
"start line": 590,
"target node": 56,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "pm_message_t ldv_2_resource_pm_message;",
"source node": 56,
"start line": 591,
"target node": 57,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "int ldv_2_ret_default;",
"source node": 57,
"start line": 592,
"target node": 58,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "struct ldv_struct_pci_scenario_2 *data;",
"source node": 58,
"start line": 593,
"target node": 59,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "data = (struct ldv_struct_pci_scenario_2 *)arg0;",
"source node": 59,
"start line": 595,
"target node": 60,
"thread": 2
},
{
"action": 7,
"condition": true,
"file": 0,
"source": "((unsigned long)data) != ((unsigned long)((struct ldv_struct_pci_scenario_2 *)0))",
"source node": 60,
"start line": 602,
"target node": 61,
"thread": 2
},
{
"action": 7,
"file": 0,
"source": "ldv_2_container_pci_driver = data->arg0;",
"source node": 61,
"start line": 603,
"target node": 62,
"thread": 2
},
{
"action": 7,
"enter": 5,
"file": 0,
"source": "ldv_free((void *)data);",
"source node": 62,
"start line": 604,
"target node": 63,
"thread": 2
},
{
"file": 4,
"source": "free(s);",
"source node": 63,
"start line": 63,
"target node": 64,
"thread": 2
},
{
"file": 4,
"return": 5,
"source": "return;",
"source node": 64,
"start line": 64,
"target node": 65,
"thread": 2
},
{
"action": 8,
"enter": 2,
"file": 0,
"source": "ldv_2_resource_dev = (struct pci_dev *)ldv_xmalloc(2936UL);",
"source node": 65,
"start line": 609,
"target node": 66,
"thread": 2
},
{
"file": 4,
"source": "void *res;",
"source node": 66,
"start line": 68,
"target node": 67,
"thread": 2
},
{
"file": 4,
"source": "res = malloc(size);",
"source node": 67,
"start line": 68,
"target node": 68,
"thread": 2
},
{
"condition": true,
"file": 4,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 68,
"start line": 69,
"target node": 69,
"thread": 2
},
{
"condition": true,
"enter": 3,
"file": 4,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 69,
"start line": 70,
"target node": 70,
"thread": 2
},
{
"file": 5,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 70,
"start line": 22,
"target node": 71,
"thread": 2
},
{
"file": 4,
"return": 2,
"source": "return res;",
"source node": 71,
"start line": 71,
"target node": 72,
"thread": 2
},
{
"action": 9,
"enter": 13,
"file": 0,
"source": "ldv_2_ldv_param_17_1_default = (struct pci_device_id *)ldv_xmalloc_unknown_size(0UL);",
"source node": 72,
"start line": 626,
"target node": 73,
"thread": 2
},
{
"file": 4,
"source": "void *res;",
"source node": 73,
"start line": 116,
"target node": 74,
"thread": 2
},
{
"file": 4,
"source": "res = external_allocated_data();",
"source node": 74,
"start line": 116,
"target node": 75,
"thread": 2
},
{
"condition": true,
"file": 4,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 75,
"start line": 117,
"target node": 76,
"thread": 2
},
{
"condition": true,
"enter": 3,
"file": 4,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 76,
"start line": 118,
"target node": 77,
"thread": 2
},
{
"file": 5,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 77,
"start line": 22,
"target node": 78,
"thread": 2
},
{
"file": 4,
"return": 13,
"source": "return res;",
"source node": 78,
"start line": 119,
"target node": 79,
"thread": 2
},
{
"action": 10,
"file": 0,
"source": "ldv_pre_probe();",
"source node": 79,
"start line": 631,
"target node": 80,
"thread": 2
},
{
"action": 10,
"enter": 15,
"file": 2,
"original file": 0,
"original start line": 633,
"source": "ldv_2_ret_default = esb_probe(ldv_2_resource_dev, ldv_2_ldv_param_17_1_default);",
"source node": 80,
"start line": 421,
"target node": 81,
"thread": 2
},
{
"file": 2,
"source": "int ret;",
"source node": 81,
"start line": 421,
"target node": 82,
"thread": 2
},
{
"file": 2,
"source": "cards_found = cards_found + 1;",
"source node": 82,
"start line": 424,
"target node": 83,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "cards_found == 1",
"source node": 83,
"start line": 425,
"target node": 84,
"thread": 2
},
{
"file": 2,
"source": "printk(\"\\016i6300esb: Intel 6300ESB WatchDog Timer Driver v%s\\n\", (char *)\"0.05\");",
"source node": 84,
"start line": 426,
"target node": 85,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "cards_found <= 1",
"source node": 85,
"start line": 429,
"target node": 86,
"thread": 2
},
{
"condition": true,
"enter": 16,
"file": 2,
"source": "((unsigned int)esb_getdevice(pdev)) != 0U",
"source node": 86,
"start line": 435,
"target node": 87,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "pci_enable_device(pdev) == 0",
"source node": 87,
"start line": 349,
"target node": 88,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "pci_request_region(pdev, 0, \"i6300ESB timer\") == 0",
"source node": 88,
"start line": 354,
"target node": 89,
"thread": 2
},
{
"file": 2,
"source": "BASEADDR = pci_ioremap_bar(pdev, 0);",
"source node": 89,
"start line": 359,
"target node": 90,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "((unsigned long)BASEADDR) != ((unsigned long)((void *)0))",
"source node": 90,
"start line": 360,
"target node": 91,
"thread": 2
},
{
"file": 2,
"source": "esb_pci = pdev;",
"source node": 91,
"start line": 367,
"target node": 92,
"thread": 2
},
{
"file": 2,
"return": 16,
"source": "return 1U;",
"source node": 92,
"start line": 368,
"target node": 93,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "((unsigned long)esb_pci) != ((unsigned long)((struct pci_dev *)0))",
"source node": 93,
"start line": 435,
"target node": 94,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "(((unsigned int)heartbeat) - 1U) > 2045U",
"source node": 94,
"start line": 440,
"target node": 95,
"thread": 2
},
{
"file": 2,
"source": "heartbeat = 30;",
"source node": 95,
"start line": 441,
"target node": 96,
"thread": 2
},
{
"file": 2,
"source": "printk(\"\\016i6300esb: heartbeat value must be 1<heartbeat<2046, using %d\\n\", heartbeat);",
"source node": 96,
"start line": 442,
"target node": 97,
"thread": 2
},
{
"enter": 17,
"file": 2,
"source": "esb_initdevice();",
"source node": 97,
"start line": 447,
"target node": 98,
"thread": 2
},
{
"file": 2,
"source": "u8 val1;",
"source node": 98,
"start line": 380,
"target node": 99,
"thread": 2
},
{
"file": 2,
"source": "u16 val2;",
"source node": 99,
"start line": 381,
"target node": 100,
"thread": 2
},
{
"enter": 18,
"file": 2,
"source": "pci_write_config_word((struct pci_dev const *)esb_pci, 96, 3);",
"source node": 100,
"start line": 395,
"target node": 101,
"thread": 2
},
{
"file": 7,
"return": 18,
"source": "return pci_bus_write_config_word(dev->bus, dev->devfn, where, (int)val);",
"source node": 101,
"start line": 853,
"target node": 102,
"thread": 2
},
{
"enter": 19,
"file": 2,
"source": "pci_read_config_byte((struct pci_dev const *)esb_pci, 104, &val1);",
"source node": 102,
"start line": 398,
"target node": 103,
"thread": 2
},
{
"file": 7,
"return": 19,
"source": "return pci_bus_read_config_byte(dev->bus, dev->devfn, where, val);",
"source node": 103,
"start line": 836,
"target node": 104,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "(((int)val1) &1) != 0",
"source node": 104,
"start line": 399,
"target node": 105,
"thread": 2
},
{
"file": 2,
"source": "printk(\"\\fi6300esb: nowayout already set\\n\");",
"source node": 105,
"start line": 400,
"target node": 106,
"thread": 2
},
{
"enter": 20,
"file": 2,
"source": "pci_write_config_byte((struct pci_dev const *)esb_pci, 104, 0);",
"source node": 106,
"start line": 403,
"target node": 107,
"thread": 2
},
{
"file": 7,
"return": 20,
"source": "return pci_bus_write_config_byte(dev->bus, dev->devfn, where, (int)val);",
"source node": 107,
"start line": 849,
"target node": 108,
"thread": 2
},
{
"enter": 21,
"file": 2,
"source": "esb_unlock_registers();",
"source node": 108,
"start line": 406,
"target node": 109,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(128, (void volatile *)(BASEADDR + 12UL));",
"source node": 109,
"start line": 116,
"target node": 110,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 110,
"start line": 63,
"target node": 111,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(134, (void volatile *)(BASEADDR + 12UL));",
"source node": 111,
"start line": 117,
"target node": 112,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 112,
"start line": 63,
"target node": 113,
"thread": 2
},
{
"file": 2,
"return": 21,
"source": "return;",
"source node": 113,
"start line": 118,
"target node": 114,
"thread": 2
},
{
"enter": 23,
"file": 2,
"source": "val2 = readw((void const volatile *)(BASEADDR + 12UL));",
"source node": 114,
"start line": 407,
"target node": 115,
"thread": 2
},
{
"file": 8,
"source": "unsigned short ret;",
"source node": 115,
"start line": 56,
"target node": 116,
"thread": 2
},
{
"file": 8,
"return": 23,
"source": "return ret;",
"source node": 116,
"start line": 54,
"target node": 117,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "(((int)val2) &512) != 0",
"source node": 117,
"start line": 408,
"target node": 118,
"thread": 2
},
{
"file": 2,
"source": "triggered = 32U;",
"source node": 118,
"start line": 409,
"target node": 119,
"thread": 2
},
{
"enter": 21,
"file": 2,
"source": "esb_unlock_registers();",
"source node": 119,
"start line": 412,
"target node": 120,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(128, (void volatile *)(BASEADDR + 12UL));",
"source node": 120,
"start line": 116,
"target node": 121,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 121,
"start line": 63,
"target node": 122,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(134, (void volatile *)(BASEADDR + 12UL));",
"source node": 122,
"start line": 117,
"target node": 123,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 123,
"start line": 63,
"target node": 124,
"thread": 2
},
{
"file": 2,
"return": 21,
"source": "return;",
"source node": 124,
"start line": 118,
"target node": 125,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(768, (void volatile *)(BASEADDR + 12UL));",
"source node": 125,
"start line": 413,
"target node": 126,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 126,
"start line": 63,
"target node": 127,
"thread": 2
},
{
"enter": 24,
"file": 2,
"source": "esb_timer_set_heartbeat(heartbeat);",
"source node": 127,
"start line": 416,
"target node": 128,
"thread": 2
},
{
"file": 2,
"source": "u32 val;",
"source node": 128,
"start line": 162,
"target node": 129,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "(((unsigned int)time) - 1U) <= 2045U",
"source node": 129,
"start line": 164,
"target node": 130,
"thread": 2
},
{
"enter": 25,
"file": 2,
"source": "spin_lock(&esb_lock);",
"source node": 130,
"start line": 167,
"target node": 131,
"thread": 2
},
{
"file": 9,
"source": "_raw_spin_lock(&lock->__annonCompField19.rlock);",
"source node": 131,
"start line": 303,
"target node": 132,
"thread": 2
},
{
"file": 9,
"return": 25,
"source": "return;",
"source node": 132,
"start line": 304,
"target node": 133,
"thread": 2
},
{
"file": 2,
"source": "val = (u32)(time << 9);",
"source node": 133,
"start line": 173,
"target node": 134,
"thread": 2
},
{
"enter": 21,
"file": 2,
"source": "esb_unlock_registers();",
"source node": 134,
"start line": 176,
"target node": 135,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(128, (void volatile *)(BASEADDR + 12UL));",
"source node": 135,
"start line": 116,
"target node": 136,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 136,
"start line": 63,
"target node": 137,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(134, (void volatile *)(BASEADDR + 12UL));",
"source node": 137,
"start line": 117,
"target node": 138,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 138,
"start line": 63,
"target node": 139,
"thread": 2
},
{
"file": 2,
"return": 21,
"source": "return;",
"source node": 139,
"start line": 118,
"target node": 140,
"thread": 2
},
{
"enter": 26,
"file": 2,
"source": "writel(val, (void volatile *)BASEADDR);",
"source node": 140,
"start line": 177,
"target node": 141,
"thread": 2
},
{
"file": 8,
"return": 26,
"source": "return;",
"source node": 141,
"start line": 64,
"target node": 142,
"thread": 2
},
{
"enter": 21,
"file": 2,
"source": "esb_unlock_registers();",
"source node": 142,
"start line": 180,
"target node": 143,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(128, (void volatile *)(BASEADDR + 12UL));",
"source node": 143,
"start line": 116,
"target node": 144,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 144,
"start line": 63,
"target node": 145,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(134, (void volatile *)(BASEADDR + 12UL));",
"source node": 145,
"start line": 117,
"target node": 146,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 146,
"start line": 63,
"target node": 147,
"thread": 2
},
{
"file": 2,
"return": 21,
"source": "return;",
"source node": 147,
"start line": 118,
"target node": 148,
"thread": 2
},
{
"enter": 26,
"file": 2,
"source": "writel(val, (void volatile *)(BASEADDR + 4UL));",
"source node": 148,
"start line": 181,
"target node": 149,
"thread": 2
},
{
"file": 8,
"return": 26,
"source": "return;",
"source node": 149,
"start line": 64,
"target node": 150,
"thread": 2
},
{
"enter": 21,
"file": 2,
"source": "esb_unlock_registers();",
"source node": 150,
"start line": 184,
"target node": 151,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(128, (void volatile *)(BASEADDR + 12UL));",
"source node": 151,
"start line": 116,
"target node": 152,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 152,
"start line": 63,
"target node": 153,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(134, (void volatile *)(BASEADDR + 12UL));",
"source node": 153,
"start line": 117,
"target node": 154,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 154,
"start line": 63,
"target node": 155,
"thread": 2
},
{
"file": 2,
"return": 21,
"source": "return;",
"source node": 155,
"start line": 118,
"target node": 156,
"thread": 2
},
{
"enter": 22,
"file": 2,
"source": "writew(256, (void volatile *)(BASEADDR + 12UL));",
"source node": 156,
"start line": 185,
"target node": 157,
"thread": 2
},
{
"file": 8,
"return": 22,
"source": "return;",
"source node": 157,
"start line": 63,
"target node": 158,
"thread": 2
},
{
"file": 2,
"source": "heartbeat = time;",
"source node": 158,
"start line": 190,
"target node": 159,
"thread": 2
},
{
"enter": 27,
"file": 2,
"source": "spin_unlock(&esb_lock);",
"source node": 159,
"start line": 191,
"target node": 160,
"thread": 2
},
{
"file": 9,
"source": "_raw_spin_unlock(&lock->__annonCompField19.rlock);",
"source node": 160,
"start line": 343,
"target node": 161,
"thread": 2
},
{
"file": 9,
"return": 27,
"source": "return;",
"source node": 161,
"start line": 344,
"target node": 162,
"thread": 2
},
{
"file": 2,
"return": 24,
"source": "return 0;",
"source node": 162,
"start line": 192,
"target node": 163,
"thread": 2
},
{
"file": 2,
"return": 17,
"source": "return;",
"source node": 163,
"start line": 417,
"target node": 164,
"thread": 2
},
{
"enter": 29,
"file": 2,
"source": "ret = ldv_emg_misc_register(&esb_miscdev);",
"source node": 164,
"start line": 450,
"target node": 165,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "struct file_operations *ldv_5_file_operations_file_operations;",
"source node": 165,
"start line": 407,
"target node": 166,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "struct miscdevice *ldv_5_miscdevice_miscdevice;",
"source node": 166,
"start line": 408,
"target node": 167,
"thread": 2
},
{
"action": 11,
"enter": 30,
"file": 0,
"return": 29,
"source": "return ldv_undef_int_negative();",
"source node": 167,
"start line": 431,
"target node": 168,
"thread": 2
},
{
"file": 6,
"source": "int ret;",
"source node": 168,
"start line": 54,
"target node": 169,
"thread": 2
},
{
"enter": 6,
"file": 6,
"source": "ret = ldv_undef_int();",
"source node": 169,
"start line": 54,
"target node": 170,
"thread": 2
},
{
"file": 6,
"return": 6,
"source": "return __VERIFIER_nondet_int();",
"source node": 170,
"start line": 41,
"target node": 171,
"thread": 2
},
{
"condition": true,
"file": 6,
"source": "__VERIFIER_assume(ret < 0);",
"source node": 171,
"start line": 55,
"target node": 172,
"thread": 2
},
{
"file": 6,
"return": 30,
"source": "return ret;",
"source node": 172,
"start line": 56,
"target node": 173,
"thread": 2
},
{
"condition": true,
"file": 2,
"source": "ret != 0",
"source node": 173,
"start line": 451,
"target node": 174,
"thread": 2
},
{
"file": 2,
"source": "printk(\"\\vi6300esb: cannot register miscdev on minor=%d (err=%d)\\n\", 130, ret);",
"source node": 174,
"start line": 452,
"target node": 175,
"thread": 2
},
{
"enter": 32,
"file": 2,
"source": "ldv_io_mem_unmap();",
"source node": 175,
"start line": 461,
"target node": 176,
"thread": 2,
"warn": "io-memory should be alloctaed before release"
},
{
"enter": 33,
"file": 3,
"note": "io-memory should be alloctaed before release",
"source": "ldv_assert_linux_arch_io__less_initial_decrement(ldv_iomem > 0);",
"source node": 176,
"start line": 43,
"target node": 177,
"thread": 2
},
{
"condition": true,
"file": 10,
"source": "expr == 0",
"source node": 177,
"start line": 4,
"target node": 178,
"thread": 2
},
{
"file": 10,
"source": "__VERIFIER_error();",
"source node": 178,
"start line": 5,
"target node": 179,
"thread": 2
}
],
"entry node": 0,
"files": [
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/avtg/drivers/watchdog/i6300esb.ko/linux:arch:io/weaver/.tmp_i6300esb.c.aux",
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/lkbce/include/linux/export.h",
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/lkbce/drivers/watchdog/i6300esb.c",
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/job/root/linux/arch/io.c",
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/job/root/verifier/memory.c",
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/job/root/linux/err.c",
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/job/root/verifier/nondet.c",
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/lkbce/include/linux/pci.h",
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/lkbce/arch/x86/include/asm/io.h",
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/lkbce/include/linux/spinlock.h",
"/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/b6a3bba6e2b558de36ac7680a6a194c4/klever-core-work-dir/vtg/drivers/watchdog/i6300esb.ko/linux:arch:io/rsb/bug kind funcs.c"
],
"funcs": [
"ldv_main_8",
"ldv_dispatch_insmod_register_8_3",
"ldv_xmalloc",
"ldv_is_err",
"ldv_insmod_3",
"ldv_free",
"ldv_undef_int",
"ldv_insmod_esb_driver_init_3_6",
"esb_driver_init",
"ldv___pci_register_driver_14",
"ldv_emg___pci_register_driver",
"ldv_dispatch_register_7_3",
"ldv_pci_scenario_2",
"ldv_xmalloc_unknown_size",
"ldv_pci_scenario_probe_2_17",
"esb_probe",
"esb_getdevice",
"esb_initdevice",
"pci_write_config_word",
"pci_read_config_byte",
"pci_write_config_byte",
"esb_unlock_registers",
"writew",
"readw",
"esb_timer_set_heartbeat",
"spin_lock",
"writel",
"spin_unlock",
"ldv_misc_register_10",
"ldv_emg_misc_register",
"ldv_undef_int_negative",
"ldv_iounmap_11",
"ldv_io_mem_unmap",
"ldv_assert_linux_arch_io__less_initial_decrement"
],
"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,
null
]
],
"violation nodes": [
179
]
}
(1-1/2)