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.