./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/pthread/fib_unsafe-11.i


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


--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/pthread/fib_unsafe-11.i:690:5-690:14)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:688:7-688:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:698:5-698:14)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:696:7-696:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:707:5-707:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:706:7-706:26)
[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_bool" will never be called: 1LoC (includes/sv-comp.c:15:1-15:57)
[Warning][Deadcode] Function "__VERIFIER_nondet_char" will never be called: 1LoC (includes/sv-comp.c:16:1-16:55)
[Warning][Deadcode] Function "__VERIFIER_nondet_int" will never be called: 1LoC (includes/sv-comp.c:18:1-18:52)
[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 j@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:683:8-683:9 (race with conf. 110):
  read with [region:{j},
           mhp:{tid=[main]; created={[main, t1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:721:3-721:53], [main, t2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:722:3-722:53]}}, thread:[main]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:725:6-725:32)
  write with [region:{j}, mhp:{tid=[main, t2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:722:3-722:53]}, lock:{[__VERIFIER_atomic]}, thread:[main, t2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:722:3-722:53]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:698:5-698:14)
[Warning][Race] Memory location i@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:683:5-683:6 (race with conf. 110):
  read with [region:{i}, mhp:{tid=[main]; created={[main, t1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:721:3-721:53], [main, t2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:722:3-722:53]}}, thread:[main]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:725:6-725:32)
  write with [region:{i}, mhp:{tid=[main, t1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:721:3-721:53]}, lock:{[__VERIFIER_atomic]}, thread:[main, t1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:721:3-721:53]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-11.i:690:5-690:14)
SV-COMP result: unknown

Summary for all memory locations:
	safe:            6
	vulnerable:      0
	unsafe:          2
	-------------------
	total:           8
