./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain ONLY for:
[Info] ldv_module_refcounter, pppox_protos, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, tmp, tmp, tmp, tmp, ldv_func_arg1, module, tmp, module, module_get_succeeded, module, module, tmp, tmp___0, tmp___1, var_group1, var_group2, var_pppox_create_4_p2, var_pppox_create_4_p3, tmp, protocol, tmp, net, sock, rc, cmd, __ret_pu, __pu_val, sk, sock, arg, tmp, rc, sk, proto_num, proto_num, pp, sk
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4915:3-4915:44)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4915:3-4915:44)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4915:3-4915:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4963:7-4963:89)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:12:1-12:196)
[Warning][Deadcode] Function 'lock_sock' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4719:1-4727:1)
[Warning][Deadcode] Function 'pppox_sk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4729:1-4734:1)
[Warning][Deadcode] Function 'register_pppox_proto' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4740:1-4757:1)
[Warning][Deadcode] Function 'unregister_pppox_proto' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4758:1-4770:1)
[Warning][Deadcode] Function 'pppox_unbind_sock' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4771:1-4784:1)
[Warning][Deadcode] Function 'pppox_ioctl' is uncalled: 40 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4785:1-4871:1)
[Warning][Deadcode] Function 'ldv_blast_assert' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4992:1-4997:1)
[Warning][Deadcode] Function 'ldv_module_get' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5000:1-5009:1)
[Warning][Deadcode] Function 'ldv_try_module_get' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5010:1-5027:1)
[Warning][Deadcode] Function 'ldv_module_put' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5028:1-5043:1)
[Warning][Deadcode] Function 'ldv_module_put_and_exit' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5044:1-5053:1)
[Warning][Deadcode] Function 'ldv_module_refcount' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5054:1-5059:1)
[Warning][Deadcode] Function 'ldv_try_module_get_1' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5072:1-5080:1)
[Warning][Deadcode] Function 'ldv_module_put_2' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5081:1-5089:1)
[Warning][Deadcode] Function 'ldv_undefined_int' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5098:1-5100:1)
[Warning][Deadcode] Function 'lock_sock_nested' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5101:1-5103:1)
[Warning][Deadcode] Function 'might_fault' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5104:1-5106:1)
[Warning][Deadcode] Function 'ppp_channel_index' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5108:1-5110:1)
[Warning][Deadcode] Function 'ppp_unregister_channel' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5111:1-5113:1)
[Warning][Deadcode] Function 'release_sock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5114:1-5116:1)
[Warning][Deadcode] Function 'kfree' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5125:1-5127:1)
[Warning][Deadcode] Function 'ldv_check_final_state' has dead code:
  on line 5065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5065-5065)
[Warning][Deadcode] Function 'main' has dead code:
  on line 4960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4960-4960)
[Warning][Deadcode] Function 'pppox_create' has dead code:
  on line 4895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4895-4895)
  on line 4897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4897-4897)
  on lines 4903..4904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4903-4904)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 40
  dead: 99 (93 in uncalled functions)
  total lines: 139
[Warning][Deadcode][CWE-571] condition '(unsigned long )pppox_protos[protocol] == (unsigned long )((struct pppox_proto  const  *)0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4885:7-4885:96)
[Warning][Deadcode][CWE-571] condition '(unsigned long )pppox_protos[protocol] == (unsigned long )((struct pppox_proto  const  *)0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:4891:7-4891:96)
[Warning][Deadcode][CWE-570] condition 'ldv_module_refcounter != 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-pppox.ko.cil.out.i:5063:7-5063:33)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
