projects / platform / upstream / llvm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 73927d5) | patch
[clang][dataflow] Support limits on the SAT solver to force timeouts.
authorYitzhak Mandelbaum <yitzhakm@google.com>
Mon, 12 Jun 2023 17:38:31 +0000 (17:38 +0000)
committerYitzhak Mandelbaum <yitzhakm@google.com>
Mon, 12 Jun 2023 18:34:32 +0000 (18:34 +0000)
commitb639ebaa8f83dbed8adeae0a178a43d6115c9590
tree8e035bdc70a46ddf92ef064fe23c0ebaeb0849f1tree | snapshot
parent73927d574f57c1bdf792e2cefe2974b7e9375ed6commit | diff
[clang][dataflow] Support limits on the SAT solver to force timeouts.

This patch allows the client of a `WatchedLiteralsSolver` to specify a
computation limit on the use of the solver. After the limit is exhausted, the
SAT solver times out.

Fixes issues #60265.

Differential Revision: https://reviews.llvm.org/D152732
clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h diff | blob | history
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp diff | blob | history
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp diff | blob | history
Domain: System / Toolchain;