Re: How to put main procedure in SPARK_Mode?

[Shark8 <onewingedshark@gmail.com>]

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.