Project

General

Profile

Download (24.3 KB)

Feature #8372 ยป error-trace (4).json

Ilja Zakharov, 08/21/2017 06:50 PM

 
{
"actions": [
"Initialize rule models.",
"Start 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 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,
8
],
"edges": [
{
"assumption": "irq_id == 100U;",
"file": 0,
"source": "unsigned int irq_id = 100U;",
"source node": 0,
"start line": 24,
"target node": 1,
"thread": 0
},
{
"assumption": "data == 0LL;",
"file": 0,
"source": "void *data;",
"source node": 1,
"start line": 25,
"target node": 2,
"thread": 0
},
{
"file": 1,
"source": "struct ldv_thread ldv_thread_2;",
"source node": 2,
"start line": 62,
"target node": 3,
"thread": 0
},
{
"file": 1,
"source": "struct ldv_thread ldv_thread_3;",
"source node": 3,
"start line": 63,
"target node": 4,
"thread": 0
},
{
"file": 1,
"source": "struct ldv_thread ldv_thread_6;",
"source node": 4,
"start line": 64,
"target node": 5,
"thread": 0
},
{
"assumption": "registered == 0;",
"file": 2,
"source": "int registered = 0;",
"source node": 5,
"start line": 18,
"target node": 6,
"thread": 0
},
{
"assumption": "non_deregistered == 0;",
"file": 2,
"source": "int non_deregistered = 0;",
"source node": 6,
"start line": 19,
"target node": 7,
"thread": 0
},
{
"assumption": "probed == 0;",
"file": 2,
"source": "int probed = 0;",
"source node": 7,
"start line": 20,
"target node": 8,
"thread": 0
},
{
"enter": 22,
"entry_point": "Entry point 'main'",
"file": 1,
"line": 330,
"source": "Begin program execution",
"source node": 8,
"target node": 9,
"thread": 1
},
{
"enter": 0,
"entry_point": "Main entry point function.",
"file": 1,
"source": "ldv_main_6((void *)0);",
"source node": 9,
"start line": 332,
"target node": 10,
"thread": 6
},
{
"action": 0,
"file": 1,
"source": "ldv_initialize();",
"source node": 10,
"start line": 306,
"target node": 11,
"thread": 6
},
{
"action": 1,
"enter": 1,
"file": 1,
"source": "ldv_dispatch_insmod_register_6_3();",
"source node": 11,
"start line": 310,
"target node": 12,
"thread": 6
},
{
"file": 1,
"source": "struct ldv_struct_main_6 *cf_arg_3;",
"source node": 12,
"start line": 79,
"target node": 13,
"thread": 6
},
{
"enter": 2,
"file": 1,
"source": "cf_arg_3 = (struct ldv_struct_main_6 *)ldv_xmalloc(4UL);",
"source node": 13,
"start line": 79,
"target node": 14,
"thread": 6
},
{
"assumption": "size == 4UL;",
"assumption scope": 2,
"file": 3,
"source": "void *res;",
"source node": 14,
"start line": 68,
"target node": 15,
"thread": 6
},
{
"assumption": "tmp == 4LL;",
"assumption scope": 2,
"file": 3,
"source": "res = malloc(size);",
"source node": 15,
"start line": 68,
"target node": 16,
"thread": 6
},
{
"condition": true,
"file": 3,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 16,
"start line": 69,
"target node": 17,
"thread": 6
},
{
"condition": true,
"enter": 3,
"file": 3,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 17,
"start line": 70,
"target node": 18,
"thread": 6
},
{
"assumption": "ptr == 4LL;",
"assumption scope": 3,
"file": 4,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 18,
"start line": 22,
"target node": 19,
"thread": 6
},
{
"file": 3,
"return": 2,
"source": "return res;",
"source node": 19,
"start line": 71,
"target node": 20,
"thread": 6
},
{
"enter": 4,
"entry_point": "Initialize or exit module.",
"file": 1,
"source": "ldv_insmod_3((void *)cf_arg_3);",
"source node": 20,
"start line": 80,
"target node": 21,
"thread": 3
},
{
"action": 2,
"file": 1,
"source": "void (*ldv_3_ldv_exit_default)(void);",
"source node": 21,
"start line": 167,
"target node": 22,
"thread": 3
},
{
"action": 2,
"file": 1,
"source": "int (*ldv_3_ldv_init_default)(void);",
"source node": 22,
"start line": 168,
"target node": 23,
"thread": 3
},
{
"action": 2,
"file": 1,
"source": "int ldv_3_ret_default;",
"source node": 23,
"start line": 169,
"target node": 24,
"thread": 3
},
{
"action": 3,
"enter": 5,
"file": 1,
"source": "ldv_free(arg0);",
"source node": 24,
"start line": 173,
"target node": 25,
"thread": 3
},
{
"file": 3,
"source": "free(s);",
"source node": 25,
"start line": 63,
"target node": 26,
"thread": 3
},
{
"file": 3,
"return": 5,
"source": "return;",
"source node": 26,
"start line": 64,
"target node": 27,
"thread": 3
},
{
"action": 4,
"enter": 7,
"file": 0,
"original file": 1,
"original start line": 178,
"source": "ldv_3_ret_default = ldv_init();",
"source node": 27,
"start line": 35,
"target node": 28,
"thread": 3
},
{
"enter": 9,
"entry_point": "Allocate an interrupt line for a managed device. (Relevant to 'irq_handler')",
"file": 0,
"source": "ldv_emg_request_irq(irq_id, &irq_handler, 0UL, \"ldv interrupt\", data);",
"source node": 28,
"start line": 35,
"target node": 29,
"thread": 3
},
{
"action": 2,
"assumption": "arg0 == 100U; arg4 == 0LL;",
"assumption scope": 9,
"file": 1,
"source": "irqreturn_t (*ldv_5_callback_handler)(int, void *);",
"source node": 29,
"start line": 128,
"target node": 30,
"thread": 3
},
{
"action": 2,
"file": 1,
"source": "void *ldv_5_data_data;",
"source node": 30,
"start line": 129,
"target node": 31,
"thread": 3
},
{
"action": 2,
"file": 1,
"source": "int ldv_5_line_line;",
"source node": 31,
"start line": 130,
"target node": 32,
"thread": 3
},
{
"action": 2,
"file": 1,
"source": "irqreturn_t (*ldv_5_thread_thread)(int, void *);",
"source node": 32,
"start line": 131,
"target node": 33,
"thread": 3
},
{
"action": 5,
"file": 1,
"source": "ldv_5_line_line = (int)arg0;",
"source node": 33,
"start line": 137,
"target node": 34,
"thread": 3
},
{
"action": 5,
"file": 1,
"source": "ldv_5_callback_handler = arg1;",
"source node": 34,
"start line": 138,
"target node": 35,
"thread": 3
},
{
"action": 5,
"file": 1,
"source": "ldv_5_thread_thread = (irqreturn_t (*)(int, void *))0;",
"source node": 35,
"start line": 139,
"target node": 36,
"thread": 3
},
{
"action": 5,
"file": 1,
"source": "ldv_5_data_data = arg4;",
"source node": 36,
"start line": 140,
"target node": 37,
"thread": 3
},
{
"action": 6,
"enter": 11,
"file": 1,
"source": "ldv_dispatch_irq_register_5_3(ldv_5_line_line, ldv_5_callback_handler, ldv_5_thread_thread, ldv_5_data_data);",
"source node": 37,
"start line": 144,
"target node": 38,
"thread": 3
},
{
"assumption": "arg0 == 100; arg3 == 0LL;",
"assumption scope": 11,
"file": 1,
"source": "struct ldv_struct_interrupt_scenario_2 *cf_arg_2;",
"source node": 38,
"start line": 95,
"target node": 39,
"thread": 3
},
{
"enter": 2,
"file": 1,
"source": "cf_arg_2 = (struct ldv_struct_interrupt_scenario_2 *)ldv_xmalloc(40UL);",
"source node": 39,
"start line": 94,
"target node": 40,
"thread": 3
},
{
"assumption": "res == 4LL; size == 4UL;",
"assumption scope": 2,
"file": 3,
"source": "void *res;",
"source node": 40,
"start line": 68,
"target node": 41,
"thread": 3
},
{
"assumption": "tmp == 4LL;",
"assumption scope": 2,
"file": 3,
"source": "res = malloc(size);",
"source node": 41,
"start line": 68,
"target node": 42,
"thread": 3
},
{
"condition": true,
"file": 3,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 42,
"start line": 69,
"target node": 43,
"thread": 3
},
{
"condition": true,
"enter": 3,
"file": 3,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 43,
"start line": 70,
"target node": 44,
"thread": 3
},
{
"assumption": "ptr == 4LL;",
"assumption scope": 3,
"file": 4,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 44,
"start line": 22,
"target node": 45,
"thread": 3
},
{
"file": 3,
"return": 2,
"source": "return res;",
"source node": 45,
"start line": 71,
"target node": 46,
"thread": 3
},
{
"file": 1,
"source": "cf_arg_2->arg0 = arg0;",
"source node": 46,
"start line": 95,
"target node": 47,
"thread": 3
},
{
"file": 1,
"source": "cf_arg_2->arg1 = arg1;",
"source node": 47,
"start line": 96,
"target node": 48,
"thread": 3
},
{
"file": 1,
"source": "cf_arg_2->arg2 = arg2;",
"source node": 48,
"start line": 97,
"target node": 49,
"thread": 3
},
{
"file": 1,
"source": "cf_arg_2->arg3 = arg3;",
"source node": 49,
"start line": 98,
"target node": 50,
"thread": 3
},
{
"enter": 12,
"entry_point": "Handle an interrupt. (Relevant to 'irq_handler')",
"file": 1,
"source": "ldv_interrupt_scenario_2((void *)cf_arg_2);",
"source node": 50,
"start line": 99,
"target node": 51,
"thread": 2
},
{
"action": 2,
"assumption": "arg0 == 2LL;",
"assumption scope": 12,
"file": 1,
"source": "irqreturn_t (*ldv_2_callback_handler)(int, void *);",
"source node": 51,
"start line": 230,
"target node": 52,
"thread": 2
},
{
"action": 2,
"file": 1,
"source": "void *ldv_2_data_data;",
"source node": 52,
"start line": 231,
"target node": 53,
"thread": 2
},
{
"action": 2,
"file": 1,
"source": "int ldv_2_line_line;",
"source node": 53,
"start line": 232,
"target node": 54,
"thread": 2
},
{
"action": 2,
"file": 1,
"source": "enum irqreturn ldv_2_ret_val_default;",
"source node": 54,
"start line": 233,
"target node": 55,
"thread": 2
},
{
"action": 2,
"file": 1,
"source": "irqreturn_t (*ldv_2_thread_thread)(int, void *);",
"source node": 55,
"start line": 234,
"target node": 56,
"thread": 2
},
{
"action": 2,
"file": 1,
"source": "struct ldv_struct_interrupt_scenario_2 *data___0;",
"source node": 56,
"start line": 235,
"target node": 57,
"thread": 2
},
{
"action": 2,
"assumption": "data___0 == 2LL;",
"assumption scope": 12,
"file": 1,
"source": "data___0 = (struct ldv_struct_interrupt_scenario_2 *)arg0;",
"source node": 57,
"start line": 237,
"target node": 58,
"thread": 2
},
{
"action": 7,
"condition": true,
"file": 1,
"source": "((unsigned long)data___0) != ((unsigned long)((struct ldv_struct_interrupt_scenario_2 *)0))",
"source node": 58,
"start line": 242,
"target node": 59,
"thread": 2
},
{
"action": 7,
"assumption": "ldv_2_line_line == 100;",
"assumption scope": 12,
"file": 1,
"source": "ldv_2_line_line = data___0->arg0;",
"source node": 59,
"start line": 243,
"target node": 60,
"thread": 2
},
{
"action": 7,
"file": 1,
"source": "ldv_2_callback_handler = data___0->arg1;",
"source node": 60,
"start line": 244,
"target node": 61,
"thread": 2
},
{
"action": 7,
"file": 1,
"source": "ldv_2_thread_thread = data___0->arg2;",
"source node": 61,
"start line": 245,
"target node": 62,
"thread": 2
},
{
"action": 7,
"assumption": "ldv_2_data_data == 0LL;",
"assumption scope": 12,
"file": 1,
"source": "ldv_2_data_data = data___0->arg3;",
"source node": 62,
"start line": 246,
"target node": 63,
"thread": 2
},
{
"action": 7,
"enter": 5,
"file": 1,
"source": "ldv_free((void *)data___0);",
"source node": 63,
"start line": 247,
"target node": 64,
"thread": 2
},
{
"file": 3,
"source": "free(s);",
"source node": 64,
"start line": 63,
"target node": 65,
"thread": 2
},
{
"file": 3,
"return": 5,
"source": "return;",
"source node": 65,
"start line": 64,
"target node": 66,
"thread": 2
},
{
"action": 8,
"file": 1,
"source": "ldv_switch_to_interrupt_context();",
"source node": 66,
"start line": 253,
"target node": 67,
"thread": 2
},
{
"action": 8,
"enter": 14,
"file": 0,
"original file": 1,
"original start line": 255,
"source": "ldv_2_ret_val_default = irq_handler(ldv_2_line_line, ldv_2_data_data);",
"source node": 67,
"start line": 29,
"target node": 68,
"thread": 2
},
{
"enter": 15,
"file": 0,
"source": "ldv_invoke_reached();",
"source node": 68,
"start line": 29,
"target node": 69,
"thread": 2
},
{
"enter": 16,
"file": 2,
"source": "ldv_assert_linux_emg_test(0);",
"source node": 69,
"start line": 44,
"target node": 70,
"thread": 2
},
{
"assumption": "expr == 0;",
"assumption scope": 16,
"condition": true,
"file": 6,
"source": "expr == 0",
"source node": 70,
"start line": 4,
"target node": 71,
"thread": 2
},
{
"file": 6,
"source": "__VERIFIER_error();",
"source node": 71,
"start line": 5,
"target node": 72,
"thread": 2
}
],
"entry node": 0,
"files": [
"ext-modules/irq_invoke.c",
"klever-core-work-dir/tests/irq/5d600ce/linux-emg-test/avtg/ext-modules/irq_invoke.ko/linux:emg:test/weaver/.tmp_irq_invoke.c.aux",
"linux/emg/test_model.c",
"verifier/memory.c",
"linux/err.c",
"verifier/nondet.c",
"klever-core-work-dir/tests/irq/5d600ce/linux-emg-test/vtg/ext-modules/irq_invoke.ko/linux:emg:test/rsb/bug kind funcs.c"
],
"funcs": [
"ldv_main_6",
"ldv_dispatch_insmod_register_6_3",
"ldv_xmalloc",
"ldv_is_err",
"ldv_insmod_3",
"ldv_free",
"ldv_insmod_ldv_init_3_6",
"ldv_init",
"ldv_request_irq_5",
"ldv_emg_request_irq",
"ldv_undef_int",
"ldv_dispatch_irq_register_5_3",
"ldv_interrupt_scenario_2",
"ldv_interrupt_scenario_handler_2_5",
"irq_handler",
"ldv_invoke_reached",
"ldv_assert_linux_emg_test",
"ldv_dispatch_insmod_deregister_6_2",
"ldv_dispatch_irq_deregister_4_1",
"ldv_emg_free_irq",
"ldv_insmod_ldv_exit_3_2",
"ldv_interrupt_scenario_thread_2_3",
"main",
"ERR_PTR",
"PTR_ERR",
"IS_ERR",
"IS_ERR_OR_NULL",
"ldv_free_irq_6"
],
"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,
null
]
],
"violation nodes": [
72
]
}
    (1-1/1)