./goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-same/../../../results/st-same/ourtool.2023-01-27_15-24-18.files/loop-head/discover_list.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-same/../../../results/st-same/ourtool.2023-01-27_15-24-18.files/loop-head/discover_list.yml/witness.yml --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())) )
[Error][Imprecise][Unsound] Function definition missing for smp_send_req
[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)
[Info][Witness] unassume invariant: func_code <= 255 && 0 <= func_code (/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:162:4-162:56)
[Info][Witness] unassume invariant: func_code <= 255 && 0 <= func_code (/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)
[Info][Witness] unassume invariant: ((((((((((len != 0 && (long long )a >= 0LL) && (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL) && ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL) && k <= 2147483646) && bpos <= 2147483645) && cpos <= 75) && 60 <= cpos) && 5 <= bpos) && 4 <= len) && 0 <= i) && 0 <= a (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4-195:27)
[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)
[Info][Witness] unassume invariant: ((((((((((len != 0 && (long long )a >= 0LL) && (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL) && ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL) && k <= 2147483646) && bpos <= 2147483645) && cpos <= 75) && 60 <= cpos) && 5 <= bpos) && 4 <= len) && 0 <= i) && 0 <= a (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4-195:27)
[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)
[Success][Witness] invariant confirmed: 0 <= a (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: 4 <= len (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: 5 <= bpos (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: 60 <= cpos (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: cpos <= 75 (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: bpos <= 2147483645 (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: k <= 2147483646 (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Warning][Witness] invariant unconfirmed: (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: (long long )a >= 0LL (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: len != 0 (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:195:4)
[Success][Witness] invariant confirmed: 0 <= func_code (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:162:4)
[Success][Witness] invariant confirmed: func_code <= 255 (/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/discover_list.c:162:4)
[Info][Witness] witness validation summary:
  confirmed: 13
  unconfirmed: 1
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 14
SV-COMP result: unknown

vars = 335    evals = 689    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            1.536s     1.549s    765.78MB      1×
  preprocess                         0.028s     0.031s      0.01MB      1×
  FrontC                             0.007s     0.007s      5.73MB      4×
  Cabs2cil                           0.009s     0.009s      7.13MB      4×
  mergeCIL                           0.004s     0.004s      3.73MB      1×
  analysis                           1.479s     1.486s    742.93MB      1×
    createCFG                          0.002s     0.002s      1.75MB      1×
      handle                             0.001s     0.001s      0.44MB     39×
      iter_connect                       0.001s     0.001s      1.12MB     39×
        computeSCCs                        0.001s     0.001s      0.81MB     40×
    FrontC                             0.001s     0.001s      0.19MB     28×
    Cabs2cil                           0.005s     0.005s      2.66MB     28×
    global_inits                       0.004s     0.004s      5.91MB      1×
    solving                            1.439s     1.445s    712.81MB      1×
      S.Dom.equal                        0.002s     0.003s      0.24MB    691×
      base unassume                      0.018s     0.018s     15.00MB     26×
      cheap_full_reach                   0.001s     0.001s      0.11MB      1×
      postsolver                         0.245s     0.246s    172.59MB      1×
        postsolver_iter                    0.244s     0.245s    172.36MB      1×
    warn_global                        0.001s     0.001s      0.83MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
