Project

General

Profile

Download (8.24 KB)

Feature #8496 ยป error-trace.json

Evgeny Novikov, 10/11/2017 02:03 PM

 
{
"actions": [
"Initialize rule models.",
"Start environment model scenarios.",
"Declare auxiliary variables.",
"Trigger module initialization.",
"Initialize the module after insmod with 'init' function. Invoke callback init from INSMOD."
],
"callback actions": [
4
],
"edges": [
{
"enter": 9,
"entry_point": "Entry point 'main'",
"file": 0,
"line": 176,
"source": "Begin program execution",
"source node": 0,
"target node": 1,
"thread": 1
},
{
"enter": 0,
"entry_point": "Main entry point function.",
"file": 0,
"source": "ldv_main_3((void *)0);",
"source node": 1,
"start line": 178,
"target node": 2,
"thread": 3
},
{
"action": 0,
"file": 0,
"source": "ldv_initialize();",
"source node": 2,
"start line": 152,
"target node": 3,
"thread": 3
},
{
"action": 1,
"enter": 1,
"file": 0,
"source": "ldv_dispatch_insmod_register_3_3();",
"source node": 3,
"start line": 156,
"target node": 4,
"thread": 3
},
{
"file": 0,
"source": "struct ldv_struct_main_3 *cf_arg_2;",
"source node": 4,
"start line": 85,
"target node": 5,
"thread": 3
},
{
"enter": 2,
"file": 0,
"source": "cf_arg_2 = (struct ldv_struct_main_3 *)ldv_xmalloc(4UL);",
"source node": 5,
"start line": 85,
"target node": 6,
"thread": 3
},
{
"assumption": "size == 4UL;",
"assumption scope": 2,
"file": 1,
"source": "void *res;",
"source node": 6,
"start line": 68,
"target node": 7,
"thread": 3
},
{
"file": 1,
"source": "res = malloc(size);",
"source node": 7,
"start line": 68,
"target node": 8,
"thread": 3
},
{
"condition": true,
"file": 1,
"source": "__VERIFIER_assume((unsigned long)res != (unsigned long)((void *)0));",
"source node": 8,
"start line": 69,
"target node": 9,
"thread": 3
},
{
"condition": true,
"enter": 3,
"file": 1,
"source": "__VERIFIER_assume(ldv_is_err((void const *)res) == 0L);",
"source node": 9,
"start line": 70,
"target node": 10,
"thread": 3
},
{
"file": 2,
"return": 3,
"source": "return (unsigned long)ptr > 4294967295UL;",
"source node": 10,
"start line": 22,
"target node": 11,
"thread": 3
},
{
"file": 1,
"return": 2,
"source": "return res;",
"source node": 11,
"start line": 71,
"target node": 12,
"thread": 3
},
{
"enter": 4,
"entry_point": "Initialize or exit module.",
"file": 0,
"source": "ldv_insmod_2((void *)cf_arg_2);",
"source node": 12,
"start line": 86,
"target node": 13,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "void (*ldv_2_exit_default)(void);",
"source node": 13,
"start line": 93,
"target node": 14,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "int (*ldv_2_init_default)(void);",
"source node": 14,
"start line": 94,
"target node": 15,
"thread": 2
},
{
"action": 2,
"file": 0,
"source": "int ldv_2_ret_default;",
"source node": 15,
"start line": 95,
"target node": 16,
"thread": 2
},
{
"action": 3,
"enter": 5,
"file": 0,
"source": "ldv_free(arg0);",
"source node": 16,
"start line": 102,
"target node": 17,
"thread": 2
},
{
"file": 1,
"source": "free(s);",
"source node": 17,
"start line": 63,
"target node": 18,
"thread": 2
},
{
"file": 1,
"return": 5,
"source": "return;",
"source node": 18,
"start line": 64,
"target node": 19,
"thread": 2
},
{
"action": 4,
"enter": 7,
"file": 3,
"original file": 0,
"original start line": 107,
"source": "ldv_2_ret_default = init();",
"source node": 19,
"start line": 22,
"target node": 20,
"thread": 2
},
{
"file": 3,
"note": "int *var1 ;",
"source": "int *var1;",
"source node": 20,
"start line": 22,
"target node": 21,
"thread": 2
},
{
"file": 3,
"note": "int var2 ;",
"source": "int var2;",
"source node": 21,
"start line": 23,
"target node": 22,
"thread": 2
},
{
"file": 3,
"note": "var1 = (int *)0;",
"source": "var1 = (int *)0;",
"source node": 22,
"start line": 24,
"target node": 23,
"thread": 2
},
{
"file": 3,
"source": "var2 = *var1;",
"source node": 23,
"start line": 25,
"target node": 24,
"thread": 2,
"warn": "NULL pointer dereference on read"
}
],
"entry node": 0,
"files": [
"klever-core-work-dir/tests/generic/memory/a135a98/generic-memory/vtg/ext-modules/null-ptr-dereference.ko/generic:memory/weaver/.tmp_null-ptr-dereference.c.aux",
"verifier/memory.c",
"linux/err.c",
"ext-modules/null-ptr-dereference.c"
],
"funcs": [
"ldv_main_3",
"ldv_dispatch_insmod_register_3_3",
"ldv_xmalloc",
"ldv_is_err",
"ldv_insmod_2",
"ldv_free",
"ldv_insmod_init_2_5",
"init",
"ldv_dispatch_insmod_deregister_3_2",
"main",
"ERR_PTR",
"PTR_ERR",
"IS_ERR",
"IS_ERR_OR_NULL",
"alloc_pages"
],
"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,
null
]
],
"violation nodes": [
24
]
}
    (1-1/1)