diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp index d35b740da76fa61bd6f2691d95f6e9a371019233..4e4b237da5022a9a2f00b4ad373603f04a3bd4df 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)) {