From fe95d5b7282bb1bf9f0a6882ad661e0337038590 Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Mon, 21 Sep 2020 18:04:57 -0400
Subject: [PATCH] SPARK: Translate code after conditional in guarded loop that
is being skipped.
---
src/base/SMPFunction.cpp | 14 ++++++++++++++
1 file changed, 14 insertions(+)
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 4e4b237d..09c4445e 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -16635,6 +16635,11 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
if (!this->IsBlockInLoop(FollowBlockNum, (size_t)LoopIndex)) {
this->UpdateLoopFollowBlockNum(HeaderBlockNum, FollowBlockNum);
}
+ else {
+ SMP_msg("WARNING: SPARK: LOOP_CONTINUE case detected in block %d FollowBlock %d of %s\n",
+ CurrBlock->GetNumber(), FollowBlockNum, this->GetFuncName());
+ this->DumpDotCFG();
+ }
}
else {
// Fall-through to next function, probably IDA Pro problem in func ID.
@@ -22547,6 +22552,15 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
this->SPARKLoopWorkList.push_back(WorkListItem);
this->CleanUpSPARKLoopWorkList();
+ // See if we have a loop follow block number that is inside this conditional
+ // and recurse into it if so.
+ int LoopFollowBlockNum = this->LoopFollowNodes[LoopNum];
+ assert(0 < LoopFollowBlockNum);
+ SMPBasicBlock *LoopFollowBlock = this->GetBlockByNum((size_t) LoopFollowBlockNum);
+ if (!LoopFollowBlock->IsProcessed() && this->DoesBlockDominateBlock(HeaderBlockNum, LoopFollowBlockNum)) {
+ this->EmitSPARKAdaForBlock(LoopFollowBlockNum, FollowBlockNum, SPARKBodyFile, false, false);
+ }
+
--STARS_SPARK_IndentCount;
PrintSPARKIndentTabs(SPARKBodyFile);
SMP_fprintf(SPARKBodyFile, "end if;\n");
--
GitLab