[zlib] new case study

With Frama-C, we find an initialization issue in the code; however, once it is fixed, the analysis is long and imprecise due to dynamic memory allocation. Perhaps it is better to wait for a few changes in that regard, or improve the parametrization of the analysis.

changed the description

Still an issue with slow convergence (even using fix/eva/alloc-convergence), visible with:

frama-c  \
  adler32.c \
  compress.c \
  crc32.c \
  deflate.c \
  gzclose.c \
  gzlib.c \
  gzread.c \
  gzwrite.c \
  infback.c \
  inffast.c \
  inflate.c \
  inftrees.c \
  test/minigzip.c \
  trees.c \
  uncompr.c \
  zutil.c \
-eva -eva-precision 0 -eva-alloc-functions imprecise

Le fix de convergence de l'allocation dynamique a déjà été mergé dans master (c'était la MR frama-c/frama-c!4210 pour référence).

La branche fix/eva/alloc-convergence est l'ancien fix qui n'est plus d'actualité, et qui ne devrait pas être meilleur que le master actuel.

Par contre, il y a une typo dans la commande donnée, tu veux utiliser -eva-alloc-builtin imprecise (et non -eva-alloc-functions). Avec la bonne commande, l'analyse termine en 5 minutes environ, et plus de 8000 alarmes.

De ce que je comprends, un problème avec cette option sur ce cas d'étude est que la base faible unique pour représenter toutes les allocations dynamiques contient notamment des pointeurs et est utilisé dans de très nombreux contextes, dont certains créent des garbled mix, et cette base faible devient complètement imprécise et le garbled mix grossit au fur et à mesure de l'analyse.

Mais il y a aussi apparition de garbled mix sans cette option, qui n'ont pas non plus l'air simple à résoudre…

Bref, il faudrait investiguer davantage pour comprendre ce qu'il faudrait améliorer dans Eva pour traiter ce cas d'étude — clairement, pour l'instant, il dépasse les capacités d'analyses de Eva sur l'allocation dynamique.

Merci, ça explique pourquoi je ne retrouvais plus la MR