Skip to content

Commit

Permalink
clang format
Browse files Browse the repository at this point in the history
  • Loading branch information
ladisgin committed Nov 13, 2023
1 parent 543a1e2 commit 9c0048e
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 7 deletions.
12 changes: 6 additions & 6 deletions include/klee/Core/Interpreter.h
Original file line number Diff line number Diff line change
Expand Up @@ -69,15 +69,15 @@ using FLCtoOpcode = std::unordered_map<
unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;

enum class MockStrategyKind {
Naive, // For each function call new symbolic value is generated
Deterministic // Each function is treated as uninterpreted function in SMT.
// Compatible with Z3 solver only
Naive, // For each function call new symbolic value is generated
Deterministic // Each function is treated as uninterpreted function in SMT.
// Compatible with Z3 solver only
};

enum class MockPolicy {
None, // No mock function generated
Failed, // Generate symbolic value for failed external calls
All // Generate IR module with all external values
None, // No mock function generated
Failed, // Generate symbolic value for failed external calls
All // Generate IR module with all external values
};

class Interpreter {
Expand Down
2 changes: 1 addition & 1 deletion lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -490,7 +490,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
inhibitForking(false), coverOnTheFly(false),
haltExecution(HaltExecution::NotHalt), ivcEnabled(false),
debugLogBuffer(debugBufferString) {
if (interpreterOpts.MockStrategy == MockStrategyKind::Deterministic &&
if (interpreterOpts.MockStrategy == MockStrategyKind::Deterministic &&
CoreSolverToUse != Z3_SOLVER) {
klee_error("Deterministic mocks can be generated with Z3 solver only.\n");
}
Expand Down

0 comments on commit 9c0048e

Please sign in to comment.