./deagle --no-assertions --datarace --64 /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/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/EasyLogger/main.c
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
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/EasyLogger/main.c line 1834
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_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/EasyLogger/main.c line 1833
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-pthread_mutex_init> line 27: warning: pointer parameter types differ between declaration and definition "pthread_mutex_init"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1830
signed int (pthread_mutex_t *, const pthread_mutexattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_init> line 27
signed int (pthread_mutex_t *mutex, const pthread_mutexattr_t *mutexattr)
file <builtin-library-sem_post> line 4: warning: pointer parameter types differ between declaration and definition "sem_post"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1268
signed int (sem_t *)
new definition in module <built-in-library> file <builtin-library-sem_post> line 4
signed int (sem_t *sem)
file <builtin-library-sem_wait> line 4: warning: pointer parameter types differ between declaration and definition "sem_wait"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1267
signed int (sem_t *)
new definition in module <built-in-library> file <builtin-library-sem_wait> line 4
signed int (sem_t *sem)
file <builtin-library-sem_init> line 4: warning: pointer parameter types differ between declaration and definition "sem_init"
old definition in module main file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1263
signed int (sem_t *, signed int, unsigned int)
new definition in module <built-in-library> file <builtin-library-sem_init> line 4
signed int (sem_t *sem, signed int pshared, unsigned int value)
Removal of function pointers and virtual functions
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 348 function elog_set_output_enabled: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 396 function elog_set_fmt: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 417 function elog_set_filter: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 440 function elog_set_filter_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 526 function elog_set_filter_tag_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 539 function elog_set_filter_tag_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 599 function elog_get_filter_tag_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 743 function elog_output: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 973 function elog_find_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 985 function elog_find_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 998 function elog_find_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1011 function elog_find_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1024 function elog_find_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1037 function elog_find_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1050 function elog_find_lvl: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1089 function elog_find_tag: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1101 function elog_find_tag: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1113 function elog_find_tag: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1125 function elog_find_tag: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1945 function elog_strcpy: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1957 function elog_strcpy: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 912 function get_fmt_enabled: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1599 function elog_file_write: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1611 function elog_file_write: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1646 function elog_file_deinit: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1999 function elog_cpyln: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 2011 function elog_cpyln: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 2056 function elog_memcpy: replacing function pointer by 0 possible targets
file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 2068 function elog_memcpy: replacing function pointer by 0 possible targets
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, 56 offset bits (default)
Starting Bounded Model Checking
set limit type 2
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
**** WARNING: no body for function setbuf
**** WARNING: no body for function semget
**** WARNING: no body for function semctl
**** WARNING: no body for function usleep
Unwinding loop lock_open.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1791 function lock_open thread 0
Not unwinding loop lock_open.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1791 function lock_open thread 0
**** WARNING: no body for function semop
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 0
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 0
**** WARNING: no body for function pthread_attr_init
**** WARNING: no body for function pthread_attr_setstacksize
**** WARNING: no body for function pthread_attr_setschedpolicy
**** WARNING: no body for function sched_get_priority_max
**** WARNING: no body for function pthread_attr_setschedparam
**** WARNING: no body for function pthread_attr_destroy
Unwinding loop elog_set_filter_tag_lvl_default.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 502 function elog_set_filter_tag_lvl_default thread 0
Not unwinding loop elog_set_filter_tag_lvl_default.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 502 function elog_set_filter_tag_lvl_default thread 0
pointer handling for concurrency is unsound
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 1
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 1
aborting path on assume(false) at file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1599 function elog_file_write thread 1
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 1
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 1
**** WARNING: no body for function snprintf
**** WARNING: no body for function remove
**** WARNING: no body for function rename
[Warning][Unknown] Unknown address in (FILE * __restrict  )stdout has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:2096:3)
[Warning][Unknown] Function definition missing for setbuf (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:2096:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:2096:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stdout, NoOffset))), CastE(TPtr(TInt(char, ),  __restrict  ), CastE(TPtr(TVoid(), ), Const(Int64(0,int,None)))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:2096:3)
[Warning][Unknown] Function definition missing for semget (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1746:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1746:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), Const(Int64(428934674,int,None)), Const(Int64(1,int,None)), Const(Int64(1974,int,None)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1746:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1746:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(id, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1746:3)
[Warning][Unknown] Function definition missing for semctl (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1755:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1755:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), Lval(Var(id, NoOffset)), Const(Int64(0,int,None)), Const(Int64(16,int,None)), Lval(Var(arg, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1755:5)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1755:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(rc, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1755:5)
[Warning][Unknown] Spawning functions from unknown function: sembuf (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1762:5)
[Warning][Unknown] Not creating a thread from sembuf because its type is struct sembuf  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1762:5)
[Warning][Unknown] Function definition missing for semop (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1762:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1762:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), Lval(Var(id, NoOffset)), AddrOf(Var(sembuf, NoOffset)), CastE(TNamed(size_t, TInt(unsigned long, ), ), Const(Int64(1,int,None))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1762:5)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1762:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(rc, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1762:5)
[Warning][Unknown] Function definition missing for semget (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1784:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1784:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), Const(Int64(428934674,int,None)), Const(Int64(1,int,None)), Const(Int64(438,int,None)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1784:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1784:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(id, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1784:3)
[Warning][Unknown] Spawning functions from unknown function: ds (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1792:5)
[Warning][Unknown] Not creating a thread from ds because its type is struct semid_ds  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1792:5)
[Warning][Unknown] Function definition missing for semctl (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1792:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1792:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), Lval(Var(id, NoOffset)), Const(Int64(0,int,None)), Const(Int64(2,int,None)), Lval(Var(arg, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1792:5)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1792:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(rc, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1792:5)
[Warning][Unknown] Spawning functions from unknown function: down (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Not creating a thread from down because its type is struct sembuf  const   (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Function definition missing for semop (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), Lval(Var(semid, NoOffset)), CastE(TPtr(TCompLoop(struct sembuf, _, ), ), AddrOf(Var(down, NoOffset))), CastE(TNamed(size_t, TInt(unsigned long, ), ), Const(Int64(1,int,None))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1673:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1675:9)
[Warning][Unknown] Spawning functions from unknown function: up (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Not creating a thread from up because its type is struct sembuf  const   (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Function definition missing for semop (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), Lval(Var(semid, NoOffset)), CastE(TPtr(TCompLoop(struct sembuf, _, ), ), AddrOf(Var(up, NoOffset))), CastE(TNamed(size_t, TInt(unsigned long, ), ), Const(Int64(1,int,None))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Unknown value in {&thread_attr} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1454:3)
[Warning][Unknown] Spawning functions from unknown function: thread_attr (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1454:3)
[Warning][Unknown] Not creating a thread from thread_attr because its type is pthread_attr_t  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1454:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(thread_attr,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1454:3)
[Warning][Unknown] Unknown value in {&thread_attr} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1455:3)
[Warning][Unknown] Spawning functions from unknown function: thread_attr (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1455:3)
[Warning][Unknown] Not creating a thread from thread_attr because its type is pthread_attr_t  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1455:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(thread_attr, NoOffset)), CastE(TNamed(size_t, TInt(unsigned long, ), ), Const(Int64(1024,int,None))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1455:3)
[Warning][Unknown] Unknown value in {&thread_attr} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1456:3)
[Warning][Unknown] Spawning functions from unknown function: thread_attr (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1456:3)
[Warning][Unknown] Not creating a thread from thread_attr because its type is pthread_attr_t  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1456:3)
[Warning][Unknown] Function definition missing for pthread_attr_setschedpolicy (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1456:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1456:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), AddrOf(Var(thread_attr, NoOffset)), Const(Int64(2,int,None)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1456:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1456:3)
[Warning][Unknown] Function definition missing for sched_get_priority_max (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1457:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1457:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), Const(Int64(2,int,None)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1457:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1457:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1457:3)
[Warning][Unknown] Unknown value in {&thread_attr} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1459:3)
[Warning][Unknown] Spawning functions from unknown function: thread_attr, thread_sched_param (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1459:3)
[Warning][Unknown] Not creating a thread from thread_attr because its type is pthread_attr_t  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1459:3)
[Warning][Unknown] Not creating a thread from thread_sched_param because its type is struct sched_param  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1459:3)
[Warning][Unknown] Function definition missing for pthread_attr_setschedparam (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1459:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1459:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), CastE(TPtr(TNamed(pthread_attr_t, TCompLoop(union pthread_attr_t, _, ), ),  __restrict  ), AddrOf(Var(thread_attr, NoOffset))), CastE(TPtr(TCompLoop(struct sched_param, _, ),  __restrict  ), AddrOf(Var(thread_sched_param, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1459:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1459:3)
[Debug][Analyzer] Base EvalInt ! log query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1602:3)
[Warning][Unknown] Spawning functions from unknown function: down (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Not creating a thread from down because its type is struct sembuf  const   (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Function definition missing for semop (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), Lval(Var(semid, NoOffset)), CastE(TPtr(TCompLoop(struct sembuf, _, ), ), AddrOf(Var(down, NoOffset))), CastE(TNamed(size_t, TInt(unsigned long, ), ), Const(Int64(1,int,None))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Unknown address in fp has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Function definition missing for fseek (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), Lval(Var(fp, NoOffset)), Const(Int64(0,long,None)), Const(Int64(2,int,None)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Unknown address in fp has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Function definition missing for ftell (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), Lval(Var(fp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1541:3)
[Warning][Unknown] Spawning functions from unknown function: oldpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1544:3)
[Warning][Unknown] Not creating a thread from oldpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1544:3)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), StartOf(Var(oldpath, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1544:3)
[Warning][Unknown] Spawning functions from unknown function: newpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1546:3)
[Warning][Unknown] Not creating a thread from newpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1546:3)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), StartOf(Var(newpath, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1546:3)
[Warning][Unknown] Spawning functions from unknown function: oldpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1556:5)
[Warning][Unknown] Not creating a thread from oldpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1556:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), PlusPI(StartOf(Var(oldpath, NoOffset)), Lval(Var(base, NoOffset)))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1556:5)
[Warning][Unknown] Spawning functions from unknown function: newpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1558:5)
[Warning][Unknown] Not creating a thread from newpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1558:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), PlusPI(StartOf(Var(newpath, NoOffset)), Lval(Var(base, NoOffset)))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1558:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp_fp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1560:5)
[Warning][Unknown] Unknown address in {&tmp_fp} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1560:5)
[Warning][Unknown] Spawning functions from unknown function: newpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] Not creating a thread from newpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] Function definition missing for remove (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), CastE(TPtr(TInt(char,  const  ), ), StartOf(Var(newpath, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp_fp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1565:5)
[Warning][Unknown] Unknown address in {&tmp_fp} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1565:5)
[Warning][Unknown] Spawning functions from unknown function: oldpath, newpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Not creating a thread from oldpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Not creating a thread from newpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Function definition missing for rename (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), CastE(TPtr(TInt(char,  const  ), ), StartOf(Var(oldpath, NoOffset))), CastE(TPtr(TInt(char,  const  ), ), StartOf(Var(newpath, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(err,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1577:3)
[Warning][Unknown] Unknown address in {&fp} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1577:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1625:3)
[Warning][Unknown] Unknown address in fp has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
[Warning][Unknown] Invalidating expressions: Lval(Var(fp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
[Warning][Unknown] Spawning functions from unknown function: up (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Not creating a thread from up because its type is struct sembuf  const   (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Function definition missing for semop (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), Lval(Var(semid, NoOffset)), CastE(TPtr(TCompLoop(struct sembuf, _, ), ), AddrOf(Var(up, NoOffset))), CastE(TNamed(size_t, TInt(unsigned long, ), ), Const(Int64(1,int,None))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Spawning functions from unknown function: poll_get_buf (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1368:5)
[Warning][Unknown] Not creating a thread from poll_get_buf because its type is char [25596] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1368:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),
                                      __restrict  ), Lval(Var(log, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1368:5)
[Warning][Unknown] Spawning functions from unknown function: poll_get_buf (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1370:5)
[Warning][Unknown] Not creating a thread from poll_get_buf because its type is char [25596] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1370:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), MinusPI(PlusPI(Lval(Var(log, NoOffset)), Const(Int64(25600,int,None))), Lval(Var(read_index, NoOffset)))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1370:5)
[Warning][Unknown] Spawning functions from unknown function: poll_get_buf (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1364:5)
[Warning][Unknown] Not creating a thread from poll_get_buf because its type is char [25596] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1364:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), Lval(Var(log, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1364:5)
[Warning][Unknown] Unknown value in {&thread_attr} could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3)
[Warning][Unknown] Spawning functions from unknown function: thread_attr (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3)
[Warning][Unknown] Not creating a thread from thread_attr because its type is pthread_attr_t  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3)
[Warning][Unknown] Function definition missing for pthread_attr_destroy (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), AddrOf(Var(thread_attr, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3)
[Warning][Unknown] Spawning functions from unknown function: elog (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:503:5)
[Warning][Unknown] Not creating a thread from elog because its type is EasyLogger  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:503:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(), ), StartOf(Var(elog, Field(filter:TNamed(ElogFilter, TCompLoop(struct __anonstruct_ElogFilter_816931338, _, ), ), Field(tag_lvl:TArray(TNamed(ElogTagLvlFilter, TCompLoop(struct __anonstruct_ElogTagLvlFilter_993067413, _, ), ), Some(Const(Int64(5,int,None))), ), Index(Lval(Var(i, NoOffset)), Field(tag:TArray(TInt(char, ), Some(Const(Int64(17,int,None))), ), NoOffset))))))), Const(CChr('\000')), CastE(TNamed(size_t, TInt(unsigned long, ), ), Const(Int64(17,int,None))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:503:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:717:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:720:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___3, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Warning][Unknown] Unknown address in {&tmp___3} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Debug][Analyzer] Base EvalInt ! tmp___3 query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:757:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:762:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Warning][Unknown] Spawning functions from unknown function: tag_sapce (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Not creating a thread from tag_sapce because its type is char [9] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),
                                ), StartOf(Var(tag_sapce, NoOffset))), Const(CChr(' ')), MinusA(Const(Int64(8,unsigned long,None)), Lval(Var(tag_len, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Warning][Unknown] Spawning functions from unknown function: cur_t (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1893:3)
[Warning][Unknown] Not creating a thread from cur_t because its type is time_t  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1893:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(cur_t,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1893:3)
[Warning][Unknown] Unknown address in {&cur_tm} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1894:3)
[Warning][Unknown] Spawning functions from unknown function: cur_t, cur_tm (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1894:3)
[Warning][Unknown] Not creating a thread from cur_t because its type is time_t  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1894:3)
[Warning][Unknown] Not creating a thread from cur_tm because its type is struct tm  (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1894:3)
[Warning][Unknown] Function definition missing for localtime_r (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1894:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1894:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), CastE(TPtr(TNamed(time_t, TNamed(__time_t, TInt(long, ), ),  const  ),  __restrict  ), AddrOf(Var(cur_t, NoOffset))), CastE(TPtr(TCompLoop(struct tm, _, ),  __restrict  ), AddrOf(Var(cur_tm, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1894:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1894:3)
[Warning][Unknown] Spawning functions from unknown function: cur_system_time (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1895:3)
[Warning][Unknown] Not creating a thread from cur_system_time because its type is char [24] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1895:3)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(cur_system_time, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1895:3)
[Warning][Unknown] Unknown address in {&cur_tm} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1895:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1906:3)
[Warning][Unknown] Spawning functions from unknown function: cur_process_info (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1907:3)
[Warning][Unknown] Not creating a thread from cur_process_info because its type is char [10] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1907:3)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(cur_process_info, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1907:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1918:3)
[Warning][Unknown] Spawning functions from unknown function: cur_thread_info (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1919:3)
[Warning][Unknown] Not creating a thread from cur_thread_info because its type is char [10] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1919:3)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(cur_thread_info, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1919:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Warning][Unknown] Spawning functions from unknown function: line_num (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Not creating a thread from line_num because its type is char [6] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(line_num, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Warning][Unknown] Unknown value in args could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: Lval(Var(args,
                                   NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fmt_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:864:3)
[Warning][Unknown] Invariant failed: expression "<=(PlusA(Lval(Var(log_len, NoOffset)), CastE(TNamed(size_t, TInt(unsigned long, ), ), Lval(Var(fmt_result, NoOffset)))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:865:3)
[Warning][Unknown] Invariant failed: expression ">(PlusA(PlusA(Lval(Var(log_len, NoOffset)), MinusA(sizeofStr("\033[0m"), Const(Int64(1,unsigned long,None)))), Lval(Var(newline_len, NoOffset))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:874:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! log query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1602:3)
[Warning][Unknown] Spawning functions from unknown function: down (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Not creating a thread from down because its type is struct sembuf  const   (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Function definition missing for semop (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), Lval(Var(semid, NoOffset)), CastE(TPtr(TCompLoop(struct sembuf, _, ), ), AddrOf(Var(down, NoOffset))), CastE(TNamed(size_t, TInt(unsigned long, ), ), Const(Int64(1,int,None))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Unknown] Unknown address in fp has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Function definition missing for fseek (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), Lval(Var(fp, NoOffset)), Const(Int64(0,long,None)), Const(Int64(2,int,None)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Unknown address in fp has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Function definition missing for ftell (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), Lval(Var(fp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1541:3)
[Warning][Unknown] Spawning functions from unknown function: oldpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1544:3)
[Warning][Unknown] Not creating a thread from oldpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1544:3)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), StartOf(Var(oldpath, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1544:3)
[Warning][Unknown] Spawning functions from unknown function: newpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1546:3)
[Warning][Unknown] Not creating a thread from newpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1546:3)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), StartOf(Var(newpath, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1546:3)
[Warning][Unknown] Spawning functions from unknown function: oldpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1556:5)
[Warning][Unknown] Not creating a thread from oldpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1556:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), PlusPI(StartOf(Var(oldpath, NoOffset)), Lval(Var(base, NoOffset)))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1556:5)
[Warning][Unknown] Spawning functions from unknown function: newpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1558:5)
[Warning][Unknown] Not creating a thread from newpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1558:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), PlusPI(StartOf(Var(newpath, NoOffset)), Lval(Var(base, NoOffset)))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1558:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp_fp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1560:5)
[Warning][Unknown] Unknown address in {&tmp_fp} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1560:5)
[Warning][Unknown] Spawning functions from unknown function: newpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] Not creating a thread from newpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] Function definition missing for remove (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), CastE(TPtr(TInt(char,  const  ), ), StartOf(Var(newpath, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1563:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp_fp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1565:5)
[Warning][Unknown] Unknown address in {&tmp_fp} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1565:5)
[Warning][Unknown] Spawning functions from unknown function: oldpath, newpath (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Not creating a thread from oldpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Not creating a thread from newpath because its type is char [256] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Function definition missing for rename (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), CastE(TPtr(TInt(char,  const  ), ), StartOf(Var(oldpath, NoOffset))), CastE(TPtr(TInt(char,  const  ), ), StartOf(Var(newpath, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(err,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1568:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1577:3)
[Warning][Unknown] Unknown address in {&fp} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1577:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1625:3)
[Warning][Unknown] Unknown address in fp has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
[Warning][Unknown] Invalidating expressions: Lval(Var(fp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
[Warning][Unknown] Spawning functions from unknown function: up (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Not creating a thread from up because its type is struct sembuf  const   (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Function definition missing for semop (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), Lval(Var(semid, NoOffset)), CastE(TPtr(TCompLoop(struct sembuf, _, ), ), AddrOf(Var(up, NoOffset))), CastE(TNamed(size_t, TInt(unsigned long, ), ), Const(Int64(1,int,None))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:717:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:720:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___3, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Warning][Unknown] Unknown address in {&tmp___3} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Debug][Analyzer] Base EvalInt ! tmp___3 query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:757:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:762:3)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Warning][Unknown] Spawning functions from unknown function: tag_sapce (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Not creating a thread from tag_sapce because its type is char [9] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),
                                ), StartOf(Var(tag_sapce, NoOffset))), Const(CChr(' ')), MinusA(Const(Int64(8,unsigned long,None)), Lval(Var(tag_len, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Warning][Unknown] Spawning functions from unknown function: line_num (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Not creating a thread from line_num because its type is char [6] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(line_num, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Warning][Unknown] Unknown value in args could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: Lval(Var(args,
                                   NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fmt_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:864:3)
[Warning][Unknown] Invariant failed: expression "<=(PlusA(Lval(Var(log_len, NoOffset)), CastE(TNamed(size_t, TInt(unsigned long, ), ), Lval(Var(fmt_result, NoOffset)))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:865:3)
[Warning][Unknown] Invariant failed: expression ">(PlusA(PlusA(Lval(Var(log_len, NoOffset)), MinusA(sizeofStr("\033[0m"), Const(Int64(1,unsigned long,None)))), Lval(Var(newline_len, NoOffset))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:874:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:717:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:720:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___3, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Warning][Unknown] Unknown address in {&tmp___3} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Debug][Analyzer] Base EvalInt ! tmp___3 query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:757:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:762:3)
[Warning][Unknown] Spawning functions from unknown function: tag_sapce (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Not creating a thread from tag_sapce because its type is char [9] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),
                                ), StartOf(Var(tag_sapce, NoOffset))), Const(CChr(' ')), MinusA(Const(Int64(8,unsigned long,None)), Lval(Var(tag_len, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Spawning functions from unknown function: line_num (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Not creating a thread from line_num because its type is char [6] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(line_num, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Unknown value in args could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: Lval(Var(args,
                                   NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fmt_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:864:3)
[Warning][Unknown] Invariant failed: expression "<=(PlusA(Lval(Var(log_len, NoOffset)), CastE(TNamed(size_t, TInt(unsigned long, ), ), Lval(Var(fmt_result, NoOffset)))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:865:3)
[Warning][Unknown] Invariant failed: expression ">(PlusA(PlusA(Lval(Var(log_len, NoOffset)), MinusA(sizeofStr("\033[0m"), Const(Int64(1,unsigned long,None)))), Lval(Var(newline_len, NoOffset))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:874:3)
[Warning][Unknown] Spawning functions from unknown function: log_buf___0 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1332:5)
[Warning][Unknown] Not creating a thread from log_buf___0 because its type is char [25600] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1332:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),
                                      __restrict  ), PlusPI(StartOf(Var(log_buf___0, NoOffset)), Lval(Var(write_index, NoOffset)))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1332:5)
[Warning][Unknown] Spawning functions from unknown function: log_buf___0 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1334:5)
[Warning][Unknown] Not creating a thread from log_buf___0 because its type is char [25600] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1334:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), StartOf(Var(log_buf___0, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1334:5)
[Warning][Unknown] Spawning functions from unknown function: log_buf___0 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1328:5)
[Warning][Unknown] Not creating a thread from log_buf___0 because its type is char [25600] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1328:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), PlusPI(StartOf(Var(log_buf___0, NoOffset)), Lval(Var(write_index, NoOffset)))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1328:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:717:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:720:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___3, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Warning][Unknown] Unknown address in {&tmp___3} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Debug][Analyzer] Base EvalInt ! tmp___3 query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:757:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:762:3)
[Warning][Unknown] Spawning functions from unknown function: tag_sapce (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Not creating a thread from tag_sapce because its type is char [9] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),
                                ), StartOf(Var(tag_sapce, NoOffset))), Const(CChr(' ')), MinusA(Const(Int64(8,unsigned long,None)), Lval(Var(tag_len, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Spawning functions from unknown function: line_num (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Not creating a thread from line_num because its type is char [6] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(line_num, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Unknown value in args could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: Lval(Var(args,
                                   NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fmt_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:864:3)
[Warning][Unknown] Invariant failed: expression "<=(PlusA(Lval(Var(log_len, NoOffset)), CastE(TNamed(size_t, TInt(unsigned long, ), ), Lval(Var(fmt_result, NoOffset)))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:865:3)
[Warning][Unknown] Invariant failed: expression ">(PlusA(PlusA(Lval(Var(log_len, NoOffset)), MinusA(sizeofStr("\033[0m"), Const(Int64(1,unsigned long,None)))), Lval(Var(newline_len, NoOffset))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:874:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1177:5)
[Warning][Unknown] Unknown address in {&tmp___0} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1177:5)
[Debug][Analyzer] Base EvalInt ! tmp___0 query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1178:5)
[Warning][Unknown] Invariant failed: expression "<(CastE(TInt(unsigned int, ), MinusA(CastE(TInt(int,  const  ), Lval(Mem(PlusPI(Lval(Var(buf_p, NoOffset)), PlusA(CastE(TInt(int, ), Lval(Var(i, NoOffset))), CastE(TInt(int, ), Lval(Var(j, NoOffset))))), NoOffset))), Const(Int64(32,int,None)))), Const(Int64(5f,unsigned int,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1218:9)
[Warning][Unknown] Spawning functions from unknown function: dump_string (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1223:9)
[Warning][Unknown] Not creating a thread from dump_string because its type is char [8] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1223:9)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(dump_string, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1223:9)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Spawning functions from unknown function: dump_string (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1202:9)
[Warning][Unknown] Not creating a thread from dump_string because its type is char [8] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1202:9)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(dump_string, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1202:9)
[Warning][Unknown] Spawning functions from unknown function: dump_string (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1199:9)
[Warning][Unknown] Not creating a thread from dump_string because its type is char [8] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1199:9)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(dump_string, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1199:9)
[Warning][Unknown] Invariant failed: expression "==(%(PlusA(CastE(TInt(int,
                                               ), Lval(Var(j, NoOffset))), Const(Int64(1,int,None))), Const(Int64(8,int,None))), Const(Int64(0,int,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1207:7)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Warning][Unknown] Invariant failed: expression "==(%(PlusA(CastE(TInt(int, ), Lval(Var(j, NoOffset))), Const(Int64(1,int,None))), Const(Int64(8,int,None))), Const(Int64(0,int,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1207:7)
