From de194b62be01e5e51f33d7e0ad6e317d40aadb98 Mon Sep 17 00:00:00 2001
From: Clark Coleman <clc@zephyr-software.com>
Date: Sun, 20 Sep 2020 11:36:43 -0400
Subject: [PATCH] SPARK: Handle INDIR_CALL at end of block.
---
src/base/SMPFunction.cpp | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index d35b740d..4e4b237d 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -20537,6 +20537,7 @@ void SMPFunction::EmitFuncSPARKAda(void) {
}
if (!TranslationComplete) {
SMP_msg("ERROR: Incomplete SPARK Ada translation for %s\n", this->GetFuncName());
+ this->DumpDotCFG();
if (VerboseOutput)
this->Dump();
}
@@ -22151,7 +22152,7 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrBlockNum, int FollowBlockNum, FIL
// Handle possible tail call case
;
}
- else if (FlowType == CALL) {
+ else if ((FlowType == CALL) || (FlowType == INDIR_CALL)) {
LastInst->EmitSPARKAda(SPARKBodyFile);
if (LastCFType == FALL_THROUGH) {
// if ((FALL_THROUGH == LastCFType) && (ResumeBlockNum < 0)) {
--
GitLab