./deagle /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c --64


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


./deagle_exe --svcomp --graphml-witness error-witness.graphml --no-assertions --datarace /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c
Deagle version 2.2 64-bit x86_64 linux
which contains:
CBMC version 5.67.0 (svcomp24-11-gfd1b965b5-dirty) 64-bit x86_64 linux
Parsing /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_cond_init> line 7: 
reason for conflict at #this.__data: names of member 0 differ (__annonCompField1/__wseq)

struct __pthread_cond_s {
  union __anonunion____missing_field_name_648058633 __annonCompField1;
  union __anonunion____missing_field_name_366146943 __annonCompField2;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
struct __pthread_cond_s {
  __atomic_wide_counter __wseq;
  __atomic_wide_counter __g1_start;
  unsigned int [2] __g_refs;
  unsigned int [2] __g_size;
  unsigned int __g1_orig_size;
  unsigned int __wrefs;
  unsigned int [2] __g_signals;
}
warning: pointer parameter types differ between declaration and definition "pthread_cond_init"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c line 289
signed int (pthread_cond_t *, const pthread_condattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_cond_init> line 7
signed int (pthread_cond_t *cond, const pthread_condattr_t *attr)
file <builtin-library-pthread_mutex_unlock> line 17: warning: pointer parameter types differ between declaration and definition "pthread_mutex_unlock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c line 288
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 *mutex)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c line 282
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-ctime> line 7: 
reason for conflict at #this: conflict on POD

const time_t
const time_t
warning: pointer parameter types differ between declaration and definition "ctime"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c line 266
char * (const time_t *)
new definition in module <built-in-library> file <builtin-library-ctime> line 7
char * (const time_t *clock)
file <builtin-library-time> line 11: warning: conflicting return types "time"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c line 265
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 'main' file /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c line 265
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: warning: pointer parameter types differ between declaration and definition "pthread_mutex_lock"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c line 287
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 *mutex)
file <builtin-library-fflush> line 9: 
reason for conflict at #this._chain->_old_offset: conflict on POD

__off_t
__off_t

reason for conflict at #this._chain->_old_offset: type of member _chain differs (recursive)

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;
}
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 "fflush"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c line 261
signed int (FILE *)
new definition in module <built-in-library> file <builtin-library-fflush> line 9
signed int (FILE *stream)
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 1 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 sigemptyset
**** WARNING: no body for function sigaction
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
pointer handling for concurrency is unsound
**** WARNING: no body for function sigaddset
**** WARNING: no body for function sigprocmask
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function timer_create
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function timer_settime
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function clock_gettime
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function time
**** WARNING: no body for function ftime
**** WARNING: no body for function usleep
**** WARNING: no body for function gettimeofday
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function timer_getoverrun
**** WARNING: no body for function timer_gettime
**** WARNING: no body for function lstat
**** WARNING: no body for function pthread_cond_timedwait
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 1
**** WARNING: no body for function pthread_condattr_init
**** WARNING: no body for function pthread_condattr_setclock
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 1
**** WARNING: no body for function pthread_cond_destroy
Start removing dummy accesses: 959 steps before removal
main::1::thread!0@1#3 is dummy and removed
main::1::sa!0@1#2..__sigaction_handler is dummy and removed
printf::format!0@2#2 is dummy and removed
main::1::sev!0@1#2..sigev_value is dummy and removed
main::1::timerid1!0@1#3 is dummy and removed
main::1::sev!0@1#4..sigev_value is dummy and removed
main::1::timerid2!0@1#2 is dummy and removed
printf::format!0@3#2 is dummy and removed
printf::format!0@4#2 is dummy and removed
printf::format!0@5#2 is dummy and removed
printf::format!0@6#2 is dummy and removed
stdout#2 is dummy and removed
printf::format!0@7#2 is dummy and removed
printf::format!0@8#2 is dummy and removed
main::1::timerid1!0@1#4 is dummy and removed
printf::format!0@9#2 is dummy and removed
main::1::timerid1!0@1#5 is dummy and removed
main::1::timerid2!0@1#3 is dummy and removed
printf::format!0@10#2 is dummy and removed
main::1::timerid2!0@1#4 is dummy and removed
argc'#1 is dummy and removed
argv'#2 is dummy and removed
argc'#2 is dummy and removed
argc'#3 is dummy and removed
argc'#4 is dummy and removed
argv'#3 is dummy and removed
argc'#5 is dummy and removed
argv'#4 is dummy and removed
argc'#6 is dummy and removed
argc'#7 is dummy and removed
argc'#8 is dummy and removed
printf::format!0@11#2 is dummy and removed
pthread_test::1::timeToWait!1@1#2..tv_sec is dummy and removed
pthread_test::1::timeToWait!1@1#2..tv_nsec is dummy and removed
pthread_test::1::now!1@1#2..tv_sec is dummy and removed
pthread_test::1::now!1@1#2..tv_nsec is dummy and removed
pthread_test::1::fakeCond!1@1#6 is dummy and removed
pthread_test::1::fakeCond!1@1#10 is dummy and removed
pthread_test::1::fakeCond!1@1#14 is dummy and removed
pthread_test::1::fakeCond!1@1#18 is dummy and removed
pthread_test::1::fakeCond!1@1#22 is dummy and removed
pthread_test::1::fakeCond!1@1#25 is dummy and removed
pthread_test::1::fakeCond!1@1#28 is dummy and removed
pthread_test::1::fakeCond!1@1#32 is dummy and removed
printf::format!1@1#2 is dummy and removed
printf::format!1@2#2 is dummy and removed
stdout#4 is dummy and removed
printf::format!1@3#2 is dummy and removed
printf::format!1@4#2 is dummy and removed
printf::format!1@5#2 is dummy and removed
printf::format!1@6#2 is dummy and removed
stdout#6 is dummy and removed
printf::format!1@7#2 is dummy and removed
906 steps after removal
Handling datarace with no aid
The number of races before filter: 2
The number of races after filter: 2
The number of race categories before filter: 2
The number of race categories after filter: 2
	260(1) - 355(1) stdout
	260(1) - 374(1) stdout
Races between line 260 - line 355:
	stdout#1 stdout#5
Races between line 260 - line 374:
	stdout#1 stdout#7
Runtime Symex: 1.03629s
Adding SC constraints
Shared __CPROVER_threads_exited: 2R/2W
Shared __CPROVER_next_thread_id: 1R/2W
Shared stdout: 3R/1W
Shared argv': 1R/1W
Shared main::1::its!0@1..it_value..tv_sec: 1R/3W
Shared main::1::thread!0@1: 1R/2W
Shared pthread_test::1::fakeMutex!1@1: 26R/17W
Shared pthread_test::1::fakeCond!1@1: 16R/12W
Shared pthread_test::1::monotonic_cond!1@1: 1R/3W
Shared pthread_test::1::now!1@1..tv_sec: 2R/1W
Shared pthread_test::1::now!1@1..tv_nsec: 2R/1W
size of program expression: 1341 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.00542473s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0767522s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.000352687s
Solving with Deagle's Closure Solver
135822 variables, 517119 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 0.000369337s
Runtime decision procedure: 0.0997004s

** Results:
[nodatarace.assertion.0] No data races on variable stdout between line 260 and line 355: SUCCESS
[nodatarace.assertion.1] No data races on variable stdout between line 260 and line 374: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL
