diff options
| author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2021-03-20 22:10:03 +0000 |
|---|---|---|
| committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2021-04-20 11:42:23 +0100 |
| commit | e2cb581253b18b50d6526cc4a28ee7ff933a29bf (patch) | |
| tree | b4f0809619cadb0d60b456ce364c8f066ef944d2 /lib/Core | |
| parent | 458e3f9ec4f8d5d2711a0aeff7a532b184e7d075 (diff) | |
| download | klee-e2cb581253b18b50d6526cc4a28ee7ff933a29bf.tar.gz | |
Refactored maxStaticPctChecks into a sequence of conditions.
Diffstat (limited to 'lib/Core')
| -rw-r--r-- | lib/Core/Executor.cpp | 28 |
1 files changed, 19 insertions, 9 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 7bfc0dac..6891dc93 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -986,18 +986,28 @@ ref<Expr> Executor::maxStaticPctChecks(ExecutionState ¤t, StatisticManager &sm = *theStatisticManager; CallPathNode *cpn = current.stack.back().callPathNode; - if ((MaxStaticForkPct < 1. && - sm.getIndexedValue(stats::forks, sm.getIndex()) > - stats::forks * MaxStaticForkPct) || - (MaxStaticCPForkPct < 1. && cpn && - (cpn->statistics.getValue(stats::forks) > - stats::forks * MaxStaticCPForkPct)) || + + bool reached_max_fork_limit = + (MaxStaticForkPct < 1. && + (sm.getIndexedValue(stats::forks, sm.getIndex()) > + stats::forks * MaxStaticForkPct)); + + bool reached_max_cp_fork_limit = (MaxStaticCPForkPct < 1. && cpn && + (cpn->statistics.getValue(stats::forks) > + stats::forks * MaxStaticCPForkPct)); + + bool reached_max_solver_limit = (MaxStaticSolvePct < 1 && - sm.getIndexedValue(stats::solverTime, sm.getIndex()) > - stats::solverTime * MaxStaticSolvePct) || + (sm.getIndexedValue(stats::solverTime, sm.getIndex()) > + stats::solverTime * MaxStaticSolvePct)); + + bool reached_max_cp_solver_limit = (MaxStaticCPForkPct < 1. && cpn && (cpn->statistics.getValue(stats::solverTime) > - stats::solverTime * MaxStaticCPSolvePct))) { + stats::solverTime * MaxStaticCPSolvePct)); + + if (reached_max_fork_limit || reached_max_cp_fork_limit || + reached_max_solver_limit || reached_max_cp_solver_limit) { ref<klee::ConstantExpr> value; bool success = solver->getValue(current.constraints, condition, value, current.queryMetaData); |