./goblint --conf conf/svcomp.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/weaver/parallel-parallel-sum-2.wvr.c


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:156:3-156:36)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:173:3-173:69)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:175:3-175:54)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:175:3-175:54)
[Info][Unsound] Unknown address in {&tmp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:175:3-175:54)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:175:3-175:54)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:157:3-157:100)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:157:3-157:100)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:51:5-51:9)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:184:3-184:53)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:185:3-185:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:66:5-66:9)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:85:3-85:33)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:97:5-97:9)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:112:5-112:9)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:131:3-131:34)
[Warning][Deadcode] Function "__VERIFIER_error" will never be called: 1LoC (includes/sv-comp.c:2:1-2:36)
[Warning][Deadcode] Function "__VERIFIER_assume" will never be called: 1LoC (includes/sv-comp.c:9:1-9:89)
[Warning][Deadcode] Function "__VERIFIER_nondet_char" will never be called: 1LoC (includes/sv-comp.c:16:1-16:55)
[Warning][Deadcode] Function "__VERIFIER_nondet_float" will never be called: 1LoC (includes/sv-comp.c:19:1-19:58)
[Warning][Deadcode] Function "__VERIFIER_nondet_double" will never be called: 1LoC (includes/sv-comp.c:20:1-20:61)
[Warning][Deadcode] Function "__VERIFIER_nondet_long" will never be called: 1LoC (includes/sv-comp.c:22:1-22:55)
[Warning][Deadcode] Function "__VERIFIER_nondet_pchar" will never be called: 1LoC (includes/sv-comp.c:23:1-23:58)
[Warning][Deadcode] Function "__VERIFIER_nondet_short" will never be called: 1LoC (includes/sv-comp.c:26:1-26:58)
[Warning][Deadcode] Function "__VERIFIER_nondet_uchar" will never be called: 1LoC (includes/sv-comp.c:29:1-29:74)
[Warning][Deadcode] Function "__VERIFIER_nondet_uint" will never be called: 1LoC (includes/sv-comp.c:30:1-30:71)
[Warning][Deadcode] Function "__VERIFIER_nondet_ulong" will never be called: 1LoC (includes/sv-comp.c:31:1-31:74)
[Warning][Deadcode] Function "__VERIFIER_nondet_unsigned" will never be called: 1LoC (includes/sv-comp.c:32:1-32:67)
[Warning][Deadcode] Function "__VERIFIER_nondet_ushort" will never be called: 1LoC (includes/sv-comp.c:33:1-33:77)
[Warning][Deadcode] Function "__VERIFIER_nondet_pointer" will never be called: 1LoC (includes/sv-comp.c:35:1-35:60)
[Warning][Race] Memory location i1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:42:5-42:7 (race with conf. 110):
  read with [region:{i1},
           mhp:{tid=[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:160:3-160:37]; created={[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:160:3-160:37, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:80:3-80:37], [main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:160:3-160:37, thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:81:3-81:37]}}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:160:3-160:37]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:85:3-85:33)
  write with [region:{i1}, mhp:{tid=[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:160:3-160:37, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:80:3-80:37]}, lock:{[__VERIFIER_atomic]}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:160:3-160:37, thread2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:80:3-80:37]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:51:5-51:9)
  write with [region:{i1}, mhp:{tid=[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:160:3-160:37, thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:81:3-81:37]}, lock:{[__VERIFIER_atomic]}, thread:[main, thread1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:160:3-160:37, thread3@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:81:3-81:37]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:66:5-66:9)
[Warning][Race] Memory location i2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:42:9-42:11 (race with conf. 110):
  read with [region:{i2}, mhp:{tid=[main, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3-161:37]; created={[main, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3-161:37, thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:126:3-126:37], [main, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3-161:37, thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:127:3-127:37]}}, thread:[main, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3-161:37]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:131:3-131:34)
  write with [region:{i2}, mhp:{tid=[main, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3-161:37, thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:126:3-126:37]}, lock:{[__VERIFIER_atomic]}, thread:[main, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3-161:37, thread5@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:126:3-126:37]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:97:5-97:9)
  write with [region:{i2}, mhp:{tid=[main, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3-161:37, thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:127:3-127:37]}, lock:{[__VERIFIER_atomic]}, thread:[main, thread4@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:161:3-161:37, thread6@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:127:3-127:37]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-parallel-sum-2.wvr.c:112:5-112:9)
SV-COMP result: unknown

Summary for all memory locations:
	safe:           13
	vulnerable:      0
	unsafe:          2
	-------------------
	total:          15
:-1: Warning: Incompatible declaration for pthread_create (from .goblint/preprocessed/parallel-parallel-sum-2.wvr.i(3)).
 Previous was at /usr/include/pthread.h:198 (from .goblint/preprocessed/pthread.i (2)) 
	Failed assumption that pthread_attr_t and pthread_attr_t are isomorphic 
	Failed assumption that union pthread_attr_t and union pthread_attr_t are isomorphic (different array sizes)
union pthread_attr_t {
   char __size[56] ;
   long __align ;
};

union pthread_attr_t {
   char __size[36] ;
   long __align ;
};
 
