Project

General

Profile

Download (17.3 KB)

Bug #8981 » error trace.json

Evgeny Novikov, 06/21/2018 10:32 AM

 
{
"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."
],
"callback actions": [
4
],
"edges": [
{
"assumption": "__ldv_in_interrupt_context == 0;",
"end line": 25,
"file": 0,
"source": "static bool __ldv_in_interrupt_context = 0;",
"source node": 0,
"start line": 25,
"target node": 1,
"thread": 0
},
{
"end line": 166,
"enter": 0,
"entry_point": "Entry point 'main'",
"file": 1,
"line": 166,
"source": "Begin program execution",
"source node": 1,
"start line": 166,
"target node": 2,
"thread": 1
},
{
"end line": 168,
"enter": 1,
"entry_point": "Main entry point function.",
"file": 1,
"source": "ldv_main_3((void *)0);",
"source node": 2,
"start line": 168,
"target node": 3,
"thread": 3
},
{
"action": 0,
"end line": 143,
"file": 1,
"source": "ldv_initialize();",
"source node": 3,
"start line": 143,
"target node": 4,
"thread": 3
},
{
"action": 1,
"end line": 147,
"enter": 2,
"file": 1,
"source": "ldv_dispatch_insmod_register_3_3();",
"source node": 4,
"start line": 147,
"target node": 5,
"thread": 3
},
{
"end line": 77,
"file": 1,
"source": "struct ldv_struct_main_3 *cf_arg_2;",
"source node": 5,
"start line": 77,
"target node": 6,
"thread": 3
},
{
"end line": 77,
"enter": 3,
"file": 1,
"source": "cf_arg_2 = (struct ldv_struct_main_3 *)ldv_xmalloc(4UL);",
"source node": 6,
"start line": 77,
"target node": 7,
"thread": 3
},
{
"assumption": "size == 4UL;",
"assumption scope": 3,
"end line": 69,
"file": 2,
"source": "void *res;",
"source node": 7,
"start line": 69,
"target node": 8,
"thread": 3
},
{
"end line": 69,
"file": 2,
"source": "res = malloc(size);",
"source node": 8,
"start line": 69,
"target node": 9,
"thread": 3
},
{
"end line": 71,
"file": 2,
"source": "[__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));]",
"source node": 9,
"start line": 71,
"target node": 10,
"thread": 3
},
{
"end line": 72,
"enter": 4,
"file": 2,
"source": "[__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);]",
"source node": 10,
"start line": 72,
"target node": 11,
"thread": 3
},
{
"end line": 22,
"file": 3,
"return": 4,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 11,
"start line": 22,
"target node": 12,
"thread": 3
},
{
"end line": 74,
"file": 2,
"return": 3,
"source": "return res;",
"source node": 12,
"start line": 74,
"target node": 13,
"thread": 3
},
{
"end line": 78,
"enter": 5,
"entry_point": "Initialize or exit module.",
"file": 1,
"source": "ldv_insmod_2((void *)cf_arg_2);",
"source node": 13,
"start line": 78,
"target node": 14,
"thread": 2
},
{
"action": 2,
"end line": 85,
"file": 1,
"source": "void (*ldv_2_exit_default)(void);",
"source node": 14,
"start line": 85,
"target node": 15,
"thread": 2
},
{
"action": 2,
"end line": 86,
"file": 1,
"source": "int (*ldv_2_ldv_init_default)(void);",
"source node": 15,
"start line": 86,
"target node": 16,
"thread": 2
},
{
"action": 2,
"end line": 87,
"file": 1,
"source": "int ldv_2_ret_default;",
"source node": 16,
"start line": 87,
"target node": 17,
"thread": 2
},
{
"action": 3,
"end line": 94,
"enter": 6,
"file": 1,
"source": "ldv_free(arg0);",
"source node": 17,
"start line": 94,
"target node": 18,
"thread": 2
},
{
"end line": 64,
"file": 2,
"source": "free(s);",
"source node": 18,
"start line": 64,
"target node": 19,
"thread": 2
},
{
"end line": 65,
"file": 2,
"return": 6,
"source": "return;",
"source node": 19,
"start line": 65,
"target node": 20,
"thread": 2
},
{
"action": 4,
"end line": 99,
"enter": 8,
"file": 4,
"original file": 1,
"original start line": 99,
"source": "ldv_2_ret_default = ldv_init();",
"source node": 20,
"start line": 23,
"target node": 21,
"thread": 2
},
{
"end line": 23,
"file": 4,
"note": "int **buf ;",
"source": "int **buf;",
"source node": 21,
"start line": 23,
"target node": 22,
"thread": 2
},
{
"end line": 24,
"file": 4,
"note": "int i ;",
"source": "int i;",
"source node": 22,
"start line": 24,
"target node": 23,
"thread": 2
},
{
"end line": 25,
"enter": 9,
"file": 4,
"note": "tmp = kzalloc(40UL, 208U);",
"source": "kzalloc(40UL, 208U) = kzalloc(40UL, 208U);",
"source node": 23,
"start line": 25,
"target node": 24,
"thread": 2
},
{
"end line": 280,
"enter": 10,
"file": 1,
"note": "tmp = ldv_kzalloc(size, flags);",
"source": "ldv_kzalloc(size, flags) = ldv_kzalloc(size, flags);",
"source node": 24,
"start line": 280,
"target node": 25,
"thread": 2
},
{
"assumption": "size == 40UL; flags == 208U;",
"assumption scope": 10,
"end line": 23,
"file": 5,
"note": "void *res ;",
"source": "void *res;",
"source node": 25,
"start line": 23,
"target node": 26,
"thread": 2
},
{
"end line": 25,
"file": 5,
"source": "ldv_check_alloc_flags(flags);",
"source node": 26,
"start line": 25,
"target node": 27,
"thread": 2
},
{
"end line": 26,
"enter": 11,
"file": 5,
"note": "res = ldv_zalloc(size);",
"source": "res = ldv_zalloc(size);",
"source node": 27,
"start line": 26,
"target node": 28,
"thread": 2
},
{
"end line": 59,
"enter": 12,
"file": 2,
"note": "tmp = ldv_calloc(1UL, size);",
"source": "ldv_calloc(1UL, size) = ldv_calloc(1UL, size);",
"source node": 28,
"start line": 59,
"target node": 29,
"thread": 2
},
{
"assumption": "nmemb == 1UL; size == 40UL;",
"assumption scope": 12,
"end line": 45,
"file": 2,
"note": "void *res ;",
"source": "void *res;",
"source node": 29,
"start line": 45,
"target node": 30,
"thread": 2
},
{
"condition": true,
"end line": 45,
"enter": 13,
"file": 2,
"source": "ldv_undef_int() != 0",
"source node": 30,
"start line": 45,
"target node": 31,
"thread": 2
},
{
"end line": 43,
"file": 6,
"return": 13,
"source": "return __VERIFIER_nondet_int();",
"source node": 31,
"start line": 43,
"target node": 32,
"thread": 2
},
{
"assumption": "(*((signed long long int *)tmp)) == 0LL;",
"assumption scope": 12,
"end line": 46,
"file": 2,
"note": "res = tmp;",
"source": "res = calloc(nmemb, size);",
"source node": 32,
"start line": 46,
"target node": 33,
"thread": 2
},
{
"end line": 48,
"file": 2,
"source": "[__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));]",
"source node": 33,
"start line": 48,
"target node": 34,
"thread": 2
},
{
"end line": 49,
"enter": 4,
"file": 2,
"source": "[__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);]",
"source node": 34,
"start line": 49,
"target node": 35,
"thread": 2
},
{
"assumption": "(*((signed long long int *)ptr)) == 0LL;",
"assumption scope": 4,
"end line": 22,
"file": 3,
"return": 4,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 35,
"start line": 22,
"target node": 36,
"thread": 2
},
{
"end line": 51,
"file": 2,
"note": "return (res);",
"return": 12,
"source": "return res;",
"source node": 36,
"start line": 51,
"target node": 37,
"thread": 2
},
{
"end line": 59,
"file": 2,
"note": "return (tmp);",
"return": 11,
"source": "return tmp;",
"source node": 37,
"start line": 59,
"target node": 38,
"thread": 2
},
{
"end line": 26,
"file": 5,
"note": "res = ldv_zalloc(size);",
"source": "res = ldv_zalloc(size);",
"source node": 38,
"start line": 26,
"target node": 39,
"thread": 2
},
{
"end line": 27,
"enter": 14,
"file": 5,
"source": "ldv_after_alloc(res);",
"source node": 39,
"start line": 27,
"target node": 40,
"thread": 2
},
{
"assumption": "(*((signed long long int *)res)) == 0LL;",
"assumption scope": 14,
"end line": 20,
"file": 7,
"return": 14,
"source": "return;",
"source node": 40,
"start line": 20,
"target node": 41,
"thread": 2
},
{
"end line": 29,
"file": 5,
"note": "return (res);",
"return": 10,
"source": "return res;",
"source node": 41,
"start line": 29,
"target node": 42,
"thread": 2
},
{
"end line": 280,
"file": 1,
"note": "return (tmp);",
"return": 9,
"source": "return tmp;",
"source node": 42,
"start line": 280,
"target node": 43,
"thread": 2
},
{
"end line": 25,
"file": 4,
"note": "buf = (int **)tmp;",
"source": "buf = (int **)tmp;",
"source node": 43,
"start line": 25,
"target node": 44,
"thread": 2
},
{
"condition": true,
"end line": 26,
"file": 4,
"source": "((unsigned long)buf) != ((unsigned long)((int **)0))",
"source node": 44,
"start line": 26,
"target node": 45,
"thread": 2
},
{
"end line": 29,
"file": 4,
"source": "i = *(*(buf + 9UL));",
"source node": 45,
"start line": 29,
"target node": 46,
"thread": 2,
"warn": "Field with 8 byte size can't be read from offset 72 byte of object 40 byte size"
}
],
"entry node": 0,
"files": [
"linux/ldv/common.c",
"klever-core-work-dir/0/tests/generic/memory/generic-memory/vtg/ext-modules/generic/memory/zalloc.ko/generic:memory/weaver/.tmp_zalloc.c.aux",
"verifier/memory.c",
"linux/err.c",
"ext-modules/generic/memory/zalloc.c",
"linux/mm/kzalloc.c",
"verifier/nondet.c",
"generic/memory.c"
],
"funcs": [
"main",
"ldv_main_3",
"ldv_dispatch_insmod_register_3_3",
"ldv_xmalloc",
"ldv_is_err",
"ldv_insmod_2",
"ldv_free",
"ldv_insmod_ldv_init_2_5",
"ldv_init",
"kzalloc",
"ldv_kzalloc",
"ldv_zalloc",
"ldv_calloc",
"ldv_undef_int",
"ldv_after_alloc",
"ldv_switch_to_interrupt_context",
"ldv_switch_to_process_context",
"ldv_dispatch_insmod_deregister_3_2",
"ERR_PTR",
"PTR_ERR",
"IS_ERR",
"IS_ERR_OR_NULL",
"alloc_pages",
"ldv___get_free_pages_6",
"kmalloc",
"kmalloc_node",
"kcalloc",
"ldv_kmalloc_array_10",
"kmem_cache_zalloc",
"ldv_kmem_cache_alloc_12",
"kzalloc_node",
"ldv_kfree_15"
],
"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,
null
]
],
"violation nodes": [
46
]
}
(2-2/3)