./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-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.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] 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_mutex_cred_guard_mutex_of_signal_struct, ldv_mutex_lock, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r, top, expression, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp, tmp___1, size, tmp, p, tmp___0, cond, tmp, nondetermined, atomic_value_after_dec, is_mutex_held_by_another_thread, nondetermined, nondetermined, nondetermined, atomic_value_after_dec, is_mutex_held_by_another_thread, nondetermined, nondetermined, nondetermined, atomic_value_after_dec, is_mutex_held_by_another_thread, nondetermined, nondetermined, nondetermined, atomic_value_after_dec, is_mutex_held_by_another_thread, nondetermined, nondetermined, exp, ldv_func_arg1, ldv_func_arg1, ldv_func_arg1, ldv_func_arg1, ldv_func_arg1, ldv_func_arg1, ldv_func_arg1, ldv_func_arg1, ldv_func_res, tmp, tmp___0, ldv_func_arg1, ldv_func_arg1, ldv_func_arg1, tmp, tmp___2, tmp___0, tmp___1, tmp___3, tmp, i, i, pmic, tmp, tmp___2, i2c, err, err, dev, idx, dev, func, adap, adap, tmp, data, tmp, tmp
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2259:3-2259:32)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2654:3-2654:48)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2950:3-2950:9)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2655:3-2655:28)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3191:3-3191:9)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2656:3-2656:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2260:3-2260:69)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2262:5-2262:87)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2262:5-2262:87)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2265:3-2265:34)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2662:3-2662:50)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3008:3-3008:9)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2663:3-2663:30)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3198:3-3198:9)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2664:3-2664:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2276:3-2276:33)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2670:3-2670:48)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2671:3-2671:28)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2672:3-2672:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2277:3-2277:93)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2279:5-2279:87)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2279:5-2279:87)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2282:3-2282:35)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2678:3-2678:50)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2679:3-2679:30)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2680:3-2680:9)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2417:3-2417:68)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2417:3-2417:68)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2417:3-2417:68)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2225:3-2225:36)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3166:10-3166:25)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:19:144-19:147)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3160:6-3160:30)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3160:39-3160:40)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3161:8-3161:25)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3161:8-3161:25)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3162:3-3162:38)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2175:3-2175:76)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2694:11-2694:15)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2176:11-2176:15)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3162:3-3162:38)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3157:1-3157:1)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3163:10-3163:11)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3166:10-3166:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2388:3-2388:38)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2476:7-2476:28)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2319:3-2319:67)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2320:3-2320:56)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2320:3-2320:56)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2248:3-2248:36)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2241:3-2241:47)
[Warning][Imprecise][Call] Function pointer *((adap->algo)->functionality) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2241:3-2241:47)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2241:3-2241:47)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2322:13-2322:16)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2325:3-2325:50)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3173:10-3173:25)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:19:144-19:147)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3160:6-3160:30)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3160:39-3160:40)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3161:8-3161:25)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3161:8-3161:25)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3162:3-3162:38)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2175:3-2175:76)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2694:11-2694:15)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2176:11-2176:15)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3162:3-3162:38)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3157:1-3157:1)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3163:10-3163:11)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3173:10-3173:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2326:3-2326:36)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2328:13-2328:17)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2331:3-2331:21)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2332:3-2332:51)
[Warning][Unknown] lval (& pmic)->mtx points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3146:3-3146:9)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2333:3-2333:8)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2336:3-2336:26)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2340:5-2340:25)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2338:5-2338:69)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2342:3-2342:36)
[Info][Unsound] Unknown address in {&config} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2343:3-2344:82)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2343:3-2344:82)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2343:3-2344:82)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2343:3-2344:82)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2343:3-2344:82)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3212:10-3212:50)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3212:10-3212:50)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2345:3-2345:48)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2353:3-2353:12)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2361:3-2361:40)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2232:3-2232:36)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:136-22:139)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3170:10-3170:33)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3170:10-3170:33)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2347:5-2347:104)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:136-22:139)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3150:10-3150:33)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3150:10-3150:33)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2348:5-2348:51)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2169:11-2169:22)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2169:11-2169:22)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2349:5-2349:24)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2349:5-2349:24)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2366:3-2366:38)
[Warning][Unknown] lval (& i2c)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3215:3-3215:9)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2368:3-2368:12)
[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2375:11-2375:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2466:9-2466:30)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2424:3-2424:40)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2424:3-2424:40)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2424:3-2424:40)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:12:1-12:234)
[Warning][Deadcode] Function 'ldv_mutex_lock_1' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2591:1-2598:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_2' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2599:1-2606:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_3' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2607:1-2614:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_4' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2615:1-2626:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_5' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2627:1-2634:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_6' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2635:1-2642:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_7' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2643:1-2650:1)
[Warning][Deadcode] Function 'ldv_error' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2684:1-2689:1)
[Warning][Deadcode] Function 'ldv__builtin_trap' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2697:1-2703:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2705:1-2720:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2721:1-2736:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_cred_guard_mutex_of_signal_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2737:1-2747:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2748:1-2763:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_cred_guard_mutex_of_signal_struct' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2764:1-2780:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_cred_guard_mutex_of_signal_struct' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2781:1-2795:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_cred_guard_mutex_of_signal_struct' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2796:1-2806:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2808:1-2823:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2824:1-2839:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2840:1-2850:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2851:1-2866:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_lock' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2867:1-2882:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_lock' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2883:1-2897:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2898:1-2908:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_mtx_of_isl_pmic' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2910:1-2925:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_mtx_of_isl_pmic' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2926:1-2941:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_mtx_of_isl_pmic' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2953:1-2968:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_mtx_of_isl_pmic' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2969:1-2984:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_mtx_of_isl_pmic' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2985:1-2999:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_interruptible_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3012:1-3027:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_killable_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3028:1-3043:1)
[Warning][Deadcode] Function 'ldv_mutex_lock_mutex_of_device' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3044:1-3054:1)
[Warning][Deadcode] Function 'ldv_mutex_trylock_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3055:1-3070:1)
[Warning][Deadcode] Function 'ldv_atomic_dec_and_mutex_lock_mutex_of_device' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3071:1-3086:1)
[Warning][Deadcode] Function 'ldv_mutex_is_locked_mutex_of_device' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3087:1-3101:1)
[Warning][Deadcode] Function 'ldv_mutex_unlock_mutex_of_device' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3102:1-3112:1)
[Warning][Deadcode] Function 'mutex_trylock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3194:1-3196:1)
[Warning][Deadcode] Function 'kfree' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3218:1-3220:1)
[Warning][Deadcode] Function 'ldv_check_final_state' has dead code:
  on line 3128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3128-3128)
  on line 3132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3132-3132)
  on line 3136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3136-3136)
  on line 3140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3140-3140)
[Warning][Deadcode] Function 'ldv_mutex_lock_mtx_of_isl_pmic' has dead code:
  on line 2947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2947-2947)
[Warning][Deadcode] Function 'ldv_mutex_unlock_mtx_of_isl_pmic' has dead code:
  on line 3005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3005-3005)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 235
  dead: 197 (191 in uncalled functions)
  total lines: 432
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_mutex_of_device == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3138:7-3138:37)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_mtx_of_isl_pmic == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2945:7-2945:37)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2529:9-2529:34)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2536:9-2536:34)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2543:9-2543:34)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2550:9-2550:34)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_mtx_of_isl_pmic == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3003:7-3003:37)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_2 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2568:9-2568:34)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_0 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:2488:7-2488:32)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_cred_guard_mutex_of_signal_struct == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3126:7-3126:55)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_lock == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3130:7-3130:26)
[Warning][Deadcode][CWE-571] condition 'ldv_mutex_mtx_of_isl_pmic == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--regulator--isl6271a-regulator.ko-main.cil.out.i:3134:7-3134:37)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
[Warning][Unsound][Call] No suitable function to call
