From ca0cb29f9a3e3f7013e536233e1d2359613e8c81 Mon Sep 17 00:00:00 2001 From: Clark Coleman <clc@zephyr-software.com> Date: Wed, 8 Jan 2025 17:12:26 +0000 Subject: [PATCH] Solve infinite loop in monerod binary SPARK translation. --- src/base/SMPFunctionSPARK.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/base/SMPFunctionSPARK.cpp b/src/base/SMPFunctionSPARK.cpp index 23c160c5..9a7b8d1a 100644 --- a/src/base/SMPFunctionSPARK.cpp +++ b/src/base/SMPFunctionSPARK.cpp @@ -2098,6 +2098,7 @@ int SMPFunction::FindConditionalFollowNode4(const int HeadBlockNum, bool &IfThen OddIfThenCase = false; IfThenElseCase = false; FollowBlockNum = SMP_BLOCKNUM_UNINIT; + this->SPARKCloningWorkList.clear(); // Reverse earlier decision to fix by cloning. } } } @@ -2200,7 +2201,6 @@ bool SMPFunction::SolveConditionalDomFrontierProblemViaCloning(const int HeadBlo SMP_msg("INFO: SPARK: CLONING 4: Cloning from %d to %d would solve DomFrontier non-convergence for HeadBlock %d ", NFTDomFrontierBlockNum, FTDomFrontierBlockNum, HeadBlockNum); this->DumpFuncNameAndAddr(); this->DumpDotCFG(); - this->ResetTCFGVisitedBlocks(); FollowBlockNum = FTDomFrontierBlockNum; CloningStructuresConditional = true; this->ResetTCFGVisitedBlocks(); -- GitLab