From: mockturtle <framefritti@gmail.com>
Subject: Re: How to put main procedure in SPARK_Mode?
Date: Tue, 21 May 2019 07:22:35 -0700 (PDT)
Date: 2019-05-21T07:22:35-07:00 [thread overview]
Message-ID: <ce3cb794-da56-4624-ae44-1d299b392a67@googlegroups.com> (raw)
In-Reply-To: <lyef4rzygd.fsf@pushface.org>
On Tuesday, May 21, 2019 at 4:14:44 PM UTC+2, Simon Wright wrote:
> mockturtle <framefritti@gmail.com> writes:
>
> > I am fooling around with SPARK (I always wanted to learn to use it)
> > and I want to put the "main" procedure (that is in a body file of its
> > own) in SPARK_Mode, but with no success so far.
> >
> > I tried many things including (but not limited to :-))
> >
> > * Using Pragma SPARK_Mode (with and without "On") at the beginning of
> > the file
> >
> > * Using Pragma SPARK_MODE after the "is"
> >
> > * Using
> > procedure Main with SPARK_Mode => is ....
> >
> > and other variations that I do not remember.
> >
> > The only way I was able to put the procedure in SPARK mode is by
> > putting it into a package, but in this way it cannot be the "main"
> > (right?). I solved the problem by having a microscopic main procedure
> > whose only action is to call the true main in the package, but it
> > seems to me less than ideal...
> >
> > Any suggestions?
>
> I just tried
>
> project Spark_Main is
> for Source_Files use ("spark_main.adb");
> end Spark_Main;
>
> and
>
> procedure Spark_Main with SPARK_Mode is
> begin
> null;
> end Spark_Main;
>
> and it worked OK.
I know it sounds crazy, but I am pretty sure I tried this too...
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.
next prev parent reply other threads:[~2019-05-21 14:22 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 [this message]
2019-05-21 16:38 ` Shark8
2019-05-21 16:56 ` Simon Wright
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox