steakhal added a comment. In D77792#1971921 <https://reviews.llvm.org/D77792#1971921>, @Szelethus wrote:
> You seem to have forgotten `-U9999` :^) Nice catch! ================ Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:774 +Optional<ProgramStateRef> RangeConstraintManager::tryAssumeSymSymOp( + ProgramStateRef State, BinaryOperator::Opcode Op, SymbolRef LHSSym, ---------------- martong wrote: > Is it possible to ever return with `None`? Other `assume` functions usually > just return with `nullptr` on infeasible state as you do. What would be the > meaning if `None` is returned, is that another kind of infeasibility? The rest of the functions there is no `maybe` answer. There is always `yes` or `no`, returning the `State` or the `nullptr`. In our case, we don't know in advance that we know a definitive answer. Imagine the following: When the analyzer sees the `a < b` comparison. It queries whether it `canReasonAbout()`. In our case that would return `true` due to my change. When tries to reason about the given `SymSymExpr` (`a < b`), we don't know if the corresponding value ranges of `a` and `b` are disjunct or not, we need to check that. If we can prove that the ranges are disjunct (or just connected: `a: [a1,x]` and `b: [x,b2]`) then we know an answer. That can be `true` (`State`) or `false` (`nullptr`). Otherwise the result should be `UNKNOWN` (`llvm::None`). ================ Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:797 + + switch (Op) { + case BO_LT: ---------------- martong wrote: > Perhaps this hunk could be greatly simplified if `CompareResult` was actually > `BinaryOperator::Opcode`. > > Maybe (?): > ``` > if (Res == Op) > return State; > return InfeasibleState; > ``` Honestly, I had exactly the same thoughts. I think an `Opcode` is a different thing than a result of a comparison. Here, we have a partial ordering among `RangeSet`s. But you can convince me :) But I agree, it looks clunky, looking forward to a better solution. Any idea? ================ Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:70 + +// [2,5] and [5,10] +void test_range6(int l, int r) { ---------------- martong wrote: > How is it different than `// [0,5] and [5,10]`? It covers the same. I just wanted a full and clear showcase of the possible intervals. I can be convinced to remove this testcase. ================ Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:172 +} + ---------------- martong wrote: > I think we could benefit from tests for cases like this: > ``` > {[0,1],[5,6]} < {[9,9],[11,42],[44,44]} > ``` Really good idea. I added tests for these. But I'm not really sure what's going on there :D I'm sure that these test cases are not testing what I meant to test. //(The exploded graphs are showing that each subrange is assumed for a given value (`l` and `r`) on a given path)// Any idea of how to express the proper value ranges? CHANGES SINCE LAST ACTION https://reviews.llvm.org/D77792/new/ https://reviews.llvm.org/D77792 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits