Project

General

Profile

Download (31.7 KB)

Feature #8743 » error trace(14).json

Ilja Zakharov, 07/18/2018 01:53 PM

 
{
"actions": [
"Initialize rule models.",
"Begin Environment model scenarios.",
"Declare auxiliary variables.",
"Trigger module initialization.",
"Initialize the module after insmod with 'ldv_init' function. Invoke callback ldv_init from INSMOD.",
"Get 'usb' callbacks to register.",
"Register USB callbacks.",
"Begin USB callbacks invocation scenario.",
"Allocate memory and initialize new USB interface.",
"Allocate memory for adhoc callback parameters.",
"Associate driver-specific data with the USB interface. Invoke callback probe from usb_driver."
],
"callback actions": [
0,
4,
10
],
"edges": [
{
"end line": 54,
"file": 0,
"source": "static struct usb_driver ldv_driver = #line 34 {\"ldv-test\", &ldv_probe, &ldv_disconnect, 0, 0, 0, 0, 0, 0, 0, {{{{{0U}, 0U, 0U, 0, {0, 0, 0, 0, 0UL}}}}, {0, 0}}, {{0, 0, 0, 0, (_Bool)0, 0, 0, 0, 0, 0, 0, 0, 0}, 0}, 0U, 0U, 0U};",
"source node": 0,
"start line": 34,
"target node": 1,
"thread": 0
},
{
"assumption": "registered == 0;",
"end line": 18,
"file": 1,
"source": "int registered;",
"source node": 1,
"start line": 18,
"target node": 2,
"thread": 0
},
{
"assumption": "probed == 0;",
"end line": 19,
"file": 1,
"source": "int probed;",
"source node": 2,
"start line": 19,
"target node": 3,
"thread": 0
},
{
"assumption": "supress == 0;",
"end line": 20,
"file": 1,
"source": "int supress;",
"source node": 3,
"start line": 20,
"target node": 4,
"thread": 0
},
{
"end line": 25,
"file": 2,
"source": "static bool __ldv_in_interrupt_context = 0;",
"source node": 4,
"start line": 25,
"target node": 5,
"thread": 0
},
{
"end line": 419,
"enter": 0,
"entry_point": "Entry point 'main'",
"file": 3,
"line": 419,
"source": "Begin program execution",
"source node": 5,
"start line": 419,
"target node": 6,
"thread": 1
},
{
"action": 0,
"end line": 422,
"enter": 1,
"file": 3,
"note": "Initialize EMG test rule specification.",
"source": "ldv_initialize();",
"source node": 6,
"start line": 422,
"target node": 7,
"thread": 1
},
{
"end line": 25,
"file": 1,
"source": "int registered___0;",
"source node": 7,
"start line": 25,
"target node": 8,
"thread": 1
},
{
"end line": 26,
"file": 1,
"note": "Initializing EMG test states.",
"source": "int probed___0;",
"source node": 8,
"start line": 26,
"target node": 9,
"thread": 1
},
{
"end line": 26,
"file": 1,
"note": "Initializing EMG test states.",
"source": "registered___0 = 0;",
"source node": 9,
"start line": 26,
"target node": 10,
"thread": 1
},
{
"end line": 27,
"file": 1,
"source": "probed___0 = 0;",
"source node": 10,
"start line": 27,
"target node": 11,
"thread": 1
},
{
"end line": 28,
"file": 1,
"return": 1,
"source": "return;",
"source node": 11,
"start line": 28,
"target node": 12,
"thread": 1
},
{
"action": 1,
"end line": 425,
"enter": 3,
"file": 3,
"source": "ldv_dispatch_insmod_register_6_2();",
"source node": 12,
"start line": 425,
"target node": 13,
"thread": 1
},
{
"end line": 73,
"file": 3,
"source": "struct ldv_struct_main_6 *cf_arg_3;",
"source node": 13,
"start line": 73,
"target node": 14,
"thread": 1
},
{
"end line": 73,
"enter": 4,
"file": 3,
"source": "cf_arg_3 = (struct ldv_struct_main_6 *)ldv_xmalloc(4UL);",
"source node": 14,
"start line": 73,
"target node": 15,
"thread": 1
},
{
"assumption": "size == 4UL;",
"assumption scope": 4,
"end line": 69,
"file": 4,
"source": "void *res;",
"source node": 15,
"start line": 69,
"target node": 16,
"thread": 1
},
{
"end line": 69,
"file": 4,
"source": "res = malloc(size);",
"source node": 16,
"start line": 69,
"target node": 17,
"thread": 1
},
{
"end line": 71,
"file": 4,
"source": "[__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));]",
"source node": 17,
"start line": 71,
"target node": 18,
"thread": 1
},
{
"end line": 72,
"enter": 5,
"file": 4,
"source": "[__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);]",
"source node": 18,
"start line": 72,
"target node": 19,
"thread": 1
},
{
"end line": 22,
"file": 5,
"return": 5,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 19,
"start line": 22,
"target node": 20,
"thread": 1
},
{
"end line": 74,
"file": 4,
"return": 4,
"source": "return res;",
"source node": 20,
"start line": 74,
"target node": 21,
"thread": 1
},
{
"end line": 74,
"enter": 6,
"entry_point": "Initialize or exit module.",
"file": 3,
"source": "ldv_insmod_3((void *)cf_arg_3);",
"source node": 21,
"start line": 74,
"target node": 22,
"thread": 3
},
{
"action": 2,
"end line": 145,
"file": 3,
"source": "void (*ldv_3_ldv_exit_default)(void);",
"source node": 22,
"start line": 145,
"target node": 23,
"thread": 3
},
{
"action": 2,
"end line": 146,
"file": 3,
"source": "int (*ldv_3_ldv_init_default)(void);",
"source node": 23,
"start line": 146,
"target node": 24,
"thread": 3
},
{
"action": 2,
"end line": 147,
"file": 3,
"source": "int ldv_3_ret_default;",
"source node": 24,
"start line": 147,
"target node": 25,
"thread": 3
},
{
"action": 3,
"end line": 151,
"enter": 7,
"file": 3,
"source": "ldv_free(arg0);",
"source node": 25,
"start line": 151,
"target node": 26,
"thread": 3
},
{
"end line": 64,
"file": 4,
"source": "free(s);",
"source node": 26,
"start line": 64,
"target node": 27,
"thread": 3
},
{
"end line": 65,
"file": 4,
"return": 7,
"source": "return;",
"source node": 27,
"start line": 65,
"target node": 28,
"thread": 3
},
{
"action": 4,
"end line": 156,
"enter": 9,
"file": 0,
"original file": 3,
"original start line": 156,
"source": "ldv_3_ret_default = ldv_init();",
"source node": 28,
"start line": 42,
"target node": 29,
"thread": 3
},
{
"end line": 42,
"enter": 10,
"file": 0,
"note": "Supress unrelevant warnings.",
"source": "ldv_invoke_test();",
"source node": 29,
"start line": 42,
"target node": 30,
"thread": 3
},
{
"end line": 33,
"file": 1,
"source": "int supress___0;",
"source node": 30,
"start line": 33,
"target node": 31,
"thread": 3
},
{
"end line": 34,
"file": 1,
"note": "This test is intended to only the fact that callbacks are called. Supress rest warnings.",
"source": "supress___0 = 1;",
"source node": 31,
"start line": 34,
"target node": 32,
"thread": 3
},
{
"end line": 35,
"file": 1,
"return": 10,
"source": "return;",
"source node": 32,
"start line": 35,
"target node": 33,
"thread": 3
},
{
"end line": 43,
"enter": 12,
"entry_point": "Register 'usb' callbacks. (Relevant to 'ldv_driver')",
"file": 0,
"source": "ldv_emg_usb_register(&ldv_driver);",
"source node": 33,
"start line": 43,
"target node": 34,
"thread": 3
},
{
"action": 2,
"end line": 111,
"file": 3,
"source": "struct usb_driver *ldv_5_usb_driver_usb_driver;",
"source node": 34,
"start line": 111,
"target node": 35,
"thread": 3
},
{
"action": 5,
"end line": 118,
"file": 3,
"source": "ldv_5_usb_driver_usb_driver = arg0;",
"source node": 35,
"start line": 118,
"target node": 36,
"thread": 3
},
{
"action": 6,
"end line": 122,
"enter": 14,
"file": 3,
"source": "ldv_dispatch_register_5_3(ldv_5_usb_driver_usb_driver);",
"source node": 36,
"start line": 122,
"target node": 37,
"thread": 3
},
{
"end line": 81,
"file": 3,
"source": "struct ldv_struct_usb_scenario_2 *cf_arg_2;",
"source node": 37,
"start line": 81,
"target node": 38,
"thread": 3
},
{
"end line": 81,
"enter": 4,
"file": 3,
"source": "cf_arg_2 = (struct ldv_struct_usb_scenario_2 *)ldv_xmalloc(16UL);",
"source node": 38,
"start line": 81,
"target node": 39,
"thread": 3
},
{
"assumption": "size == 4UL;",
"assumption scope": 4,
"end line": 69,
"file": 4,
"source": "void *res;",
"source node": 39,
"start line": 69,
"target node": 40,
"thread": 3
},
{
"end line": 69,
"file": 4,
"source": "res = malloc(size);",
"source node": 40,
"start line": 69,
"target node": 41,
"thread": 3
},
{
"end line": 71,
"file": 4,
"source": "[__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));]",
"source node": 41,
"start line": 71,
"target node": 42,
"thread": 3
},
{
"end line": 72,
"enter": 5,
"file": 4,
"source": "[__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);]",
"source node": 42,
"start line": 72,
"target node": 43,
"thread": 3
},
{
"end line": 22,
"file": 5,
"return": 5,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 43,
"start line": 22,
"target node": 44,
"thread": 3
},
{
"end line": 74,
"file": 4,
"return": 4,
"source": "return res;",
"source node": 44,
"start line": 74,
"target node": 45,
"thread": 3
},
{
"end line": 82,
"file": 3,
"source": "cf_arg_2->arg0 = arg0;",
"source node": 45,
"start line": 82,
"target node": 46,
"thread": 3
},
{
"end line": 83,
"enter": 15,
"entry_point": "Invoke usb callbacks. (Relevant to 'ldv_driver')",
"file": 3,
"source": "ldv_usb_scenario_2((void *)cf_arg_2);",
"source node": 46,
"start line": 83,
"target node": 47,
"thread": 2
},
{
"action": 2,
"end line": 228,
"file": 3,
"source": "struct usb_driver *ldv_2_container_usb_driver;",
"source node": 47,
"start line": 228,
"target node": 48,
"thread": 2
},
{
"action": 2,
"end line": 229,
"file": 3,
"source": "struct usb_device_id *ldv_2_ldv_param_14_1_default;",
"source node": 48,
"start line": 229,
"target node": 49,
"thread": 2
},
{
"action": 2,
"end line": 230,
"file": 3,
"source": "int ldv_2_probe_retval_default;",
"source node": 49,
"start line": 230,
"target node": 50,
"thread": 2
},
{
"action": 2,
"end line": 231,
"file": 3,
"source": "_Bool ldv_2_reset_flag_default;",
"source node": 50,
"start line": 231,
"target node": 51,
"thread": 2
},
{
"action": 2,
"end line": 232,
"file": 3,
"source": "struct usb_interface *ldv_2_resource_usb_interface;",
"source node": 51,
"start line": 232,
"target node": 52,
"thread": 2
},
{
"action": 2,
"end line": 233,
"file": 3,
"source": "struct usb_device *ldv_2_usb_device_usb_device;",
"source node": 52,
"start line": 233,
"target node": 53,
"thread": 2
},
{
"action": 2,
"end line": 234,
"file": 3,
"source": "struct ldv_struct_usb_scenario_2 *data;",
"source node": 53,
"start line": 234,
"target node": 54,
"thread": 2
},
{
"action": 2,
"end line": 236,
"file": 3,
"source": "data = (struct ldv_struct_usb_scenario_2 *)arg0;",
"source node": 54,
"start line": 236,
"target node": 55,
"thread": 2
},
{
"action": 7,
"condition": true,
"end line": 244,
"file": 3,
"source": "((unsigned long)data) != ((unsigned long)((struct ldv_struct_usb_scenario_2 *)0))",
"source node": 55,
"start line": 244,
"target node": 56,
"thread": 2
},
{
"action": 7,
"end line": 245,
"file": 3,
"source": "ldv_2_container_usb_driver = data->arg0;",
"source node": 56,
"start line": 245,
"target node": 57,
"thread": 2
},
{
"action": 7,
"end line": 246,
"enter": 7,
"file": 3,
"source": "ldv_free((void *)data);",
"source node": 57,
"start line": 246,
"target node": 58,
"thread": 2
},
{
"end line": 64,
"file": 4,
"source": "free(s);",
"source node": 58,
"start line": 64,
"target node": 59,
"thread": 2
},
{
"end line": 65,
"file": 4,
"return": 7,
"source": "return;",
"source node": 59,
"start line": 65,
"target node": 60,
"thread": 2
},
{
"action": 8,
"end line": 252,
"enter": 4,
"file": 3,
"source": "ldv_2_resource_usb_interface = (struct usb_interface *)ldv_xmalloc(968UL);",
"source node": 60,
"start line": 252,
"target node": 61,
"thread": 2
},
{
"assumption": "size == 4UL;",
"assumption scope": 4,
"end line": 69,
"file": 4,
"source": "void *res;",
"source node": 61,
"start line": 69,
"target node": 62,
"thread": 2
},
{
"end line": 69,
"file": 4,
"source": "res = malloc(size);",
"source node": 62,
"start line": 69,
"target node": 63,
"thread": 2
},
{
"end line": 71,
"file": 4,
"source": "[__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));]",
"source node": 63,
"start line": 71,
"target node": 64,
"thread": 2
},
{
"end line": 72,
"enter": 5,
"file": 4,
"source": "[__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);]",
"source node": 64,
"start line": 72,
"target node": 65,
"thread": 2
},
{
"end line": 22,
"file": 5,
"return": 5,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 65,
"start line": 22,
"target node": 66,
"thread": 2
},
{
"end line": 74,
"file": 4,
"return": 4,
"source": "return res;",
"source node": 66,
"start line": 74,
"target node": 67,
"thread": 2
},
{
"action": 8,
"end line": 253,
"enter": 4,
"file": 3,
"source": "ldv_2_usb_device_usb_device = (struct usb_device *)ldv_xmalloc(2096UL);",
"source node": 67,
"start line": 253,
"target node": 68,
"thread": 2
},
{
"assumption": "size == 4UL;",
"assumption scope": 4,
"end line": 69,
"file": 4,
"source": "void *res;",
"source node": 68,
"start line": 69,
"target node": 69,
"thread": 2
},
{
"end line": 69,
"file": 4,
"source": "res = malloc(size);",
"source node": 69,
"start line": 69,
"target node": 70,
"thread": 2
},
{
"end line": 71,
"file": 4,
"source": "[__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));]",
"source node": 70,
"start line": 71,
"target node": 71,
"thread": 2
},
{
"end line": 72,
"enter": 5,
"file": 4,
"source": "[__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);]",
"source node": 71,
"start line": 72,
"target node": 72,
"thread": 2
},
{
"end line": 22,
"file": 5,
"return": 5,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 72,
"start line": 22,
"target node": 73,
"thread": 2
},
{
"end line": 74,
"file": 4,
"return": 4,
"source": "return res;",
"source node": 73,
"start line": 74,
"target node": 74,
"thread": 2
},
{
"action": 8,
"end line": 254,
"file": 3,
"source": "ldv_2_resource_usb_interface->dev.parent = &ldv_2_usb_device_usb_device->dev;",
"source node": 74,
"start line": 254,
"target node": 75,
"thread": 2
},
{
"action": 9,
"end line": 280,
"enter": 16,
"file": 3,
"source": "ldv_2_ldv_param_14_1_default = (struct usb_device_id *)ldv_xmalloc_unknown_size(0UL);",
"source node": 75,
"start line": 280,
"target node": 76,
"thread": 2
},
{
"end line": 123,
"file": 4,
"source": "void *res;",
"source node": 76,
"start line": 123,
"target node": 77,
"thread": 2
},
{
"end line": 123,
"file": 4,
"source": "res = external_allocated_data();",
"source node": 77,
"start line": 123,
"target node": 78,
"thread": 2
},
{
"end line": 125,
"file": 4,
"source": "[__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));]",
"source node": 78,
"start line": 125,
"target node": 79,
"thread": 2
},
{
"end line": 126,
"enter": 5,
"file": 4,
"source": "[__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);]",
"source node": 79,
"start line": 126,
"target node": 80,
"thread": 2
},
{
"end line": 22,
"file": 5,
"return": 5,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 80,
"start line": 22,
"target node": 81,
"thread": 2
},
{
"end line": 128,
"file": 4,
"return": 16,
"source": "return res;",
"source node": 81,
"start line": 128,
"target node": 82,
"thread": 2
},
{
"action": 10,
"end line": 285,
"file": 3,
"source": "ldv_pre_probe();",
"source node": 82,
"start line": 285,
"target node": 83,
"thread": 2
},
{
"action": 10,
"end line": 290,
"enter": 18,
"file": 0,
"original file": 3,
"original start line": 287,
"source": "ldv_2_probe_retval_default = ldv_probe(ldv_2_resource_usb_interface, ldv_2_ldv_param_14_1_default);",
"source node": 83,
"start line": 25,
"target node": 84,
"thread": 2
},
{
"end line": 25,
"enter": 19,
"file": 0,
"source": "ldv_invoke_reached();",
"source node": 84,
"start line": 25,
"target node": 85,
"thread": 2,
"warn": "Test successfully passes as the callback call is reached."
},
{
"end line": 60,
"enter": 20,
"file": 1,
"note": "Test successfully passes as the callback call is reached.",
"source": "ldv_assert_linux_emg_test(0);",
"source node": 85,
"start line": 60,
"target node": 86,
"thread": 2
},
{
"assumption": "expr == 0;",
"assumption scope": 20,
"condition": true,
"end line": 4,
"file": 1,
"source": "expr == 0",
"source node": 86,
"start line": 4,
"target node": 87,
"thread": 2
},
{
"end line": 5,
"file": 1,
"source": "__VERIFIER_error();",
"source node": 87,
"start line": 5,
"target node": 88,
"thread": 2
}
],
"entry node": 0,
"files": [
"ext-modules/usb_driver_v.1/usb_invoke.c",
"linux/emg/test_model.c",
"linux/ldv/common.c",
"klever-core-work-dir/0/tests/acda82a/linux-emg-test/vtg/ext-modules/usb_driver_v.1/usb_invoke.ko/linux:emg:test/weaver/.tmp_usb_invoke.c.aux",
"verifier/memory.c",
"linux/err.c",
"verifier/nondet.c"
],
"funcs": [
"main",
"ldv_initialize",
"ldv_main_6",
"ldv_dispatch_insmod_register_6_2",
"ldv_xmalloc",
"ldv_is_err",
"ldv_insmod_3",
"ldv_free",
"ldv_insmod_ldv_init_3_6",
"ldv_init",
"ldv_invoke_test",
"ldv_usb_register_9",
"ldv_emg_usb_register",
"ldv_undef_int",
"ldv_dispatch_register_5_3",
"ldv_usb_scenario_2",
"ldv_xmalloc_unknown_size",
"ldv_usb_scenario_probe_2_14",
"ldv_probe",
"ldv_invoke_reached",
"ldv_assert_linux_emg_test",
"ldv_invoke_callback",
"ldv_invoke_middle_callback",
"ldv_deregister",
"ldv_register",
"ldv_probe_up",
"ldv_release_down",
"ldv_release_completely",
"ldv_check_final_state",
"ldv_switch_to_interrupt_context",
"ldv_switch_to_process_context",
"ldv_dispatch_deregister_4_1",
"ldv_dispatch_insmod_deregister_6_1",
"ldv_emg_usb_deregister",
"ldv_insmod_ldv_exit_3_2",
"ldv_usb_scenario_post_2_10",
"ldv_usb_scenario_pre_2_11",
"ldv_usb_scenario_release_2_5",
"ldv_usb_scenario_resume_2_8",
"ERR_PTR",
"PTR_ERR",
"IS_ERR",
"IS_ERR_OR_NULL",
"kmalloc",
"kcalloc",
"kzalloc",
"ldv_dev_get_drvdata_8",
"ldv_usb_deregister_10"
],
"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,
null
]
],
"violation nodes": [
88
]
}
(3-3/3)