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
  • [PATCH] D49074: [Analyzer]... Balogh , Ádám via Phabricator via cfe-commits
    • [PATCH] D49074: [Anal... Balogh , Ádám via Phabricator via cfe-commits

Reply via email to