@@ -4670,25 +4670,6 @@ void Executor::run(ExecutionState *initialState) {
46704670 haltExecution = HaltExecution::NotHalt;
46714671}
46724672
4673- void Executor::runWithTarget (ExecutionState &state, KFunction *kf,
4674- KBlock *target) {
4675- if (pathWriter)
4676- state.pathOS = pathWriter->open ();
4677- if (symPathWriter)
4678- state.symPathOS = symPathWriter->open ();
4679-
4680- if (statsTracker)
4681- statsTracker->framePushed (state, 0 );
4682-
4683- processForest = std::make_unique<PForest>();
4684- processForest->addRoot (&state);
4685- targetedRun (state, target);
4686- processForest = nullptr ;
4687-
4688- if (statsTracker)
4689- statsTracker->done ();
4690- }
4691-
46924673void Executor::initializeTypeManager () {
46934674 if (UseAdvancedTypeSystem) {
46944675 typeSystemManager = new CXXTypeManager (kmodule.get ());
@@ -4794,55 +4775,6 @@ void Executor::goForward(ref<ForwardAction> action) {
47944775 }
47954776}
47964777
4797- void Executor::targetedRun (ExecutionState &initialState, KBlock *target,
4798- ExecutionState **resultState) {
4799- // Delay init till now so that ticks don't accrue during optimization and
4800- // such.
4801- if (guidanceKind != GuidanceKind::ErrorGuidance)
4802- timers.reset ();
4803-
4804- // TODO: Inconsistent init, sort things out later
4805- objectManager->addProcessForest (processForest.get ());
4806- objectManager->addInitialState (&initialState);
4807-
4808- TargetedSearcher *targetedSearcher = new TargetedSearcher (
4809- ReachBlockTarget::create (target), *distanceCalculator);
4810-
4811- searcher = std::make_unique<ForwardOnlySearcher>(targetedSearcher);
4812-
4813- // main interpreter loop
4814- KInstruction *terminator =
4815- target != nullptr ? target->getFirstInstruction () : nullptr ;
4816- while (!searcher->empty () && !haltExecution) {
4817- auto action = searcher->selectAction ();
4818- auto forward = cast<ForwardAction>(action);
4819-
4820- KInstruction *ki = forward->state ->pc ;
4821-
4822- if (ki == terminator) {
4823- *resultState = forward->state ->copy ();
4824- terminateStateEarly (*forward->state , " " ,
4825- StateTerminationType::SilentExit);
4826- objectManager->updateSubscribers ();
4827- haltExecution = HaltExecution::ReachedTarget;
4828- break ;
4829- }
4830-
4831- executeAction (action);
4832- objectManager->updateSubscribers ();
4833-
4834- if (!checkMemoryUsage ()) {
4835- objectManager->updateSubscribers ();
4836- }
4837- }
4838-
4839- searcher = nullptr ;
4840-
4841- doDumpStates ();
4842- if (*resultState)
4843- haltExecution = HaltExecution::NotHalt;
4844- }
4845-
48464778std::string Executor::getAddressInfo (ExecutionState &state,
48474779 ref<PointerExpr> address, unsigned size,
48484780 const MemoryObject *mo) const {
0 commit comments