./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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.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"
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain ONLY for:
[Info] dev_err, ldv_count_1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, tmp, tmp, tmp, tmp, tmp, tmp, tmp, ptr, tmp, exp, ldv_func_arg2, tmp, ldv_func_arg2, tmp, ptr, tmp, ptr, tmp, ldv_s_s3c_hwmon_driver_platform_driver, tmp___0, res_s3c_hwmon_probe_10, tmp, tmp___1, var_group1, tmp, i, i, ret, hwmon, tmp___1, tmp___3, pdata, cfg, dev, dev, ret, attr, channel, dev, buf, ret, dev, buf, hwmon, ret, channel, data, tmp, size, tmp, size, flags, tmp___2, size, tmp, size, res, tmp, tmp___0, tmp___1, tmp___2, cond
[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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1157:3-1157:53)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1157:3-1157:53)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1157:3-1157:53)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1213:5-1213:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1132:3-1132:66)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:877:3-877:37)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:877:3-877:37)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1356:10-1356:25)
[Warning][Unknown] lval (& pdev)->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 (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:839:6-839:29)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:840:8-840:27)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:840:8-840:27)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:841:3-841:40)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1284:11-1284:40)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:841:3-841:40)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:841:3-841:40)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:841:3-841:40)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:834:1-834:1)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:842:10-842:13)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:844:11-844:21)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1356:10-1356:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1134:3-1134:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1134:3-1134:35)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:921:3-921:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1138:3-1138:98)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1138:3-1138:98)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1013:3-1013:83)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1013:3-1013:83)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1370:3-1370:9)
[Warning][Unknown] lval (& attrs)->in.dev_attr points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1370:3-1370:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1014:3-1014:86)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1014:3-1014:86)
[Warning][Unknown] lval (& attrs)->label.dev_attr points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1370:3-1370:9)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1015:3-1015:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1145:3-1145:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1145:3-1145:44)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1146:3-1146:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1146:3-1146:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1199:5-1199:57)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1032:3-1032:59)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1035:5-1035:80)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1035:5-1035:80)
[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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1353:10-1353: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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1353:10-1353:33)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1042:5-1042:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1042:5-1042:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1046:3-1046:43)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:884:3-884:37)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:884:3-884:37)
[Warning][Unknown] lval (& pdev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1363:3-1363:9)
[Warning][Unknown] lval (& hwmon)->lock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1349:3-1349:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1048:3-1048:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1057:3-1057:38)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1057:3-1057: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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:915:11-915:13)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1062:3-1062:55)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1062:3-1062:55)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1373:10-1373:43)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:839:6-839:29)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:840:8-840:27)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:840:8-840:27)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:841:3-841: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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1284:11-1284: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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:841:3-841: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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:841:3-841: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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:841:3-841: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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:834:1-834: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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:842:10-842:13)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:844:11-844:21)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1373:10-1373:43)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1080:5-1081:16)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1080:5-1081:16)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1367:10-1367: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-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1367:10-1367:33)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1089:3-1090:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1089:3-1090:33)
[Info][Imprecise] Invalidating expressions: (char *)(& attrs->in_name) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:980:3-980:67)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:981:3-981:21)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:982:3-982:24)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:983:3-983:62)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:984:3-984:34)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:985:3-985:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:986:3-986:91)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:986:3-986:91)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1256:3-1256:82)
[Warning][Unknown] lval (& attrs)->in points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1256:3-1256:82)
[Warning][Unknown] lval (& attr)->dev_attr points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1256:3-1256:82)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1085:5-1085:81)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1085:5-1085:81)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1051:5-1051:74)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1051:5-1051:74)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1296:11-1296:49)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1296:11-1296:49)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1053:5-1053:24)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1065:5-1065:83)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1065:5-1065:83)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1067:5-1067:24)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1118:3-1118:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1118:3-1118:35)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1164:3-1164:49)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1164:3-1164:49)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1164:3-1164:49)
[Warning][Deadcode] Function 's3c_hwmon_read_ch' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:897:1-911:1)
[Warning][Deadcode] Function 's3c_hwmon_ch_show' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:924:1-956:1)
[Warning][Deadcode] Function 's3c_hwmon_label_show' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:957:1-973:1)
[Warning][Deadcode] Function 'ldv_device_create_file_6' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1260:1-1267:1)
[Warning][Deadcode] Function 'ldv__builtin_expect' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1275:1-1280:1)
[Warning][Deadcode] Function 'ldv_err_ptr' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1287:1-1292:1)
[Warning][Deadcode] Function 'ldv_is_err_or_null' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1299:1-1316:1)
[Warning][Deadcode] Function 'ldv_sysfs' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1319:1-1325:1)
[Warning][Deadcode] Function 'dev_printk' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1359:1-1361:1)
[Warning][Deadcode] Function 'mutex_lock_interruptible_nested' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1391:1-1393:1)
[Warning][Deadcode] Function 'mutex_unlock' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1394:1-1396:1)
[Warning][Deadcode] Function 's3c_adc_read' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1405:1-1407:1)
[Warning][Deadcode] Function 'ldv_device_create_file_5' has dead code:
  on line 1257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1257-1257)
[Warning][Deadcode] Function 'ldv_device_create_file_dev_attr_of_sensor_device_attribute' has dead code:
  on line 1339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1339-1339)
[Warning][Deadcode] Function 'ldv_error' has dead code:
  on line 1274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1274-1274)
[Warning][Deadcode] Function 's3c_hwmon_create_attr' has dead code:
  on lines 987..989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:987-989)
  on lines 992..1002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:992-1002)
  on line 1007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1007-1007)
[Warning][Deadcode] Function 's3c_hwmon_probe' has dead code:
  on lines 1091..1092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1091-1092)
  on line 1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1094-1094)
  on lines 1097..1098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1097-1098)
  on line 1100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1100-1100)
  on line 1116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1116-1116)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 183
  dead: 70 (45 in uncalled functions)
  total lines: 253
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:12:73-12:74)
[Warning][Deadcode][CWE-570] condition 'ret != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1058:7-1058:15)
[Warning][Deadcode][CWE-571] condition 'ldv_call_dev_attr_of_sensor_device_attribute == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1330:7-1330:56)
[Warning][Deadcode][CWE-570] condition 'ldv_count_1 >= ldv_count_2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_drivers-hwmon-s3c-hwmon-ko--130_7a--af3071a-1.i:1333:9-1333:35)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
