Re: Ada features supported by SPARK 2014

[Daniel King <daniel.dmk@googlemail.com>]

On Tuesday, 6 December 2016 05:17:56 UTC-4, Simon Wright  wrote:
> Daniel King <danie...@googlemail.com> writes:
> 
> > In addition, for tasking features, SPARK is limited to the "Ravenscar
> > profile", which is basically a set of restrictions on Ada's tasking
> > features, to permit static analysis for formal verification.
> 
> I found that - as soon as there's anything involving time - I couldn't
> work out how to specify flow (when I "fixed" one problem, another would
> pop up somewhere else; if I "fixed" that, the first would pop up
> again). So I left it up to the tool to infer flow for itself according
> to whatever arcane rules it wanted to (not really a satisfactory state
> of affairs for something that's supposed to increase my confidence in
> the code).

Do you mean using "delay until"?

In such cases I've found that I've needed the following annotations:

   with Global => (Input => Ada.Real_Time.Clock_Time),
   Depends => (null => Ada.Real_Time.Clock_Time);