From 93a4929ad743e3ca9835e183f0e93179ea05e6e8 Mon Sep 17 00:00:00 2001 From: Aleksei Babushkin Date: Mon, 30 Sep 2024 19:26:10 +0500 Subject: [PATCH] [style] --- include/klee/ADT/ImmutableList.h | 22 ++++++------ include/klee/Core/Interpreter.h | 1 - include/klee/Expr/Constraints.h | 1 - include/klee/Expr/SourceBuilder.h | 6 ++-- include/klee/Expr/SymbolicSource.h | 2 +- include/klee/Module/CodeGraphInfo.h | 3 +- include/klee/Module/KInstruction.h | 2 -- include/klee/Module/KModule.h | 2 -- include/klee/Module/TargetForest.h | 2 +- lib/Core/BidirectionalSearcher.cpp | 2 -- lib/Core/Composer.cpp | 53 +++++++++++++++-------------- lib/Core/Composer.h | 22 ++++++------ lib/Core/DistanceCalculator.cpp | 9 +++-- lib/Core/DistanceCalculator.h | 3 +- lib/Core/Executor.cpp | 33 +++++++++--------- lib/Core/Executor.h | 8 ++--- lib/Core/Memory.h | 1 - lib/Core/ObjectManager.cpp | 4 +-- lib/Core/ObjectManager.h | 2 +- lib/Core/ProofObligation.cpp | 3 +- lib/Core/TargetedExecutionManager.h | 1 - lib/Expr/Constraints.cpp | 1 - lib/Expr/Lemma.cpp | 4 +-- 23 files changed, 87 insertions(+), 100 deletions(-) diff --git a/include/klee/ADT/ImmutableList.h b/include/klee/ADT/ImmutableList.h index 969a40a453..d8b8d5916b 100644 --- a/include/klee/ADT/ImmutableList.h +++ b/include/klee/ADT/ImmutableList.h @@ -39,9 +39,9 @@ template class ImmutableList { } } - ImmutableListNode(std::shared_ptr prev, size_t prev_len, std::vector values) - : prev(prev), prev_len(prev_len), values(std::move(values)) { - } + ImmutableListNode(std::shared_ptr prev, size_t prev_len, + std::vector values) + : prev(prev), prev_len(prev_len), values(std::move(values)) {} }; std::shared_ptr node; @@ -108,7 +108,8 @@ template class ImmutableList { if (!node) { return; } - node = std::make_shared(node->prev, node->prev_len, node->values); + node = std::make_shared(node->prev, node->prev_len, + node->values); node->values.pop_back(); } @@ -129,11 +130,10 @@ template class ImmutableList { return *it; } - const T& front() const { - return at(0); - } + const T &front() const { return at(0); } - friend bool operator==(const ImmutableList &lhs, const ImmutableList &rhs) { + friend bool operator==(const ImmutableList &lhs, + const ImmutableList &rhs) { if (lhs.size() != rhs.size()) { return false; } @@ -151,11 +151,13 @@ template class ImmutableList { return true; } - friend bool operator!=(const ImmutableList &lhs, const ImmutableList &rhs) { + friend bool operator!=(const ImmutableList &lhs, + const ImmutableList &rhs) { return !(lhs == rhs); } - friend bool operator<(const ImmutableList &lhs, const ImmutableList &rhs) { + friend bool operator<(const ImmutableList &lhs, + const ImmutableList &rhs) { if (lhs.size() < rhs.size()) { return true; } else if (lhs.size() > rhs.size()) { diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index d3788fa89d..c3c88d640c 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -86,7 +86,6 @@ enum class MockMutableGlobalsPolicy { All, // Mock globals on module build stage and generate bc module for it }; - enum class ExecutionKind { Forward, Bidirectional }; class Interpreter { diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h index a1fa1fd9e7..595d749593 100644 --- a/include/klee/Expr/Constraints.h +++ b/include/klee/Expr/Constraints.h @@ -112,7 +112,6 @@ class ConstraintSet { std::vector> &result) const; }; - class PathConstraints { public: using ordered_constraints_ty = diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h index afec8fd65e..dd60560a3e 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -29,9 +29,9 @@ class SourceBuilder { symbolicSizeConstantAddress(unsigned version, const KGlobalVariable *allocSite, ref size); - static ref symbolicSizeConstantAddress(unsigned version, - const KValue *allocSite, - ref size); + static ref + symbolicSizeConstantAddress(unsigned version, const KValue *allocSite, + ref size); static ref makeSymbolic(const std::string &name, unsigned version); diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index f7ad20e647..ab18377d58 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -7,8 +7,8 @@ #include "llvm/ADT/StringExtras.h" #include "llvm/IR/Argument.h" -#include "llvm/IR/Instruction.h" #include "llvm/IR/GlobalVariable.h" +#include "llvm/IR/Instruction.h" #include #include diff --git a/include/klee/Module/CodeGraphInfo.h b/include/klee/Module/CodeGraphInfo.h index 9383ad3f32..3f2dbd8fce 100644 --- a/include/klee/Module/CodeGraphInfo.h +++ b/include/klee/Module/CodeGraphInfo.h @@ -70,8 +70,7 @@ class CodeGraphInfo { const FunctionDistanceMap &getBackwardDistance(KFunction *kf); void getNearestPredicateSatisfying(KBlock *from, KBlockPredicate predicate, - bool forward, - KBlockSet &result); + bool forward, KBlockSet &result); const KBlockMap> &getFunctionBranches(KFunction *kf); diff --git a/include/klee/Module/KInstruction.h b/include/klee/Module/KInstruction.h index 7d9da17439..a3545523db 100644 --- a/include/klee/Module/KInstruction.h +++ b/include/klee/Module/KInstruction.h @@ -136,7 +136,6 @@ struct KInstruction : public KValue { } }; - struct CallStackFrame { KInstruction *caller; KFunction *kf; @@ -173,7 +172,6 @@ struct CallStackFrame { } }; - struct KGEPInstruction : KInstruction { /// indices - The list of variable sized adjustments to add to the pointer /// operand to execute the instruction. The first element is the operand diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h index a43c9b8b9a..ba60b29622 100644 --- a/include/klee/Module/KModule.h +++ b/include/klee/Module/KModule.h @@ -176,8 +176,6 @@ struct PredicateAdapter { InitializerPredicate &predicate; }; - - struct KBasicBlock : public KBlock { public: KBasicBlock(KFunction *, llvm::BasicBlock *, KModule *, diff --git a/include/klee/Module/TargetForest.h b/include/klee/Module/TargetForest.h index 75c71ce9d4..0f06ce1828 100644 --- a/include/klee/Module/TargetForest.h +++ b/include/klee/Module/TargetForest.h @@ -237,7 +237,7 @@ class TargetForest { Layer(const InternalLayer &forest, const TargetsToVector &targetsToVector, confidence::ty confidence) : forest(forest), targetsToVector(targetsToVector), - confidence(confidence) { + confidence(confidence) { for (auto &targetVect : targetsToVector) { targets.insert(targetVect.first); } diff --git a/lib/Core/BidirectionalSearcher.cpp b/lib/Core/BidirectionalSearcher.cpp index 00b9a8499c..574952dd53 100644 --- a/lib/Core/BidirectionalSearcher.cpp +++ b/lib/Core/BidirectionalSearcher.cpp @@ -21,7 +21,6 @@ llvm::cl::opt BackwardTicks("backward-ticks", llvm::cl::desc(""), llvm::cl::init(25), llvm::cl::cat(ExecCat)); - BidirectionalSearcher::StepKind BidirectionalSearcher::selectStep() { size_t initial_choice = ticker.getCurrent(); size_t choice = initial_choice; @@ -141,7 +140,6 @@ BidirectionalSearcher::~BidirectionalSearcher() { delete initializer; } - ref ForwardOnlySearcher::selectAction() { return new ForwardAction(&searcher->selectState()); } diff --git a/lib/Core/Composer.cpp b/lib/Core/Composer.cpp index 7c77cf7b80..556c56a324 100644 --- a/lib/Core/Composer.cpp +++ b/lib/Core/Composer.cpp @@ -11,9 +11,8 @@ using namespace klee; using namespace llvm; bool ComposeHelper::collectMemoryObjects( - ExecutionState &state, ref address, - KInstruction *target, ref &guard, - std::vector> &resolveConditions, + ExecutionState &state, ref address, KInstruction *target, + ref &guard, std::vector> &resolveConditions, std::vector> &unboundConditions, ObjectResolutionList &resolvedMemoryObjects) { bool mayBeOutOfBound = true; @@ -28,10 +27,10 @@ bool ComposeHelper::collectMemoryObjects( } ref checkOutOfBounds; - if (!checkResolvedMemoryObjects( - state, address, 0, mayBeResolvedMemoryObjects, - hasLazyInitialized, resolvedMemoryObjects, resolveConditions, - unboundConditions, checkOutOfBounds, mayBeOutOfBound)) { + if (!checkResolvedMemoryObjects(state, address, 0, mayBeResolvedMemoryObjects, + hasLazyInitialized, resolvedMemoryObjects, + resolveConditions, unboundConditions, + checkOutOfBounds, mayBeOutOfBound)) { return false; } @@ -42,7 +41,8 @@ bool ComposeHelper::collectMemoryObjects( return true; } -bool ComposeHelper::tryResolveAddress(ExecutionState &state, ref address, +bool ComposeHelper::tryResolveAddress(ExecutionState &state, + ref address, std::pair, ref> &result) { ref guard; std::vector> resolveConditions; @@ -50,9 +50,8 @@ bool ComposeHelper::tryResolveAddress(ExecutionState &state, ref ad ObjectResolutionList resolvedMemoryObjects; KInstruction *target = nullptr; - if (!collectMemoryObjects(state, address, target, guard, - resolveConditions, unboundConditions, - resolvedMemoryObjects)) { + if (!collectMemoryObjects(state, address, target, guard, resolveConditions, + unboundConditions, resolvedMemoryObjects)) { return false; } @@ -60,7 +59,7 @@ bool ComposeHelper::tryResolveAddress(ExecutionState &state, ref ad if (resolvedMemoryObjects.size() > 0) { state.assumptions.insert(guard); ref resultAddress = - resolvedMemoryObjects.at(resolveConditions.size() - 1)->getBaseExpr(); + resolvedMemoryObjects.at(resolveConditions.size() - 1)->getBaseExpr(); for (unsigned int i = 0; i < resolveConditions.size(); ++i) { unsigned int index = resolveConditions.size() - 1 - i; @@ -75,7 +74,8 @@ bool ComposeHelper::tryResolveAddress(ExecutionState &state, ref ad return true; } -bool ComposeHelper::tryResolveSize(ExecutionState &state, ref address, +bool ComposeHelper::tryResolveSize(ExecutionState &state, + ref address, std::pair, ref> &result) { ref guard; std::vector> resolveConditions; @@ -83,9 +83,8 @@ bool ComposeHelper::tryResolveSize(ExecutionState &state, ref addre ObjectResolutionList resolvedMemoryObjects; KInstruction *target = nullptr; - if (!collectMemoryObjects(state, address, target, guard, - resolveConditions, unboundConditions, - resolvedMemoryObjects)) { + if (!collectMemoryObjects(state, address, target, guard, resolveConditions, + unboundConditions, resolvedMemoryObjects)) { return false; } @@ -96,7 +95,7 @@ bool ComposeHelper::tryResolveSize(ExecutionState &state, ref addre resolvedMemoryObjects.at(resolveConditions.size() - 1)->getSizeExpr(); for (unsigned int i = 0; i < resolveConditions.size(); ++i) { unsigned int index = resolveConditions.size() - 1 - i; - ref mo =resolvedMemoryObjects.at(index); + ref mo = resolvedMemoryObjects.at(index); resultSize = SelectExpr::create(resolveConditions[index], mo->getSizeExpr(), resultSize); } @@ -119,9 +118,8 @@ bool ComposeHelper::tryResolveContent( ObjectResolutionList mayBeResolvedMemoryObjects; KInstruction *target = nullptr; - if (!resolveMemoryObjects(state, base, target, 0, - mayBeResolvedMemoryObjects, mayBeOutOfBound, - hasLazyInitialized, incomplete)) { + if (!resolveMemoryObjects(state, base, target, 0, mayBeResolvedMemoryObjects, + mayBeOutOfBound, hasLazyInitialized, incomplete)) { return false; } @@ -302,8 +300,9 @@ ref ComposeVisitor::processRead(const Array *root, } case SymbolicSource::Kind::LazyInitializationAddress: { auto pointer = - visit(cast(root->source)->pointer); - ref address = cast(PointerExpr::create(pointer)); + visit(cast(root->source)->pointer); + ref address = + cast(PointerExpr::create(pointer)); auto guardedAddress = helper.fillLazyInitializationAddress(state, address); safetyConstraints.insert(guardedAddress.first); @@ -312,8 +311,9 @@ ref ComposeVisitor::processRead(const Array *root, } case SymbolicSource::Kind::LazyInitializationSize: { auto pointer = - visit(cast(root->source)->pointer); - ref address = cast(PointerExpr::create(pointer)); + visit(cast(root->source)->pointer); + ref address = + cast(PointerExpr::create(pointer)); auto guardedSize = helper.fillLazyInitializationSize(state, address); safetyConstraints.insert(guardedSize.first); composedArray = guardedSize.second; @@ -321,8 +321,9 @@ ref ComposeVisitor::processRead(const Array *root, } case SymbolicSource::Kind::LazyInitializationContent: { auto pointer = - visit(cast(root->source)->pointer); - ref address = cast(PointerExpr::create(pointer)); + visit(cast(root->source)->pointer); + ref address = + cast(PointerExpr::create(pointer)); // index is not used because there are conditions composed before // that act as the index check auto guardedContent = diff --git a/lib/Core/Composer.h b/lib/Core/Composer.h index 4643b355e6..907cc030d9 100644 --- a/lib/Core/Composer.h +++ b/lib/Core/Composer.h @@ -21,8 +21,7 @@ struct ComposeHelper { ComposeHelper(Executor *_executor) : executor(_executor) {} bool getResponse(const ExecutionState &state, ref expr, - ref &queryResult, - SolverQueryMetaData &) { + ref &queryResult, SolverQueryMetaData &) { executor->solver->setTimeout(executor->coreSolverTimeout); bool success = executor->solver->getResponse( state.constraints.withAssumtions(state.assumptions), expr, queryResult, @@ -43,8 +42,7 @@ struct ComposeHelper { bool evaluate(const ExecutionState &state, ref expr, ref &queryResult, - ref &negateQueryResult, - SolverQueryMetaData &) { + ref &negateQueryResult, SolverQueryMetaData &) { executor->solver->setTimeout(executor->coreSolverTimeout); bool success = executor->solver->evaluate( state.constraints.withAssumtions(state.assumptions), expr, queryResult, @@ -54,8 +52,7 @@ struct ComposeHelper { } bool resolveMemoryObjects(ExecutionState &state, ref address, - KInstruction *target, - unsigned bytes, + KInstruction *target, unsigned bytes, ObjectResolutionList &mayBeResolvedMemoryObjects, bool &mayBeOutOfBound, bool &mayLazyInitialize, bool &incomplete) { @@ -65,16 +62,16 @@ struct ComposeHelper { } bool checkResolvedMemoryObjects( - ExecutionState &state, ref address, - unsigned bytes, const ObjectResolutionList &mayBeResolvedMemoryObjects, + ExecutionState &state, ref address, unsigned bytes, + const ObjectResolutionList &mayBeResolvedMemoryObjects, bool hasLazyInitialized, ObjectResolutionList &resolvedMemoryObjects, std::vector> &resolveConditions, std::vector> &unboundConditions, ref &checkOutOfBounds, bool &mayBeOutOfBound) { return executor->checkResolvedMemoryObjects( - state, address, bytes, mayBeResolvedMemoryObjects, - hasLazyInitialized, resolvedMemoryObjects, resolveConditions, - unboundConditions, checkOutOfBounds, mayBeOutOfBound); + state, address, bytes, mayBeResolvedMemoryObjects, hasLazyInitialized, + resolvedMemoryObjects, resolveConditions, unboundConditions, + checkOutOfBounds, mayBeOutOfBound); } bool makeGuard(ExecutionState &state, @@ -160,7 +157,8 @@ struct ComposeHelper { } std::pair, ref> - fillLazyInitializationAddress(ExecutionState &state, ref pointer); + fillLazyInitializationAddress(ExecutionState &state, + ref pointer); std::pair, ref> fillLazyInitializationSize(ExecutionState &state, ref pointer); diff --git a/lib/Core/DistanceCalculator.cpp b/lib/Core/DistanceCalculator.cpp index 0ab5460234..f1d6d645b1 100644 --- a/lib/Core/DistanceCalculator.cpp +++ b/lib/Core/DistanceCalculator.cpp @@ -102,8 +102,7 @@ DistanceResult DistanceCalculator::computeDistance(KBlock *kb, TargetKind kind, break; case PreTarget: - res = tryGetPreTargetWeight(kb, weight, distanceToTargetFunction, - reversed); + res = tryGetPreTargetWeight(kb, weight, distanceToTargetFunction, reversed); isInsideFunction = false; break; @@ -227,7 +226,8 @@ DistanceCalculator::tryGetLocalWeight(KBlock *kb, weight_type &weight, WeightResult DistanceCalculator::tryGetPreTargetWeight( KBlock *kb, weight_type &weight, const std::unordered_map - &distanceToTargetFunction, bool reversed) const { + &distanceToTargetFunction, + bool reversed) const { KFunction *currentKF = kb->parent; std::vector localTargets; for (auto kCallBlock : currentKF->kCallBlocks) { @@ -265,7 +265,6 @@ WeightResult DistanceCalculator::tryGetTargetWeight(KBlock *kb, KBlock *target, bool reversed) const { std::vector localTargets = {target}; - WeightResult res = - tryGetLocalWeight(kb, weight, localTargets, reversed); + WeightResult res = tryGetLocalWeight(kb, weight, localTargets, reversed); return res; } diff --git a/lib/Core/DistanceCalculator.h b/lib/Core/DistanceCalculator.h index d0045efa03..8c01636fb0 100644 --- a/lib/Core/DistanceCalculator.h +++ b/lib/Core/DistanceCalculator.h @@ -125,7 +125,8 @@ class DistanceCalculator { WeightResult tryGetPreTargetWeight(KBlock *kb, weight_type &weight, const std::unordered_map - &distanceToTargetFunction,bool reversed) const; + &distanceToTargetFunction, + bool reversed) const; WeightResult tryGetTargetWeight(KBlock *kb, weight_type &weight, KBlock *target, bool reversed) const; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index db763b2e7d..94bab5c949 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -521,9 +521,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, : Interpreter(opts), interpreterHandler(ih), searcher(nullptr), externalDispatcher(new ExternalDispatcher(ctx)), summary(interpreterHandler), statsTracker(0), pathWriter(0), - symPathWriter(0), specialFunctionHandler(0), - timers{time::Span(TimerInterval)}, guidanceKind(opts.Guidance), - codeGraphInfo(new CodeGraphInfo()), + symPathWriter(0), + specialFunctionHandler(0), timers{time::Span(TimerInterval)}, + guidanceKind(opts.Guidance), codeGraphInfo(new CodeGraphInfo()), distanceCalculator(new DistanceCalculator(*codeGraphInfo)), targetCalculator(new TargetCalculator(*codeGraphInfo)), targetManager(new TargetManager(guidanceKind, *distanceCalculator, @@ -2594,7 +2594,7 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, // offsets of variadic arguments std::vector offsets(callingArgs, 0); - uint64_t argWidth; // width of current variadic argument + uint64_t argWidth; // width of current variadic argument const CallBase &cb = cast(*i); for (unsigned k = funcArgs; k < callingArgs; k++) { @@ -4856,7 +4856,7 @@ ref Executor::fillSymbolicSizeConstantAddress( ref arraySize, ref size) { unsigned stateNameVersion = state.arrayNames.count("const_arr") ? state.arrayNames.at("const_arr") - : 0; + : 0; unsigned newVersion = symbolicSizeConstantAddressSource->version + stateNameVersion; const Array *newArray = makeArray( @@ -4929,8 +4929,7 @@ Executor::compose(const ExecutionState &state, const PathConstraints &pob, return result; } - auto added = - composer.state.constraints.addConstraint(condition, index); + auto added = composer.state.constraints.addConstraint(condition, index); for (auto expr : added) { rebuildMap.insert({expr, constraint}); } @@ -6076,7 +6075,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, e->getWidth() == Context::get().getPointerWidth() && resultType->isPointerTy()) { ref symExternCallsCanReturnNullExpr = - makeMockValue(state, "symExternCallsCanReturnNull", Expr::Bool); + makeMockValue(state, "symExternCallsCanReturnNull", Expr::Bool); e = SelectExpr::create( symExternCallsCanReturnNullExpr, PointerExpr::create(Expr::createPointer(0), Expr::createPointer(0)), @@ -6209,7 +6208,7 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, if (checkOutOfMemory && !isLocal) { ref symCheckOutOfMemoryExpr = - makeMockValue(state, "symCheckOutOfMemory", Expr::Bool); + makeMockValue(state, "symCheckOutOfMemory", Expr::Bool); address = SelectExpr::create(symCheckOutOfMemoryExpr, Expr::createPointer(0), address); } @@ -6628,7 +6627,8 @@ bool Executor::resolveMemoryObjects( size = kmodule->targetData->getTypeStoreSize(state.gepExprBases[base]); } - // base = Simplificator::simplifyExpr(state.constraints.cs(), base).simplified; + // base = Simplificator::simplifyExpr(state.constraints.cs(), + // base).simplified; ref basePointer = PointerExpr::create(base, base); auto mso = MemorySubobject(address, bytes); @@ -6960,7 +6960,8 @@ void Executor::executeMemoryOperation( if (SimplifySymIndices) { // if (!isa(base)) { // base = - // Simplificator::simplifyExpr(estate.constraints.cs(), base).simplified; + // Simplificator::simplifyExpr(estate.constraints.cs(), + // base).simplified; // } if (isWrite && !isa(value)) value = Simplificator::simplifyExpr(estate.constraints.cs(), value) @@ -7407,7 +7408,8 @@ void Executor::lazyInitializeLocalObject(ExecutionState &state, StackFrame &sf, } ref conditionExpr = Expr::createTrue(); ref pointer = PointerExpr::create(address); - ref basePointer = PointerExpr::create(pointer->getBase(), pointer->getBase()); + ref basePointer = + PointerExpr::create(pointer->getBase(), pointer->getBase()); ref id = lazyInitializeObject(state, pointer, target, elementSize, size, true, conditionExpr, UseSymbolicSizeLazyInit); @@ -7668,8 +7670,7 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv, continue; } auto mo = globalObjects[&v]; - auto array = - makeArray(mo->sizeExpr, SourceBuilder::global(v)); + auto array = makeArray(mo->sizeExpr, SourceBuilder::global(v)); bindObjectInState(*emptyState, mo, false, array); } objectManager->setEmptyState(emptyState); @@ -7696,8 +7697,8 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv, trace.push_back({kEntryFunction->entryKBlock}); auto kCallBlock = kfIt->second->entryKBlock; trace.push_back({kCallBlock}); - data = targetedExecutionManager->prepareTargets(kEntryFunction, - {trace}); + data = + targetedExecutionManager->prepareTargets(kEntryFunction, {trace}); } } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index a044f0a784..48868e0579 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -112,7 +112,7 @@ template class ref; /// during an instruction step. Should contain addedStates, /// removedStates, and haltExecution, among others. - typedef std::vector> ObjectResolutionList; +typedef std::vector> ObjectResolutionList; class Executor : public Interpreter { friend struct ComposeHelper; @@ -262,7 +262,6 @@ class Executor : public Interpreter { std::unordered_set successTransitionsTo; std::unordered_map failedTransitionsTo; - /// Typeids used during exception handling std::vector> eh_typeids; @@ -486,8 +485,8 @@ class Executor : public Interpreter { // Used for testing. ref replaceReadWithSymbolic(ExecutionState &state, ref e); - ref makeMockValue(ExecutionState &state, - const std::string &name, Expr::Width width); + ref makeMockValue(ExecutionState &state, const std::string &name, + Expr::Width width); const Cell &eval(const KInstruction *ki, unsigned index, ExecutionState &state, StackFrame &sf, @@ -793,7 +792,6 @@ class Executor : public Interpreter { void closeProofObligation(ProofObligation *pob); - // void executeAction(ref action); // void goForward(ref action); diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index 22119645ac..e9bff7df53 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -293,7 +293,6 @@ class ObjectState { ObjectState(const MemoryObject *mo, const Array *array); ObjectState(const MemoryObject *mo); - /// Create a new object state for the given memory object with symbolic /// contents. ObjectState(const Array *array); diff --git a/lib/Core/ObjectManager.cpp b/lib/Core/ObjectManager.cpp index fee66b35c9..d7031ea460 100644 --- a/lib/Core/ObjectManager.cpp +++ b/lib/Core/ObjectManager.cpp @@ -72,8 +72,8 @@ void ObjectManager::removeState(ExecutionState *state) { assert(itr == removedStates.end()); if (state->isolated) { - llvm::errs() << "Removing isolated: " << - state->constraints.path().toString() << "\n"; + llvm::errs() << "Removing isolated: " + << state->constraints.path().toString() << "\n"; } if (!statesUpdated) { diff --git a/lib/Core/ObjectManager.h b/lib/Core/ObjectManager.h index 1c337dc64f..e50d860f9d 100644 --- a/lib/Core/ObjectManager.h +++ b/lib/Core/ObjectManager.h @@ -148,7 +148,7 @@ class ObjectManager { std::map propagationCount; std::unordered_set reachedOriginal; // TODO remove - std::unordered_set removeSet; // TODO remove + std::unordered_set removeSet; // TODO remove // These are used to buffer execution results and pass the updates to // subscribers diff --git a/lib/Core/ProofObligation.cpp b/lib/Core/ProofObligation.cpp index d6df072117..5b63b28541 100644 --- a/lib/Core/ProofObligation.cpp +++ b/lib/Core/ProofObligation.cpp @@ -1,6 +1,5 @@ -#include #include "ProofObligation.h" - +#include namespace klee { bool ProofObligationIDCompare::operator()(const ProofObligation *a, diff --git a/lib/Core/TargetedExecutionManager.h b/lib/Core/TargetedExecutionManager.h index 710d8dd852..74228cb33a 100644 --- a/lib/Core/TargetedExecutionManager.h +++ b/lib/Core/TargetedExecutionManager.h @@ -117,7 +117,6 @@ class TargetedExecutionManager : public Subscriber { StatesSet localStates; public: - struct Data { ref forwardWhitelist; std::map> backwardWhitelists; diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 37a08e8377..cd053016fc 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -401,7 +401,6 @@ PathConstraints::withAssumtions(const ExprHashSet &assumptions) const { return tmpConstraints; } - const PathConstraints::ordered_constraints_ty & PathConstraints::orderedCS() const { return orderedConstraints; diff --git a/lib/Expr/Lemma.cpp b/lib/Expr/Lemma.cpp index c7608263a0..eb312795de 100644 --- a/lib/Expr/Lemma.cpp +++ b/lib/Expr/Lemma.cpp @@ -87,8 +87,8 @@ void Summary::readFromFile(KModule *km) { } std::unique_ptr &MB = *MBResult; std::unique_ptr Builder(createDefaultExprBuilder()); - expr::Parser *P = expr::Parser::Create("LemmaParser", MB.get(), Builder.get(), - km, true); + expr::Parser *P = + expr::Parser::Create("LemmaParser", MB.get(), Builder.get(), km, true); while (auto parsed = P->ParseTopLevelDecl()) { if (auto lemmaDecl = dyn_cast(parsed)) { ref l(new Lemma(lemmaDecl->path, lemmaDecl->constraints));