From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: How to put main procedure in SPARK_Mode?
Date: Tue, 21 May 2019 15:14:42 +0100
Organization: A noiseless patient Spider
Message-ID: <lyef4rzygd.fsf@pushface.org>
References: <9ad71ff8-71c6-436c-9a56-f9637565d99a@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="2a57a09140910fc57e1b44da630f3017";
	logging-data="29971"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19pDJ4SQeLM4tdfEcvdxX3NNsgzRSGRw5s="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (darwin)
Cancel-Lock: sha1:WBUvjtTOuS0zkgGQQxtgjf3egm8=
	sha1:d/o6cpg+1zk2fkWRg0lNjKKQ+xI=
Xref: reader01.eternal-september.org comp.lang.ada:56355
Date: 2019-05-21T15:14:42+01:00
List-Id: <comp.lang.ada>

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.