Skip to content

Commit

Permalink
Fix after rebase 3
Browse files Browse the repository at this point in the history
  • Loading branch information
ladisgin committed Nov 20, 2023
1 parent 26f93a7 commit c2a5ab8
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 9 deletions.
7 changes: 2 additions & 5 deletions lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2951,15 +2951,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
have already got a value. But in the end the caches should
handle it for us, albeit with some overhead. */
do {
if (!isa<ConstantExpr>(v) &&
interpreterOpts.Mock == MockPolicy::Failed) {
if (!first && interpreterOpts.Mock == MockPolicy::Failed) {
free = nullptr;
if (ki->inst->getType()->isSized()) {
prepareMockValue(state, "mockExternResult", ki);
}
} else {
ExecutionState *free = &state;
bool hasInvalid = false, first = true;

v = optimizer.optimizeExpr(v, true);
ref<ConstantExpr> value;
bool success = solver->getValue(free->constraints.cs(), v, value,
Expand Down
6 changes: 2 additions & 4 deletions tools/klee/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -374,8 +374,7 @@ cl::opt<bool> MockModeledFunction(
cl::init(false), cl::cat(MockCat));

cl::opt<MockPolicy>
Mock("mock-policy", cl::init(MockPolicy::None),
cl::desc("Specify policy for mocking external calls"),
Mock("mock-policy", cl::desc("Specify policy for mocking external calls"),
cl::values(clEnumValN(MockPolicy::None, "none",
"No mock function generated"),
clEnumValN(MockPolicy::Failed, "failed",
Expand All @@ -386,8 +385,7 @@ cl::opt<MockPolicy>
cl::init(MockPolicy::None), cl::cat(MockCat));

cl::opt<MockStrategyKind> MockStrategy(
"mock-strategy", cl::init(MockStrategyKind::Naive),
cl::desc("Specify strategy for mocking external calls"),
"mock-strategy", cl::desc("Specify strategy for mocking external calls"),
cl::values(
clEnumValN(MockStrategyKind::Naive, "naive",
"Every time external function is called, new symbolic value "
Expand Down

0 comments on commit c2a5ab8

Please sign in to comment.