baloghadamsoftware added a comment. Here is the proof of the algorithm for `signed char` and `unsigned char` types. The dumper which tests every `n` for the `n*k <comparison operator> m` relation and creates ranges from values satisfying the expression for every `k` and `m` produces exactly the same output as the generator which generates the ranges using the algorithm from the patch. One the machine I run them they take between 30 and 60 seconds to run.
F7551311: proof.tar.bz2 <https://reviews.llvm.org/F7551311> https://reviews.llvm.org/D49074 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits