* How to put main procedure in SPARK_Mode?
@ 2019-05-21 12:44 mockturtle
2019-05-21 14:14 ` Simon Wright
0 siblings, 1 reply; 5+ messages in thread
From: mockturtle @ 2019-05-21 12:44 UTC (permalink / raw)
Dear.all,
this is really a silly questions, but I am stumped...
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?
Thank you in advance
Riccardo
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: How to put main procedure in SPARK_Mode?
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
0 siblings, 1 reply; 5+ messages in thread
From: Simon Wright @ 2019-05-21 14:14 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: How to put main procedure in SPARK_Mode?
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
0 siblings, 2 replies; 5+ messages in thread
From: mockturtle @ 2019-05-21 14:22 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: How to put main procedure in SPARK_Mode?
2019-05-21 14:22 ` mockturtle
@ 2019-05-21 16:38 ` Shark8
2019-05-21 16:56 ` Simon Wright
1 sibling, 0 replies; 5+ messages in thread
From: Shark8 @ 2019-05-21 16:38 UTC (permalink / raw)
On Tuesday, May 21, 2019 at 8:22:37 AM UTC-6, mockturtle wrote:
> On Tuesday, May 21, 2019 at 4:14:44 PM UTC+2, Simon Wright wrote:
> > mockturtle 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.
Hm, you could try the following:
-- whatever.child.pkg.main_program.ads
Procedure whatever.child.pkg.main_program
with SPARK_Mode => On, Depends => Null;
-- Main.ads
Procedure Main
with SPARK_Mode => On;
-- Main.adb
With whatever.child.pkg.main_program;
Procedure Main
renames whatever.child.pkg.main_program;
I *think* this will give you a good SPARK-proven main-program; plus it's good if you have several alternate "main" programs that you want to try out.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: How to put main procedure in SPARK_Mode?
2019-05-21 14:22 ` mockturtle
2019-05-21 16:38 ` Shark8
@ 2019-05-21 16:56 ` Simon Wright
1 sibling, 0 replies; 5+ messages in thread
From: Simon Wright @ 2019-05-21 16:56 UTC (permalink / raw)
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'.
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2019-05-21 16:56 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
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 is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox