/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume cbmc/discover_list.yml.witness.yml --witness.yaml.validate cbmc/discover_list.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/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. (../plain/discover_list.c:496:5-496:91)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (../plain/discover_list.c:496:5-496:91)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (../plain/discover_list.c:424:1-424:21)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (../plain/discover_list.c:430:1-430:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (../plain/discover_list.c:431:1-431:31)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (../plain/discover_list.c:433:1-433:20)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (../plain/discover_list.c:434:1-434:34)
[Error][Imprecise][Unsound] Function definition missing for smp_send_req (../plain/discover_list.c:436:1-436:47)
[Info][Imprecise] INVALIDATING ALL GLOBALS! (../plain/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))) (../plain/discover_list.c:436:1-436:47)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(res,
                                     NoOffset)) (../plain/discover_list.c:436:1-436:47)
[Info][Witness] unassume invariant: smp_def_rrlen_arr[0].func == 0 (../plain/discover_list.c:162:4-162:56)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:162:4-162:56)
[Info][Witness] unassume invariant: smp_def_rrlen_arr[0].func == 0 (../plain/discover_list.c:162:4-162:56)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/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)))) (../plain/discover_list.c:193:1-193:33)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(k,
                                     NoOffset)) (../plain/discover_list.c:193:1-193:33)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:194:5-194:83)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:194:5-194:83)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (../plain/discover_list.c:194:5-194:83)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:197:1-197:11)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/discover_list.c:197:1-197:11)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/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)))) (../plain/discover_list.c:201:5-201:163)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(__tmpTR__int_1,
                                     NoOffset)) (../plain/discover_list.c:201:5-201:163)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:202:5-202:92)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:157:3-157:9)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:213:1-213:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/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)))) (../plain/discover_list.c:217:1-217:33)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(k,
                                     NoOffset)) (../plain/discover_list.c:217:1-217:33)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:218:5-218:83)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (../plain/discover_list.c:218:5-218:83)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:218:5-218:83)
[Warning][Deadcode] Function 'smp_is_naa5' is uncalled: 1 LLoC (../plain/discover_list.c:169:1-172:1)
[Warning][Deadcode] Function 'smp_get_num' is uncalled: 62 LLoC (../plain/discover_list.c:223:1-310:1)
[Warning][Deadcode] Function 'smp_get_llnum' is uncalled: 77 LLoC (../plain/discover_list.c:311:1-412:1)
[Warning][Deadcode] Function 'dStrHex' has dead code:
  on line 186 (../plain/discover_list.c:186-186)
  on line 191 (../plain/discover_list.c:191-191)
  on lines 207..209 (../plain/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 (../plain/discover_list.c:423:1-423:62)
[Warning][Deadcode][CWE-570] condition 'len <= 0' is always false (../plain/discover_list.c:185:4-185:12)
[Warning][Deadcode][CWE-570] condition 'no_ascii < 0' is always false (../plain/discover_list.c:189:4-189:16)
[Warning][Deadcode][CWE-571] condition 'bpos >= 0' (possibly inserted by CIL) is always true (../plain/discover_list.c:201:5-201:163)
[Warning][Deadcode][CWE-571] condition 'bpos + 2 >= 0' (possibly inserted by CIL) is always true (../plain/discover_list.c:202:5-202:92)
[Warning][Deadcode][CWE-571] condition 'no_ascii' is always true (../plain/discover_list.c:203:4-203:12)
[Warning][Deadcode][CWE-571] condition '__tmpTR__int_1 >= 0' (possibly inserted by CIL) is always true (../plain/discover_list.c:204:3-204:166)
[Warning][Deadcode][CWE-571] condition '__tmpTR__int_1 < 82' is always true (../plain/discover_list.c:204:3-204:166)
[Warning][Witness] invariant unconfirmed: ((smp_def_rrlen_arr[0]).func) == (0) (../plain/discover_list.c:153:1)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: unknown

vars = 379    evals = 759    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            1.771s     1.772s    739.92MB      1×
  preprocess                         0.040s     0.039s      0.01MB      1×
  FrontC                             0.007s     0.007s      5.73MB      4×
  Cabs2cil                           0.007s     0.008s      7.13MB      4×
  mergeCIL                           0.004s     0.004s      3.73MB      1×
  analysis                           1.706s     1.707s    717.62MB      1×
    createCFG                          0.005s     0.005s      1.75MB      1×
      handle                             0.001s     0.001s      0.44MB     39×
      iter_connect                       0.005s     0.005s      1.12MB     39×
        computeSCCs                        0.001s     0.001s      0.81MB     40×
    FrontC                             0.001s     0.001s      0.02MB      2×
    Cabs2cil                           0.001s     0.001s      0.22MB      2×
    global_inits                       0.004s     0.004s      5.95MB      1×
    solving                            1.692s     1.693s    703.51MB      1×
      S.Dom.equal                        0.002s     0.003s      0.26MB    761×
      base unassume                      0.001s     0.001s      1.09MB     11×
      cheap_full_reach                   0.001s     0.001s      0.11MB      1×
      postsolver                         0.261s     0.261s    174.36MB      1×
        postsolver_iter                    0.260s     0.260s    174.13MB      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×
