From: Simon Wright <simon@pushface.org>
Subject: Re: How to put main procedure in SPARK_Mode?
Date: Tue, 21 May 2019 17:56:33 +0100
Date: 2019-05-21T17:56:33+01:00 [thread overview]
Message-ID: <lya7ffzqym.fsf@pushface.org> (raw)
In-Reply-To: ce3cb794-da56-4624-ae44-1d299b392a67@googlegroups.com
mockturtle <framefritti@gmail.com> writes:
> There is maybe a difference... I do not know if it is important, but
> in my setup the main procedure is a child of a "big root package"
> (this is a setup that I usually find convenient). Could this be the
> difference? I'll try later.
I think you need a spec for the child main procedure, also 'with SPARK_Mode'.
prev parent reply other threads:[~2019-05-21 16:56 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-05-21 12:44 How to put main procedure in SPARK_Mode? mockturtle
2019-05-21 14:14 ` Simon Wright
2019-05-21 14:22 ` mockturtle
2019-05-21 16:38 ` Shark8
2019-05-21 16:56 ` Simon Wright [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox