./goblint --enable dbg.warn_with_context --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
Collected factors:
functions: 33
functionCalls: 105
loops: 6
loopBreaks: 0
controlFlowStatements: 126
expressions: 1098
instructions: 235
integralVars: (4,51)
arrayVars: (2,0)
pointerVars: (1,26)

Complexity estimates:
File: 1772
Total: 8994
Congruence: 1570
Enabled congruence domain.
Octagon: 3000
Enabled octagon domain for:
printf, exit, i, key, count, a, tmp, j, count, k, size, a, b, c, i, top, timerid1, timerid2, timer_getoverrun_timerid1, timer_getoverrun_timerid2, argc, its, thread, tmp, now, rt, args, sig
Widening: 2652
Enabled widening thresholds
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[Info][Imprecise] Invalidating expressions: & now in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:350:3-350:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:351:3-351:38)
[Info][Imprecise] Invalidating expressions: stdout in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:355:3-355:17)
[Info][Unsound] Unknown address in stdout has escaped. in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:355:3-355:17)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:355:3-355:17)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:355:3-355:17)
[Info][Imprecise] Invalidating expressions: & rt in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:357:3-358:86)
[Info][Imprecise] Invalidating expressions: & attr in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:365:3-365:32)
[Info][Imprecise] Invalidating expressions: & attr in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:366:3-366:39)
[Info][Imprecise] Invalidating expressions: (pthread_cond_t * __restrict  )(& monotonic_cond) in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:367:3-367:124)
[Info][Imprecise] Invalidating expressions: & now in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:368:3-368:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:369:3-369:38)
[Info][Imprecise] Invalidating expressions: stdout in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:374:3-374:17)
[Info][Unsound] Unknown address in stdout has escaped. in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:374:3-374:17)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:374:3-374:17)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:374:3-374:17)
[Info][Imprecise] Invalidating expressions: & rt in context 1777922861269581824 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:376:3-377:86)
[Info][Unsound] Unknown address in {&ret} has escaped. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:426:3-426:30)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:426:3-426:30)
[Info][Imprecise] Invalidating expressions: & sa.sa_mask in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:429:3-429:28)
[Info][Imprecise] Invalidating expressions: (struct sigaction * __restrict  )((void *)0) in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:430:3-430:117)
[Info][Imprecise] Invalidating expressions: & tmp in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:430:3-430:117)
[Info][Unsound] Unknown address in {&sa} has escaped. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:430:3-430:117)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:430:3-430:117)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:430:3-430:117)
[Info][Imprecise] Invalidating expressions: & mask in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:436:3-436:22)
[Info][Imprecise] Invalidating expressions: & mask in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:437:3-437:24)
[Info][Imprecise] Invalidating expressions: (sigset_t * __restrict  )((void *)0) in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:438:3-438:108)
[Info][Imprecise] Invalidating expressions: & tmp___0 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:438:3-438:108)
[Info][Imprecise] Invalidating expressions: (struct sigevent * __restrict  )(& sev), (timer_t * __restrict  )(& timerid1) in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:446:3-446:107)
[Info][Imprecise] Invalidating expressions: & tmp___1 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:446:3-446:107)
[Info][Imprecise] Invalidating expressions: (struct itimerspec * __restrict  )((void *)0) in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:455:3-456:73)
[Info][Imprecise] Invalidating expressions: & tmp___2 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:455:3-456:73)
[Info][Imprecise] Invalidating expressions: (struct sigevent * __restrict  )(& sev), (timer_t * __restrict  )(& timerid2) in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:462:3-462:107)
[Info][Imprecise] Invalidating expressions: & tmp___3 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:462:3-462:107)
[Info][Imprecise] Invalidating expressions: & its.it_value in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:467:3-467:35)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:468:3-468:28)
[Info][Imprecise] Invalidating expressions: (struct itimerspec * __restrict  )((void *)0) in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:471:3-472:73)
[Info][Imprecise] Invalidating expressions: & tmp___4 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:471:3-472:73)
[Info][Imprecise] Invalidating expressions: & now in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:477:3-477:14)
[Info][Imprecise] Invalidating expressions: & tmp___5 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:478:3-478:45)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:479:3-480:18)
[Info][Imprecise] Invalidating expressions: (time_t *)((void *)0) in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:481:3-481:40)
[Info][Imprecise] Invalidating expressions: & tmp___6 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:481:3-481:40)
[Info][Imprecise] Invalidating expressions: & tb in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:484:3-484:14)
[Info][Imprecise] Invalidating expressions: & tmp___7 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:485:3-485:49)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:486:3-487:18)
[Info][Imprecise] Invalidating expressions: stdout in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:489:3-489:17)
[Info][Unsound] Unknown address in stdout has escaped. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:489:3-489:17)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:489:3-489:17)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:489:3-489:17)
[Info][Imprecise] Invalidating expressions: (struct timeval * __restrict  )(& tv), (void * __restrict  )((void *)0) in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:494:3-494:88)
[Info][Imprecise] Invalidating expressions: & tmp___8 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:495:3-495:51)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:496:3-497:18)
[Info][Imprecise] Invalidating expressions: (sigset_t * __restrict  )((void *)0) in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:498:3-498:108)
[Info][Imprecise] Invalidating expressions: & tmp___9 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:498:3-498:108)
[Info][Imprecise] Invalidating expressions: & ts in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:503:3-503:25)
[Info][Imprecise] Invalidating expressions: & tmp___10 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:504:3-504:52)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:505:3-506:19)
[Info][Imprecise] Invalidating expressions: & tmp___11 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:507:3-507:40)
[Info][Imprecise] Invalidating expressions: & its in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:513:3-513:33)
[Info][Imprecise] Invalidating expressions: & tmp___12 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:514:3-514:40)
[Info][Imprecise] Invalidating expressions: & its in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:520:3-520:33)
[Info][Imprecise] Invalidating expressions: (struct stat * __restrict  )(& buf) in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:521:3-521:87)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:521:3-521:87)
[Info][Imprecise] Invalidating expressions: & tmp___13 in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:522:3-522:61)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2419511831562027008 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:523:3-524:19)
[Warning][Deadcode] Function 'handler' is uncalled: 5 LLoC (/mnt/goblint-svcomp/goblint-bench/bench/concrat/libfaketime/main.c:305:1-318:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 137
  dead: 5 (5 in uncalled functions)
  total lines: 142
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
[Info][Race] Memory locations race summary:
  safe: 1
  vulnerable: 0
  unsafe: 0
  total memory locations: 1
