./goblint --conf conf/svcomp-yaml.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --enable witness.invariant.loop-head --disable witness.invariant.other --disable witness.invariant.accessed --sets ana.specification /mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Unsound] Unknown address in {&opts} has escaped. (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:496:5-496:91)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:496:5-496:91)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:424:1-424:21)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:430:1-430:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:431:1-431:31)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:433:1-433:20)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:434:1-434:34)
[Error][Imprecise][Unsound] Function definition missing for smp_send_req (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:436:1-436:47)
[Info][Imprecise] INVALIDATING ALL GLOBALS! (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:436:1-436:47)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(smp_def_rrlen_arr,
                                     NoOffset)), AddrOf(Var(__tmpTR__int_1, NoOffset)), CastE(TPtr(TComp(struct smp_target_obj, device_name : TArray(TInt(char, ), Some(Const(Int(256,int,256))), ), subvalue : TInt(int, ), sas_addr : TArray(TInt(unsigned char, ), Some(Const(Int(8,int,8))), ), interface_selector : TInt(int, ), opened : TInt(int, ), fd : TInt(int, ), ,  const  ), ), Lval(Var(top, NoOffset))), AddrOf(Var(smp_rr, NoOffset)), Lval(Mem(Lval(Var(op, NoOffset)), Field(verbose:TInt(int, ), NoOffset))) (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:436:1-436:47)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(res,
                                     NoOffset)) (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:436:1-436:47)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:162:4-162:56)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:459:1-459:20)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), PlusPI(StartOf(Var(buff, NoOffset)), Const(Int(1,int,1)))) (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:193:1-193:33)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(k,
                                     NoOffset)) (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:193:1-193:33)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:194:5-194:83)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:194:5-194:83)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:194:5-194:83)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:197:1-197:11)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:197:1-197:11)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:198:1-198:10)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), AddrOf(Var(buff, Index(Lval(Var(bpos, NoOffset)), NoOffset)))) (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:201:5-201:163)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(__tmpTR__int_1,
                                     NoOffset)) (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:201:5-201:163)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:202:5-202:92)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:157:3-157:9)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:213:1-213:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:215:1-215:8)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), PlusPI(StartOf(Var(buff, NoOffset)), Const(Int(1,int,1)))) (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:217:1-217:33)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(k,
                                     NoOffset)) (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:217:1-217:33)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:218:5-218:83)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:218:5-218:83)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:218:5-218:83)
[Warning][Deadcode] Function 'smp_is_naa5' is uncalled: 1 LLoC (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:169:1-172:1)
[Warning][Deadcode] Function 'smp_get_num' is uncalled: 62 LLoC (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:223:1-310:1)
[Warning][Deadcode] Function 'smp_get_llnum' is uncalled: 77 LLoC (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:311:1-412:1)
[Warning][Deadcode] Function 'dStrHex' has dead code:
  on line 186 (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:186-186)
  on line 191 (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:191-191)
  on lines 207..209 (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:207-209)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 91
  dead: 145 (140 in uncalled functions)
  total lines: 236
[Warning][Deadcode][CWE-571] condition 'dword_resp_len < 0x100' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:423:1-423:62)
[Warning][Deadcode][CWE-570] condition 'len <= 0' is always false (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:185:4-185:12)
[Warning][Deadcode][CWE-570] condition 'no_ascii < 0' is always false (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:189:4-189:16)
[Warning][Deadcode][CWE-571] condition 'bpos >= 0' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:201:5-201:163)
[Warning][Deadcode][CWE-571] condition 'bpos + 2 >= 0' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:202:5-202:92)
[Warning][Deadcode][CWE-571] condition 'no_ascii' is always true (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:203:4-203:12)
[Warning][Deadcode][CWE-571] condition '__tmpTR__int_1 >= 0' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:204:3-204:166)
[Warning][Deadcode][CWE-571] condition '__tmpTR__int_1 < 82' is always true (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:204:3-204:166)
SV-COMP result: unknown
[Error][Imprecise][Unsound] Function definition missing for smp_send_req
[Info][Witness] witness generation summary:
  total generation entries: 14

vars = 379    evals = 759    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            1.741s     1.743s    731.21MB      1×
  preprocess                         0.027s     0.026s      0.01MB      1×
  FrontC                             0.006s     0.006s      5.73MB      4×
  Cabs2cil                           0.007s     0.007s      7.13MB      4×
  mergeCIL                           0.003s     0.003s      3.73MB      1×
  analysis                           1.690s     1.691s    708.71MB      1×
    createCFG                          0.002s     0.002s      1.75MB      1×
      handle                             0.001s     0.001s      0.44MB     39×
      iter_connect                       0.002s     0.002s      1.12MB     39×
        computeSCCs                        0.001s     0.001s      0.81MB     40×
    global_inits                       0.003s     0.003s      5.67MB      1×
    solving                            1.671s     1.672s    683.95MB      1×
      S.Dom.equal                        0.002s     0.003s      0.26MB    761×
      cheap_full_reach                   0.001s     0.001s      0.11MB      1×
      postsolver                         0.270s     0.270s    170.00MB      1×
        postsolver_iter                    0.269s     0.269s    169.76MB      1×
    warn_global                        0.002s     0.002s      0.77MB      1×
    witness                            0.001s     0.001s      0.64MB      1×
      determine                          0.001s     0.001s      0.64MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
