diff options
| author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-12-22 19:52:12 +0000 |
|---|---|---|
| committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2021-04-20 11:42:23 +0100 |
| commit | c8ef08267fd5e67f40defac1ae692e8ec906fa3f (patch) | |
| tree | fa09f1ffa7bac2b2a75b6e32c67dd7cf904bce02 /lib/Core | |
| parent | 88893697f6630f0d281d21be6362489e616bca2f (diff) | |
| download | klee-c8ef08267fd5e67f40defac1ae692e8ec906fa3f.tar.gz | |
Added -max-static-pct-check-delay to replace the hardcoded delay after which the MaxStatic*Pct checks are performed.
Diffstat (limited to 'lib/Core')
| -rw-r--r-- | lib/Core/Executor.cpp | 12 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 3 |
2 files changed, 14 insertions, 1 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index cea7f173..cc3ac50f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -365,6 +365,12 @@ cl::opt<double> MaxStaticCPSolvePct( "instructions (default=1.0 (always))"), cl::cat(TerminationCat)); +cl::opt<std::string> MaxStaticPctCheckDelay( + "max-static-pct-check-delay", + cl::desc("Time after which the --max-static-*-pct checks are enforced (default=60s)"), + cl::init("60s"), + cl::cat(TerminationCat)); + cl::opt<std::string> TimerInterval( "timer-interval", cl::desc("Minimum interval to check timers. " @@ -485,6 +491,8 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, this->solver = new TimingSolver(solver, EqualitySubstitution); memory = new MemoryManager(&arrayCache); + maxStaticPctCheckDelay = time::Span{MaxStaticPctCheckDelay}; + initializeSearchOptions(); if (OnlyOutputStatesCoveringNew && !StatsTracker::useIStats()) @@ -971,7 +979,9 @@ ref<Expr> Executor::maxStaticPctChecks(ExecutionState ¤t, MaxStaticCPForkPct == 1. && MaxStaticCPSolvePct == 1.) return condition; - if (statsTracker->elapsed() <= time::seconds(60)) + // these checks are performed only after MaxStaticPctCheckDelay time has + // passed since execution started + if (statsTracker->elapsed() <= maxStaticPctCheckDelay) return condition; StatisticManager &sm = *theStatisticManager; diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index ae960731..db8e508c 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -205,6 +205,9 @@ private: /// Maximum time to allow for a single instruction. time::Span maxInstructionTime; + /// Time after which the --max-static-*-pct checks are enforced + time::Span maxStaticPctCheckDelay; + /// Assumes ownership of the created array objects ArrayCache arrayCache; |