How do I resolve the error "Implied return after this statement not allowed (No_Return)" when compiling my Ada project with Polyspace R2025b?

When I compile my Ada project with Polyspace R2025b, I get the following error:

Implied return after this statement not allowed (No_Return) 

The "No_Return" procedure in question calls another procedure that is implemented externally in C.  I do not receive this compilation error when I compile using the GNAT compiler.

Why am I getting this compilation error? 

Answer 1

[MathWorks Support Team]

A "No_Return" procedure cannot exit via a normal return statement or simply by reaching the end of its body. Instead, it must terminate execution through another mechanism, such as raising an exception, calling another "No_Return" procedure, or performing a non-local transfer of control (i.e. abort, task termination).

For a procedure implemented externally, Polyspace will stub the procedure without detailed knowledge of its behaviour. As a result, Polyspace does not know that the procedure never returns. So, the error you are receiving is expected.

To resolve this error, you can explicitly declare the externally-defined procedure as a no-return procedure in your Ada specification by adding:

pragma No_Return (PROCEDURE_NAME);