From 04ba0e8384ed979de6b7ffcde64994d444631260 Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Tue, 6 Oct 2020 16:32:51 -0400
Subject: [PATCH] SPARK: Clone StaysInLoop code to corner case
CurrBlock->HasLoopHeadWithInvertedExitAsSuccessor().
---
src/base/SMPFunction.cpp | 13 ++++++++++++-
1 file changed, 12 insertions(+), 1 deletion(-)
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 09c74e9c..29a277a9 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -22452,7 +22452,18 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
}
}
else {
- CurrBlock->EmitSPARKAdaForAllInsts(SPARKBodyFile);
+ bool StaysInLoop = this->IsNonExitingLoopBackBranch(LastInstAddr);
+ if (!StaysInLoop) { // just loop-back and return to EmitSPARKAdaForLoop().
+ CurrBlock->EmitSPARKAdaForAllInsts(SPARKBodyFile);
+ }
+ else {
+ // We need to emit the fall through insts, then translate COND_BRANCH to loop header
+ // into if (inverted condition) then ... for the rest of the loop body.
+ CurrBlock->EmitSPARKAdaForFallThroughInsts(SPARKBodyFile);
+ // EmitSPARKAdaForConditional() will emit the if (inverted condition) then ... and
+ // will continue through the rest of the if-then body.
+ this->EmitSPARKAdaForConditional(CurrBlockNum, FollowBlockNum, SPARKBodyFile);
+ }
}
}
else {
--
GitLab