./goblint --conf conf/svcomp25.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-data-race.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.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 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1084:5-1085:31 with factor 7
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1093:5-1097:5 with factor 7
[Info] Specification: CHECK( init(main()), LTL(G ! data-race) ) -> enabling soundness analyses "access, race"
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain ONLY for:
[Info] reach_error, fifo_push, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r, top, expression, i, got, p, tmp___0, tmp___1, i, q, self, wait, tmp, tmp___0, self, tmp, self, size, n, t, self, x, next, self, self, tmp, tmp___2, self, tmp, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1090:5-1090:20)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1090:5-1090:20)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1016:6-1016:54)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1016:6-1016:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1012:12-1012:77)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1031:10-1031:54)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1031:10-1031:54)
[Info][Unsound] Unknown address in {&(alloc@sid:60@tid:[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41])} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1032:9-1032:59)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1032:9-1032:59)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1035:5-1035:18)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1035:5-1035:18)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1036:5-1036:15)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1036:5-1036:15)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1038:9-1038:29)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1038:9-1038:29)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&(alloc@sid:60@tid:[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41])} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&(alloc@sid:60@tid:[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41])} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&(alloc@sid:60@tid:[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41])} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&(alloc@sid:60@tid:[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41])} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&(alloc@sid:60@tid:[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41])} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&(alloc@sid:60@tid:[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41])} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1085:9-1085:31)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1074:13-1074:40)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1074:13-1074:40)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1012:12-1012:77)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1076:6-1076:55)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1076:6-1076:55)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1077:10-1077:53)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1078:9-1078:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1078:9-1078:31)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1053:5-1053:34)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)old in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1055:5-1055:16)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1055:5-1055:16)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1080:12-1080:28)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1067:10-1067:80)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1069:9-1069:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1069:9-1069:31)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1059:6-1059:55)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1059:6-1059:55)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1060:5-1060:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1061:10-1061:53)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1062:14-1062:46)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1064:13-1064:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1064:13-1064:35)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1094:13-1094:39)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1095:9-1095:23)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1098:6-1098:52)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1098:6-1098:52)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1100:6-1100:52)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1100:6-1100:52)
[Info][Unsound] Unknown address in {&q} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1101:5-1101:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1101:5-1101:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1021:18-1021:42)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)self->head in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1023:9-1023:27)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1023:9-1023:27)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)self->head in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1026:5-1026:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1026:5-1026:23)
[Warning][Deadcode] Function '__bswap_16' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:63:1-67:1)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:68:1-72:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:73:15-77:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:78:1-82:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:83:1-87:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:88:1-92:1)
[Warning][Deadcode] Function 'fifo_size' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1042:1-1050:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 68
  dead: 12 (12 in uncalled functions)
  total lines: 80
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1093:9-1093:33)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1093:9-1093:33)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1093:9-1093:33)
[Warning][Deadcode][CWE-571] condition 'wait' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1074:13-1074:40)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1093:9-1093:33)
[Warning][Race] Memory location (alloc@sid:60@tid:[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41]).next (race with conf. 100): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1032:9-1032:59)
  write with thread:[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41] (conf. 100)  (exp: & (self->tail)->next) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1038:9-1038:29)
  read with [mhp:{created={[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41]}}, thread:[main]] (conf. 100)  (exp: & (self->head)->next) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1053:5-1053:34)
  read with [mhp:{created={[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41]}}, thread:[main]] (conf. 100)  (exp: & (self->head)->next) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1062:14-1062:46)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1093:9-1093:33)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1084:9-1084:33)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:993:73-993:74)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1093:9-1093:33)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1084:9-1084:33)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1084:9-1084:33)
[Warning][Deadcode][CWE-570] condition 'i < 7' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1093:9-1093:33)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1084:9-1084:33)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1084:9-1084:33)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1084:9-1084:33)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1084:9-1084:33)
[Warning][Race] Memory location (struct FifoNode_).next (race with conf. 100):
  write with thread:[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41] (conf. 100)  (exp: & (self->tail)->next) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1038:9-1038:29)
  read with [mhp:{created={[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41]}}, thread:[main]] (conf. 100)  (exp: & (self->head)->next) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1053:5-1053:34)
  read with [mhp:{created={[main, pusher@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1092:5-1092:41]}}, thread:[main]] (conf. 100)  (exp: & (self->head)->next) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1062:14-1062:46)
[Warning][Deadcode][CWE-570] condition 'i < 7' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1084:9-1084:33)
[Warning][Deadcode][CWE-571] condition 'i < 7' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/divinefifo-bug_1w1r.i:1093:9-1093:33)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
[Info][Race] Memory locations race summary:
  safe: 5
  vulnerable: 0
  unsafe: 2
  total memory locations: 7
