./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i


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


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/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i
Converting
Type-checking 04-mutex_35-trylock_rc
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_mutex_trylock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_trylock"
old definition in module 04-mutex_35-trylock_rc file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 510
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_trylock> line 17
signed int (pthread_mutex_t *pthread_mutex_trylock$$mutex)
file <builtin-library-time> line 11: warning: conflicting return types "time"
old definition in module 04-mutex_35-trylock_rc file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 159
time_t (time_t *)
new definition in module <built-in-library> file <builtin-library-time> line 11
time_t (time_t *tloc)
file <builtin-library-time> line 11: 
reason for conflict at #this: conflict on POD

time_t
time_t
error: conflicting function declarations 'time'
old definition in module '04-mutex_35-trylock_rc' file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 159
time_t (time_t *)
new definition in module '<built-in-library>' file <builtin-library-time> line 11
time_t (time_t *tloc)
file <builtin-library-pthread_mutex_lock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_lock"
old definition in module 04-mutex_35-trylock_rc file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 512
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_lock> line 17
signed int (pthread_mutex_t *pthread_mutex_lock$$mutex)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module 04-mutex_35-trylock_rc file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 399
signed int (pthread_t *, const pthread_attr_t *, void * (*)(void *), void *)
new definition in module <built-in-library> file <builtin-library-pthread_create> line 20
signed int (pthread_t *thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
file <builtin-library-pthread_mutex_unlock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_unlock"
old definition in module 04-mutex_35-trylock_rc file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 517
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_unlock> line 17
signed int (pthread_mutex_t *pthread_mutex_unlock$$mutex)
file <builtin-library-fprintf> line 12: 
reason for conflict at #this: number of members is different (30/29)

struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  unsigned int $pad21;
  __off64_t _offset;
  void * __pad1;
  void * __pad2;
  void * __pad3;
  void * __pad4;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
warning: pointer parameter types differ between declaration and definition "fprintf"
old definition in module 04-mutex_35-trylock_rc file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 816
signed int (FILE *, const char *, ...)
new definition in module <built-in-library> file <builtin-library-fprintf> line 12
signed int (FILE *stream, const char * restrict format, ...)
file /usr/include/stdio.h line 145: warning: conflicting pointer types for variable "stderr"
old definition in module 04-mutex_35-trylock_rc file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 788
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  unsigned int $pad21;
  __off64_t _offset;
  void * __pad1;
  void * __pad2;
  void * __pad3;
  void * __pad4;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
} *
new definition in module <built-in-library> file /usr/include/stdio.h line 145
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
} *
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, 24 offset bits (default)
Starting Bounded Model Checking
argc''s upper bound is 1073741824
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
**** WARNING: no body for function time
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(time_t,
                                            TNamed(__time_t, TInt(long, ), ), ), ), CastE(TPtr(TVoid(), ), Const(Int64(0,int,None)))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1839:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1839:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1804:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1809:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1811:12)
[Warning][Unknown] Unknown address in {&tmp___0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1811:12)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1811:12)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1811:12)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1811:12)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(time_t, TNamed(__time_t, TInt(long, ), ), ), ), CastE(TPtr(TVoid(), ), Const(Int64(0,int,None)))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1803:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1803:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1842:10)
[Warning][Unknown] Unknown address in {&tmp___0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1842:10)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1842:10)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1842:10)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1842:10)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(status,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1821:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1824:14)
[Warning][Unknown] Unknown address in {&tmp} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1824:14)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1824:14)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1824:14)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1824:14)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(status, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1826:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1828:14)
[Warning][Unknown] Unknown address in {&tmp___0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1828:14)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1828:14)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1828:14)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1828:14)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(time_t, TNamed(__time_t, TInt(long, ), ), ), ), CastE(TPtr(TVoid(), ), Const(Int64(0,int,None)))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1819:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1819:3)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:62:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:67:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:72:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:77:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:82:1)
[Warning][Race] Memory location counter@04-mutex_35-trylock_rc.i:1798:6 (race with conf. 110):
  read with {lock:mutex, thread:([counter_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1841:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1808:7)
  read with {lock:mutex, thread:([monitor_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1844:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1825:7)
  read with {thread:([monitor_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1844:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1830:7)
  write with {lock:mutex, thread:([counter_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1841:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1808:7)
  write with {thread:([monitor_thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1844:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i:1830:7)

Summary for all memory locations:
	safe:            1
	vulnerable:      0
	unsafe:          1
	-------------------
	total:           2
pointer handling for concurrency is unsound
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0
Unwinding loop counter_thread.1 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 1807 function counter_thread thread 1
Not unwinding loop counter_thread.1 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 1807 function counter_thread thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Unwinding loop monitor_thread.2 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 1819 function monitor_thread thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Not unwinding loop monitor_thread.2 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i line 1819 function monitor_thread thread 2
Handling datarace, passing the problem to goblint first
getcwd: /mnt/goblint-svcomp/benchexec/tools-pldi/deagle
/mnt/goblint-svcomp/benchexec/tools-pldi/deagle/goblint/goblint /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/04-mutex_35-trylock_rc.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 1808 1809 1821 1822 1825 1826 1830 1831 1839 1840 1842 1843 
The number of races before goblint filter: 60
The number of races after goblint filter: 24
Race categories: 2
	1808(1) - 1825(1) counter:
		counter#3 counter#6
		counter#3 counter#7
		counter#3 counter#8
		counter#3 counter#11
		counter#3 counter#12
		counter#3 counter#13
		counter#5 counter#6
		counter#5 counter#7
		counter#5 counter#8
		counter#5 counter#11
		counter#5 counter#12
		counter#5 counter#13
	1808(1) - 1830(1) counter:
		counter#2 counter#10
		counter#2 counter#15
		counter#3 counter#9
		counter#3 counter#10
		counter#3 counter#14
		counter#3 counter#15
		counter#4 counter#10
		counter#4 counter#15
		counter#5 counter#9
		counter#5 counter#10
		counter#5 counter#14
		counter#5 counter#15
Runtime Symex: 0.473669s
Unsupported library function!
