================
@@ -213,6 +215,15 @@ ANALYZER_OPTION(
"400'000 should on average make Z3 queries run for up to 100ms on modern "
"hardware. Set 0 for unlimited.", 0)
+ANALYZER_OPTION(
+ unsigned, Z3CrosscheckRetriesOnTimeout,
+ "crosscheck-with-z3-retries-on-timeout",
+ "Set how many times the oracle is allowed to retry a Z3 query. "
+ "Set 0 for not allowing retries, in which case each Z3 query would be "
+ "attempted only once. Increasing the number of retries is often more "
----------------
NagyDonat wrote:
I would suggest using `crosscheck-with-z3-attempts-on-timeout` (because this is
the "natural quantity"), documenting that _this must be a positive integer_ and
reporting a clear error in the unlikely case when an user still tries to
specify `crosscheck-with-z3-attempts-on-timeout=0`.
I don't think that this would "trap" too many users (because when they read
about the existence of this option, they immediately see that its value is a
positive integer) -- and even if they somehow end up with specifying 0, they
get a visible error message that asks them to clarify their intentions.
On the other hand, the `crosscheck-with-z3-retries-on-timeout` option _is_ a
trap, because if the user misunderstands its meaning (and does not notice the
pedantic details that 'number of _retries_' does not count the first attempt),
the analyzer will silently do the wrong thing.
Among the two options that you listed, I think 1. is acceptable but not ideal
(when the user just wants to simply enable/disable this crosscheck feature,
they should not bother with technical details like retries). About option 2.
(keep the current state of the commit) I'd say that I still dislike it, but if
another reviewer accepts your reasoning and favors that solution, then I won't
block merging it.
https://github.com/llvm/llvm-project/pull/120239
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