[Warning][Unknown] Spawning functions from unknown function: log_buf (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1185:5)
[Warning][Unknown] Not creating a thread from log_buf because its type is char [512] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1185:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(log_buf, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1185:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fmt_result,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1185:5)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___7,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1230:5)
[Warning][Unknown] Invariant failed: expression ">(PlusA(CastE(TNamed(size_t, TInt(unsigned long, ), ), Lval(Var(log_len, NoOffset))), Lval(Var(tmp___7, NoOffset))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1231:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___6, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1232:7)
[Debug][Analyzer] Base EvalInt ! dst query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1936:3)
[Debug][Analyzer] Base EvalInt ! src query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1948:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:3)
[Debug][Analyzer] Base EvalInt ! log query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1602:3)
[Warning][Unknown] Unknown address in fp has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Function definition missing for fseek (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook,
                                     NoOffset)), Lval(Var(fp, NoOffset)), Const(Int64(0,long,None)), Const(Int64(2,int,None)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
[Warning][Unknown] Unknown address in fp has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Function definition missing for ftell (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(elog_assert_hook, NoOffset)), Lval(Var(fp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Unknown address in {&elog_assert_hook} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1625:3)
[Warning][Unknown] Unknown address in fp has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
[Warning][Unknown] Invalidating expressions: Lval(Var(fp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
[Warning][Unknown] Spawning functions from unknown function: log_buf___0 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1332:5)
[Warning][Unknown] Not creating a thread from log_buf___0 because its type is char [25600] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1332:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), PlusPI(StartOf(Var(log_buf___0, NoOffset)), Lval(Var(write_index, NoOffset)))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1332:5)
[Warning][Unknown] Spawning functions from unknown function: log_buf___0 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1334:5)
[Warning][Unknown] Not creating a thread from log_buf___0 because its type is char [25600] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1334:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), StartOf(Var(log_buf___0, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1334:5)
[Warning][Unknown] Spawning functions from unknown function: log_buf___0 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1328:5)
[Warning][Unknown] Not creating a thread from log_buf___0 because its type is char [25600] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1328:5)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),  __restrict  ), PlusPI(StartOf(Var(log_buf___0, NoOffset)), Lval(Var(write_index, NoOffset)))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1328:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:717:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:720:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___3, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Warning][Unknown] Unknown address in {&tmp___3} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Debug][Analyzer] Base EvalInt ! tmp___3 query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:757:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:762:3)
[Warning][Unknown] Spawning functions from unknown function: tag_sapce (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Not creating a thread from tag_sapce because its type is char [9] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),
                                ), StartOf(Var(tag_sapce, NoOffset))), Const(CChr(' ')), MinusA(Const(Int64(8,unsigned long,None)), Lval(Var(tag_len, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Spawning functions from unknown function: line_num (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Not creating a thread from line_num because its type is char [6] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(line_num, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Unknown value in args could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: Lval(Var(args,
                                   NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fmt_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:864:3)
[Warning][Unknown] Invariant failed: expression "<=(PlusA(Lval(Var(log_len, NoOffset)), CastE(TNamed(size_t, TInt(unsigned long, ), ), Lval(Var(fmt_result, NoOffset)))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:865:3)
[Warning][Unknown] Invariant failed: expression ">(PlusA(PlusA(Lval(Var(log_len, NoOffset)), MinusA(sizeofStr("\033[0m"), Const(Int64(1,unsigned long,None)))), Lval(Var(newline_len, NoOffset))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:874:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:717:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:720:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___3, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Warning][Unknown] Unknown address in {&tmp___3} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Debug][Analyzer] Base EvalInt ! tmp___3 query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:757:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:762:3)
[Warning][Unknown] Spawning functions from unknown function: tag_sapce (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Not creating a thread from tag_sapce because its type is char [9] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),
                                ), StartOf(Var(tag_sapce, NoOffset))), Const(CChr(' ')), MinusA(Const(Int64(8,unsigned long,None)), Lval(Var(tag_len, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Spawning functions from unknown function: line_num (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Not creating a thread from line_num because its type is char [6] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(line_num, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Unknown value in args could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: Lval(Var(args,
                                   NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fmt_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:864:3)
[Warning][Unknown] Invariant failed: expression "<=(PlusA(Lval(Var(log_len, NoOffset)), CastE(TNamed(size_t, TInt(unsigned long, ), ), Lval(Var(fmt_result, NoOffset)))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:865:3)
[Warning][Unknown] Invariant failed: expression ">(PlusA(PlusA(Lval(Var(log_len, NoOffset)), MinusA(sizeofStr("\033[0m"), Const(Int64(1,unsigned long,None)))), Lval(Var(newline_len, NoOffset))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:874:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:717:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:720:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___3, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Warning][Unknown] Unknown address in {&tmp___3} has escaped. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:756:7)
[Debug][Analyzer] Base EvalInt ! tmp___3 query answering bot instead of Unknown (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:757:7)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:762:3)
[Warning][Unknown] Spawning functions from unknown function: tag_sapce (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Not creating a thread from tag_sapce because its type is char [9] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TVoid(),
                                ), StartOf(Var(tag_sapce, NoOffset))), Const(CChr(' ')), MinusA(Const(Int64(8,unsigned long,None)), Lval(Var(tag_len, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:780:7)
[Warning][Unknown] Spawning functions from unknown function: line_num (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Not creating a thread from line_num because its type is char [6] (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), StartOf(Var(line_num, NoOffset))) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:844:7)
[Warning][Unknown] Unknown value in args could be an escaped pointer address! (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: Lval(Var(args,
                                   NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(fmt_result, NoOffset)) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:862:3)
[Warning][Unknown] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:864:3)
[Warning][Unknown] Invariant failed: expression "<=(PlusA(Lval(Var(log_len, NoOffset)), CastE(TNamed(size_t, TInt(unsigned long, ), ), Lval(Var(fmt_result, NoOffset)))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:865:3)
[Warning][Unknown] Invariant failed: expression ">(PlusA(PlusA(Lval(Var(log_len, NoOffset)), MinusA(sizeofStr("\033[0m"), Const(Int64(1,unsigned long,None)))), Lval(Var(newline_len, NoOffset))), Const(Int64(200,unsigned long,None)))" not understood. (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:874:3)
[Warning][Deadcode] Function "elog_deinit" will never be called: 6LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:289:1)
[Warning][Deadcode] Function "elog_stop" will never be called: 6LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:318:1)
[Warning][Deadcode] Function "elog_get_text_color_enabled" will never be called: 1LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:366:1)
[Warning][Deadcode] Function "elog_get_output_enabled" will never be called: 1LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:374:1)
[Warning][Deadcode] Function "elog_set_filter" will never be called: 9LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:403:1)
[Warning][Deadcode] Function "elog_set_filter_tag" will never be called: 2LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:447:1)
[Warning][Deadcode] Function "elog_set_filter_kw" will never be called: 2LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:457:1)
[Warning][Deadcode] Function "elog_set_filter_tag_lvl" will never be called: 38LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:511:1)
[Warning][Deadcode] Function "elog_raw" will never be called: 15LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:624:1)
[Warning][Deadcode] Function "elog_assert_set_hook" will never be called: 2LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:946:1)
[Warning][Deadcode] Function "elog_find_lvl" will never be called: 45LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:955:1)
[Warning][Deadcode] Function "elog_find_tag" will never be called: 32LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1068:1)
[Warning][Deadcode] Function "elog_async_deinit" will never be called: 8LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1467:1)
[Warning][Deadcode] Function "elog_file_deinit" will never be called: 12LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1632:1)
[Warning][Deadcode] Function "elog_file_port_deinit" will never be called: 2LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1728:1)
[Warning][Deadcode] Function "lock_deinit" will never be called: 2LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1812:1)
[Warning][Deadcode] Function "elog_port_deinit" will never be called: 3LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1848:1)
[Warning][Deadcode] Function "elog_cpyln" will never be called: 29LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1976:1)
[Warning][Deadcode] Function "elog_memcpy" will never be called: 23LoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:2036:1)
[Warning][Race] Memory location fp@main.c:1505:13 (race with conf. 110):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1615:3)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1616:3)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1625:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1625:3)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1626:3)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1577:3)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1577:3)
[Warning][Race] Memory location buf_is_empty@main.c:1278:14 (race with conf. 110):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1289:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1289:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1338:3)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1361:5)
[Warning][Race] Memory location buf_is_full@main.c:1277:14 (race with conf. 110):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1288:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1288:3)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1296:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1296:3)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1325:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1374:3)
[Warning][Race] Memory location elog.output_is_locked_before_disable@main.c:248:19 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:929:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:937:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:279:3)
  write with {lock:output_lock, thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:474:5)
  write with {lock:output_lock, thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:474:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:488:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:488:5)
