./deagle --no-assertions --datarace --64 /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c


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


Deagle version 2.1 64-bit x86_64 linux
which contains:
CBMC version 5.67.0 (SVCOMP2023_221122-2-g2121ef1a2) 64-bit x86_64 linux
Parsing /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_rwlock_unlock> line 7: warning: pointer parameter types differ between declaration and definition "pthread_rwlock_unlock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 139
signed int (pthread_rwlock_t *)
new definition in module <built-in-library> file <builtin-library-pthread_rwlock_unlock> line 7
signed int (pthread_rwlock_t *pthread_rwlock_unlock$$lock)
file <builtin-library-pthread_rwlock_wrlock> line 7: warning: pointer parameter types differ between declaration and definition "pthread_rwlock_wrlock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 138
signed int (pthread_rwlock_t *)
new definition in module <built-in-library> file <builtin-library-pthread_rwlock_wrlock> line 7
signed int (pthread_rwlock_t *pthread_rwlock_wrlock$$lock)
file <builtin-library-pthread_rwlock_rdlock> line 7: warning: pointer parameter types differ between declaration and definition "pthread_rwlock_rdlock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 137
signed int (pthread_rwlock_t *)
new definition in module <built-in-library> file <builtin-library-pthread_rwlock_rdlock> line 7
signed int (pthread_rwlock_t *pthread_rwlock_rdlock$$lock)
file <builtin-library-pthread_rwlock_destroy> line 7: warning: pointer parameter types differ between declaration and definition "pthread_rwlock_destroy"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 136
signed int (pthread_rwlock_t *)
new definition in module <built-in-library> file <builtin-library-pthread_rwlock_destroy> line 7
signed int (pthread_rwlock_t *pthread_rwlock_destroy$$lock)
file <builtin-library-pthread_rwlock_init> line 16: warning: pointer parameter types differ between declaration and definition "pthread_rwlock_init"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 134
signed int (pthread_rwlock_t *, const pthread_rwlockattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_rwlock_init> line 16
signed int (pthread_rwlock_t *pthread_rwlock_init$$lock, const pthread_rwlockattr_t *attr)
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 2 possible targets
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
pointer handling for concurrency is unsound
Unwinding loop thread_routine_r.2 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 159 function thread_routine_r thread 1
Not unwinding loop thread_routine_r.2 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 159 function thread_routine_r thread 1
Unwinding loop thread_routine_r.2 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 159 function thread_routine_r thread 2
Not unwinding loop thread_routine_r.2 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 159 function thread_routine_r thread 2
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 3
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 3
Unwinding loop thread_routine_w.3 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 3
Not unwinding loop thread_routine_w.3 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 3
Unwinding loop thread_routine_w.4 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 698 function thread_routine_w thread 3
Unwinding loop thread_routine_w.3 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 3
Not unwinding loop thread_routine_w.3 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 3
Not unwinding loop thread_routine_w.4 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 698 function thread_routine_w thread 3
Unwinding loop thread_routine_w.5 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 358 function thread_routine_w thread 3
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 3
Not unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 3
Unwinding loop thread_routine_w.1 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 487 function thread_routine_w thread 3
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 3
Not unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 3
Not unwinding loop thread_routine_w.1 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 487 function thread_routine_w thread 3
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 3
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 3
Unwinding loop thread_routine_w.3 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 3
Not unwinding loop thread_routine_w.3 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 3
Unwinding loop thread_routine_w.4 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 698 function thread_routine_w thread 3
Unwinding loop thread_routine_w.3 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 3
Not unwinding loop thread_routine_w.3 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 3
Not unwinding loop thread_routine_w.4 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 698 function thread_routine_w thread 3
Not unwinding loop thread_routine_w.5 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 358 function thread_routine_w thread 3
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 4
Not unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 4
Unwinding loop thread_routine_w.1 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 487 function thread_routine_w thread 4
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 4
Not unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 4
Not unwinding loop thread_routine_w.1 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 487 function thread_routine_w thread 4
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 4
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 4
Unwinding loop thread_routine_w.3 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 4
Not unwinding loop thread_routine_w.3 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 4
Unwinding loop thread_routine_w.4 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 698 function thread_routine_w thread 4
Unwinding loop thread_routine_w.3 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 4
Not unwinding loop thread_routine_w.3 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 4
Not unwinding loop thread_routine_w.4 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 698 function thread_routine_w thread 4
Unwinding loop thread_routine_w.5 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 358 function thread_routine_w thread 4
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 4
Not unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 4
Unwinding loop thread_routine_w.1 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 487 function thread_routine_w thread 4
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 4
Not unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 4
Not unwinding loop thread_routine_w.1 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 487 function thread_routine_w thread 4
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 4
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 4
Unwinding loop thread_routine_w.3 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 4
Not unwinding loop thread_routine_w.3 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 4
Unwinding loop thread_routine_w.4 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 698 function thread_routine_w thread 4
Unwinding loop thread_routine_w.3 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 4
Not unwinding loop thread_routine_w.3 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 700 function thread_routine_w thread 4
Not unwinding loop thread_routine_w.4 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 698 function thread_routine_w thread 4
Not unwinding loop thread_routine_w.5 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c line 358 function thread_routine_w thread 4
Handling datarace, passing the problem to goblint first
getcwd: /mnt/goblint-svcomp/benchexec/t[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:772:3)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:774:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:774:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:160:5)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:162:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:162:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:160:5)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:162:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:162:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:359:5)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:361:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:361:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:359:5)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:361:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:361:7)
[Debug][Analyzer] Base EvalInt thread_r1 query answering bot instead of {([thread_routine_r@/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:779:3, main], {})} (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:801:3)
[Warning][Unknown] Unknown address in {&thread_result} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:801:3)
[Debug][Analyzer] Base EvalInt thread_r2 query answering bot instead of {([thread_routine_r@/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:785:3, main], {})} (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:803:3)
[Debug][Analyzer] Base EvalInt thread_w1 query answering bot instead of {([thread_routine_w@/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:791:3, main], {})} (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:805:3)
[Debug][Analyzer] Base EvalInt thread_w2 query answering bot instead of {([thread_routine_w@/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:797:3, main], {})} (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:807:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___1,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:815:3)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:817:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c:817:5)

Summary for all memory locations:
	safe:           15
	vulnerable:      0
	unsafe:          0
	-------------------
	total:          15
ools-pldi/deagle-pure
/mnt/goblint-svcomp/benchexec/tools-pldi/deagle-pure/goblint/goblint /mnt/goblint-svcomp/goblint-bench/bench/concrat/uthash/main.c | tee goblint/goblint_output: 0
