xazax.hun accepted this revision. xazax.hun added a comment. Very cool! Thanks for investing into fixing the soundness issues!
A couple of ideas for the future (probably you are already aware of most of this, but open communication can help other members of the community to jump in): - Some frameworks have the option to delay widening. I.e., only invoke the widening operator when the analysis of a loop did not converge after a certain number of iterations. - Some frameworks implement narrowing. In the narrowing phase, we would do a couple more iterations but using the regular join instead of the widening operator. Sometimes doing multiple narrow/widen phases can be beneficial. - Writing a widening operator can be tricky. It would be nice to add some guidance to the documentation. E.g., listing some of the algebraic properties that we expect a widening operator to have can be a lot of help for newcommers (like `bottom.widen(lat) == lat`). Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D131645/new/ https://reviews.llvm.org/D131645 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits