WGet2

[michael-schwarz]

https://gitlab.com/gnuwget/wget2

./configure
bear make
./goblint -v .

Fails because of a _Static_assert:

_Static_assert (2 * sa_alignment_max - 1 <= (small_t) -1, "verify (" "2 * sa_alignment_max - 1 <= (small_t) -1" ")");

[michael-schwarz]

After goblint/cil#62 we now get a new parser error with

#pragma clang diagnostic ignored "-Wunreachable-code"

[michael-schwarz]

With goblint/cil#63 the issue is now with _Alignof:

_Alignof (struct struniq_hash_node) 

[michael-schwarz]

With 7e88cff56df1b2e636f94572b312315fa65b7f3c and goblint/cil#66, the analysis succeeds:

Timings:
TOTAL                          36.298 s
  parse                          12.566 s
  convert to CIL                 15.271 s
  analysis                        8.462 s
    global_inits                    5.431 s
    solving                         1.698 s
      S.Dom.equal                     0.002 s
      postsolver                      0.877 s
    warn_global                     0.001 s
Timing used
Memory statistics: total=37931.30MB, max=2160.46MB, minor=37792.03MB, major=2872.40MB, promoted=2733.13MB
    minor collections=18044  major collections=29 compactions=0

[michael-schwarz]

This was with the broken old bear, I am now trying again with compiledb.

[michael-schwarz]

CIL also once more fails with parsing its own output here :/

After manually fixing the arguments of yyalloc and yyrealloc it works:
wget2-fixed.cil.zip

[michael-schwarz]

Live lines: 76
[Warning][Deadcode] Function 'wget_hpkp_db_init' has dead code:
  on line 480 (hpkp_db.c:480-480)
  on line 477 (hpkp_db.c:477-477)
  on line 472 (hpkp_db.c:472-472)
Found dead code on 18756 lines (including 18753 in uncalled functions)!
Total lines (logical LoC): 18832

That is also very problematic here

[michael-schwarz]

Ok, the main file is not the one we really want, it comes from #line 8 "test_linking_hpkp_db.c" here.