<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<div class="moz-cite-prefix">On 02/07/2020 16:41, Olwen Morgan
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:76819eb4-8711-f2a1-4c50-4be0eafcab62@phaedsys.com">So,
the next question is, do the analysis tools take this into account
when seeking to prove loop termination?</blockquote>
<p><font size="+1">There is a separate tool (called, unsurprisingly,
"GNATStack") that does static worst-case stack usage analysis.</font></p>
<p><font size="+1">For any hard real-time system running on
bare-metal or a small RTOS, I would never allow recursion
anyway, so analysis of stack usage is reasonably easy. See
<a class="moz-txt-link-freetext" href="http://docs.adacore.com/live/wave/gnatstack/html/gnatstack_ug/">http://docs.adacore.com/live/wave/gnatstack/html/gnatstack_ug/</a>
for the details of what it can do.<br>
</font></p>
<p><font size="+1">As for a compiler maliciously turning iteration
into recursion... I have never seen this in 30-odd years of
compiling and running SPARK programs, so it's not something that
I'm ever gonna lose sleep over.</font></p>
<p><font size="+1"> - Rod</font></p>
<p><font size="+1"><br>
</font></p>
</body>
</html>