@@ -4670,25 +4670,6 @@ void Executor::run(ExecutionState *initialState) {
4670
4670
haltExecution = HaltExecution::NotHalt;
4671
4671
}
4672
4672
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
-
4692
4673
void Executor::initializeTypeManager () {
4693
4674
if (UseAdvancedTypeSystem) {
4694
4675
typeSystemManager = new CXXTypeManager (kmodule.get ());
@@ -4794,55 +4775,6 @@ void Executor::goForward(ref<ForwardAction> action) {
4794
4775
}
4795
4776
}
4796
4777
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
-
4846
4778
std::string Executor::getAddressInfo (ExecutionState &state,
4847
4779
ref<PointerExpr> address, unsigned size,
4848
4780
const MemoryObject *mo) const {
0 commit comments