steakhal added inline comments.
================ Comment at: clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c:6 + +// Mock implementation: return UNDEF for the 5th invocation, otherwise it just +// returns the result of the real invocation. ---------------- martong wrote: > It's not clear why we have to wait for the 5th invocation. Can't we return > UNDEF for the first time? That would eliminate the need to call the > originalFN. > > By the way why do we have call the original, can't we just return immediately > with Z3_L_TRUE? Excellent questions, I should have clarified these upfront! > It's not clear why we have to wait for the 5th invocation. Probably lies in how the exploded graph is built up. I was also surprised that it was hit exactly 5 times. > Can't we return UNDEF for the first time? That way we would not reach the 2nd `Solver->check()` call, just simply early return. > That would eliminate the need to call the originalFN. Unfortunately, the side-effect is also required. `Solver->check()` creates a model which is accessed by `Solver->getInterpretation(Exp, Value)`. I don't really want to mock that representation as well. We could though. I'm gonna have a look at that. > By the way why do we have call the original, can't we just return immediately > with Z3_L_TRUE? We could, but as we have to call the original regardless, there is no point doing that. This way it can mimic the exact behavior that the Z3 would do, and diverge only for the 5th time. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D83660/new/ https://reviews.llvm.org/D83660 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