[Warning][Race] Memory location down.sem_num@main.c:1692:28 (race with conf. 90):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
  read with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
  write with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Race] Memory location up.sem_num@main.c:1691:28 (race with conf. 90):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
  read with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
  write with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Race] Memory location down.sem_flg@main.c:1692:28 (race with conf. 90):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
  read with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
  write with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Race] Memory location up.sem_flg@main.c:1691:28 (race with conf. 90):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
  read with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
  write with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Race] Memory location down.sem_op@main.c:1692:28 (race with conf. 90):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
  read with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
  write with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1712:5)
[Warning][Race] Memory location up.sem_op@main.c:1691:28 (race with conf. 90):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
  read with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
  write with {thread:([main], {})} (conf. 90) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1723:5)
[Warning][Race] Memory location elog.output_is_locked_before_enable@main.c:248:19 (race with conf. 110):
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:930:7)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:938:7)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:278:3)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:476:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:476:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:490:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:490:5)
[Warning][Race] Memory location read_index@main.c:1276:15 (race with conf. 110):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1285:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1285:3)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1286:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1286:5)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1290:7)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1290:7)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1363:3)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1364:5)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1366:5)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1368:5)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1370:5)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1372:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1366:5)
  write with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1372:5)
[Warning][Race] Memory location write_index@main.c:1275:15 (race with conf. 110):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1285:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1285:3)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1286:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1286:5)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1290:7)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1290:7)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1327:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1328:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1330:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1332:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1334:5)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1336:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1330:5)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1336:5)
[Warning][Race] Memory location elog.output_lock_enabled@main.c:248:19 (race with conf. 110):
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:472:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:472:3)
  read with {thread:([async_output@/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1462:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:486:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:486:3)
  read with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:928:3)
  write with {thread:([main], {})} (conf. 110) (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:927:3)

Summary for all memory locations:
	safe:           37
	vulnerable:      6
	unsafe:          8
	-------------------
	total:          51
Unwinding loop elog_file_rotate.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1550 function elog_file_rotate thread 1
Not unwinding loop elog_file_rotate.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1550 function elog_file_rotate thread 1
Unwinding loop async_output.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1419 function async_output thread 1
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 1
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 1
aborting path on assume(false) at file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1599 function elog_file_write thread 1
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 1
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 1
Unwinding loop elog_file_rotate.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1550 function elog_file_rotate thread 1
Not unwinding loop elog_file_rotate.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1550 function elog_file_rotate thread 1
Not unwinding loop async_output.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1419 function async_output thread 1
Unwinding loop async_output.1 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1417 function async_output thread 1
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 1
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 1
aborting path on assume(false) at file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1599 function elog_file_write thread 1
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 1
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 1
Unwinding loop elog_file_rotate.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1550 function elog_file_rotate thread 1
Not unwinding loop elog_file_rotate.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1550 function elog_file_rotate thread 1
Unwinding loop async_output.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1419 function async_output thread 1
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 1
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 1
aborting path on assume(false) at file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1599 function elog_file_write thread 1
Unwinding loop strlen.0 iteration 1 file <builtin-library-strlen> line 18 function strlen thread 1
Not unwinding loop strlen.0 iteration 2 file <builtin-library-strlen> line 18 function strlen thread 1
Unwinding loop elog_file_rotate.0 iteration 1 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1550 function elog_file_rotate thread 1
Not unwinding loop elog_file_rotate.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1550 function elog_file_rotate thread 1
Not unwinding loop async_output.0 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1419 function async_output thread 1
Not unwinding loop async_output.1 iteration 2 file /mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c line 1417 function async_output thread 1
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/goblint-bench/bench/concrat/EasyLogger/main.c | tee goblint/goblint_output: 0
Lines where datarace may occur: 1177 1178 1179 1185 1186 1199 1200 1202 1203 1207 1208 1223 1224 1230 1231 1285 1286 1287 1288 1289 1290 1291 1296 1297 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1454 1455 1459 1460 1462 1463 1556 1557 1558 1559 1560 1561 1563 1564 1565 1566 1568 1569 1577 1578 1602 1603 1615 1616 1617 1625 1626 1627 1673 1674 1712 1713 1723 1724 1893 1894 1895 1896 1906 1907 1908 1918 1919 1920 1936 1937 1948 1949 278 279 280 472 473 474 475 476 477 486 487 488 489 490 491 717 718 757 758 780 781 844 845 862 863 927 928 929 930 931 937 938 939 
The number of races before goblint filter: 712
The number of races after goblint filter: 56
Race categories: 14
	278(1) - 476(1) elog:
		elog#4..output_is_locked_before_enable elog#9..output_is_locked_before_enable
		elog#4..output_is_locked_before_enable elog#11..output_is_locked_before_enable
		elog#4..output_is_locked_before_enable elog#13..output_is_locked_before_enable
		elog#4..output_is_locked_before_enable elog#15..output_is_locked_before_enable
	278(1) - 490(1) elog:
		elog#4..output_is_locked_before_enable elog#10..output_is_locked_before_enable
		elog#4..output_is_locked_before_enable elog#12..output_is_locked_before_enable
		elog#4..output_is_locked_before_enable elog#14..output_is_locked_before_enable
		elog#4..output_is_locked_before_enable elog#16..output_is_locked_before_enable
	279(1) - 474(1) elog:
		elog#4..output_is_locked_before_disable elog#9..output_is_locked_before_disable
		elog#4..output_is_locked_before_disable elog#11..output_is_locked_before_disable
		elog#4..output_is_locked_before_disable elog#13..output_is_locked_before_disable
		elog#4..output_is_locked_before_disable elog#15..output_is_locked_before_disable
	279(1) - 488(1) elog:
		elog#4..output_is_locked_before_disable elog#10..output_is_locked_before_disable
		elog#4..output_is_locked_before_disable elog#12..output_is_locked_before_disable
		elog#4..output_is_locked_before_disable elog#14..output_is_locked_before_disable
		elog#4..output_is_locked_before_disable elog#16..output_is_locked_before_disable
	927(1) - 472(1) elog:
		elog#2..output_lock_enabled elog#8..output_lock_enabled
		elog#2..output_lock_enabled elog#10..output_lock_enabled
		elog#2..output_lock_enabled elog#12..output_lock_enabled
		elog#2..output_lock_enabled elog#14..output_lock_enabled
	927(1) - 486(1) elog:
		elog#2..output_lock_enabled elog#9..output_lock_enabled
		elog#2..output_lock_enabled elog#11..output_lock_enabled
		elog#2..output_lock_enabled elog#13..output_lock_enabled
		elog#2..output_lock_enabled elog#15..output_lock_enabled
	929(1) - 474(1) elog:
		elog#2..output_is_locked_before_disable elog#9..output_is_locked_before_disable
		elog#2..output_is_locked_before_disable elog#11..output_is_locked_before_disable
		elog#2..output_is_locked_before_disable elog#13..output_is_locked_before_disable
		elog#2..output_is_locked_before_disable elog#15..output_is_locked_before_disable
	929(1) - 488(1) elog:
		elog#2..output_is_locked_before_disable elog#10..output_is_locked_before_disable
		elog#2..output_is_locked_before_disable elog#12..output_is_locked_before_disable
		elog#2..output_is_locked_before_disable elog#14..output_is_locked_before_disable
		elog#2..output_is_locked_before_disable elog#16..output_is_locked_before_disable
	930(1) - 476(1) elog:
		elog#2..output_is_locked_before_enable elog#9..output_is_locked_before_enable
		elog#2..output_is_locked_before_enable elog#11..output_is_locked_before_enable
		elog#2..output_is_locked_before_enable elog#13..output_is_locked_before_enable
		elog#2..output_is_locked_before_enable elog#15..output_is_locked_before_enable
	930(1) - 490(1) elog:
		elog#2..output_is_locked_before_enable elog#10..output_is_locked_before_enable
		elog#2..output_is_locked_before_enable elog#12..output_is_locked_before_enable
		elog#2..output_is_locked_before_enable elog#14..output_is_locked_before_enable
		elog#2..output_is_locked_before_enable elog#16..output_is_locked_before_enable
	937(1) - 474(1) elog:
		elog#3..output_is_locked_before_disable elog#9..output_is_locked_before_disable
		elog#3..output_is_locked_before_disable elog#11..output_is_locked_before_disable
		elog#3..output_is_locked_before_disable elog#13..output_is_locked_before_disable
		elog#3..output_is_locked_before_disable elog#15..output_is_locked_before_disable
	937(1) - 488(1) elog:
		elog#3..output_is_locked_before_disable elog#10..output_is_locked_before_disable
		elog#3..output_is_locked_before_disable elog#12..output_is_locked_before_disable
		elog#3..output_is_locked_before_disable elog#14..output_is_locked_before_disable
		elog#3..output_is_locked_before_disable elog#16..output_is_locked_before_disable
	938(1) - 476(1) elog:
		elog#3..output_is_locked_before_enable elog#9..output_is_locked_before_enable
		elog#3..output_is_locked_before_enable elog#11..output_is_locked_before_enable
		elog#3..output_is_locked_before_enable elog#13..output_is_locked_before_enable
		elog#3..output_is_locked_before_enable elog#15..output_is_locked_before_enable
	938(1) - 490(1) elog:
		elog#3..output_is_locked_before_enable elog#10..output_is_locked_before_enable
		elog#3..output_is_locked_before_enable elog#12..output_is_locked_before_enable
		elog#3..output_is_locked_before_enable elog#14..output_is_locked_before_enable
		elog#3..output_is_locked_before_enable elog#16..output_is_locked_before_enable
Runtime Symex: 293.805s
Unsupported library function!
