martong added a comment. > As of diff 5, line 1767 and all the code in the block at line 2184 are > uncovered by the tests you provided.
Thanks, I've added new tests that cover the re-assume logic (the block of line 2184). However, I was unable to add a test that covers the case when the simplification of a trivial symbol in the disequality info results an infeasible state (line 1767). Here is how I tried: I had changed the line to an assertion and then initiated the static analysis of the following opensource projects: memcached,tmux,curl,twin,redis,vim,openssl,sqlite,ffmpeg,postgresql,tinyxml2,libwebm,xerces,bitcoin,protobuf. My idea had been, if the assertion would fired then I would use creduce to the create the test case (btw, this is how I added the other infeasible state test case). However, it did not fired. IMHO, having a defensive check at L1767 is correct b/c there is a slight chance of reaching an infeasible state there. Although the chance is minimal, I cannot prove that is 0. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D106823/new/ https://reviews.llvm.org/D106823 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
