martong added a comment. In D79431#2265155 <https://reviews.llvm.org/D79431#2265155>, @Szelethus wrote:
> In D79431#2263693 <https://reviews.llvm.org/D79431#2263693>, @martong wrote: > >> In D79431#2263690 <https://reviews.llvm.org/D79431#2263690>, @martong wrote: >> >>> What if we'd add a `toString` method to the constraints and we'd add this >>> to `Msg`? This way we'd know the contents of the constraint, thus we we'd >>> know //how// the constraint is violated. >> >> I mean we'd know what is not satisfied. But, to know why exactly that is not >> satisfied we should dump the whole `State` but that's obviously not an >> option. Perhaps we could track which symbols and expressions are >> participating in the assumption related to the constraint and we could dump >> only those, but this seems to be a very complex approach. > > I realize that the //how// and //why// phrases in this context a bit too > vague :) What do you mean under having to dump the whole `State`? I didn't > mean to compress a bug path into a warning message, only what I mentioned in > D79431#2020951 <https://reviews.llvm.org/D79431#2020951>. In any case, I > think its okay to just move on with this patch. LGTM! First, thanks for the review! Second, "dumping the whole State" is an overstatement. What I meant is this: to properly explain to the user how the constraint is failed is a hard task. Because we should dig up all symbols and expressions that are related to the constraint and we should dump their values. E.g. consider the violation of a range constraint here, ssize_t send(int socket, const void *buffer, size_t length, int flags); void foo() { if (socket < 0) send(socket, buf, buflen, flags); // constraint violation for 'socket' it should be in [0, IntMax] } We should print something like this: `'socket' it should be in [0, IntMax] but it is in [IntMin, -1]` In this example, the related symbol is only `socket` but this could be more complex, e.g. if the constraint is related to a buffer size ... Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D79431/new/ https://reviews.llvm.org/D79431 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits