SPARK Overiew: downloaded examples do not contain SPARK_Mode in main.adc

[mgrojo]

When you download the examples and use the same arguments to gnatprove as in the web platform, you don't get the same results.

The reader doesn't understand that until reaching this paragraph:

If you don't explicitly specify otherwise, SPARK_Mode is Off, meaning you can use the complete set of Ada features in that code and that it should not be analyzed by GNATprove. You can change this default either selectively (on some units or subprograms or packages inside units) or globally (using a configuration pragma, which is what we're doing in this tutorial).

The included main.adc is not the same as the one used in the web. Only when you add

pragma SPARK_Mode (On);

the output of gnatprove is then the same.

The download example should already have that pragma, so the user gets the same output without having to figure out.

[gusthoff]

Hello Manuel,

I'm not sure I understand where you're seeing this issue. Could you please point me to a specific code example from that zip file that gives you unexpected results?

I've just looked into one of the code examples from the first chapter: https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html#example-1

In the zip file, this example is currently located here: projects/Courses/Intro_To_Spark/Overview/Example_01/2b15e13e850435fb93406054d70b51c6/

This folder contains a file called main_spark.adc with the following restrictions:

pragma Profile(GNAT_Extended_Ravenscar);
pragma Partition_Elaboration_Policy(Sequential);
pragma SPARK_Mode (On);
pragma Warnings (Off, "no Global contract available");
pragma Warnings (Off, "subprogram * has no effect");
pragma Warnings (Off, "file name does not match");

Also, If I run gnatprove on this example, I get the same output as on the website:

Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

stack_package.ads:9:13: error: function with "in out" parameter is not allowed in SPARK
    9 |   function Pop (S : in out Stack) return Element;
      |            ^~~
  violation of aspect SPARK_Mode at line 2
    2 |  with SPARK_Mode => On
      |       ^ here
gnatprove: error during flow analysis and proof

So, again, it'd be great if could point me to a code example that doesn't work for you. Thanks!

[mgrojo]

Strange, I reproduce the problem with that same example.

I use the Download button from:

My downloaded zip file doesn't contain any main_spark.adc, only main.adc with this content:

pragma Restrictions (No_Specification_of_Aspect => Import);
pragma Restrictions (No_Use_Of_Pragma => Import);
pragma Restrictions (No_Use_Of_Pragma => Interface);
pragma Restrictions (No_Use_Of_Pragma => Linker_Options);
pragma Restrictions (No_Dependence => System.Machine_Code);
pragma Restrictions (No_Dependence => Machine_Code);

This is the md5sum of the downloaded file: c6b125027f2da4d82cc85877508ee616 Courses.Intro_To_Spark.Overview.Example_01.zip

Content:

Archive:  Courses.Intro_To_Spark.Overview.Example_01.zip
  Length      Date    Time    Name
---------  ---------- -----   ----
      344  2024-04-13 10:21   stack_package.ads
      334  2024-04-13 10:21   main.adc
      408  2024-04-13 10:21   main.gpr
---------                     -------
     1086                     3 files

Browser: Mozilla Firefox snap for Ubuntu 123.0.1 (64-bit) I also tested with "Chromium Versión 123.0.6312.105 (Build oficial) snap (64 bits)" and the result was the same.

URL according to Firefox Downloads window: blob:https://learn.adacore.com/9bc647df-f0f6-4219-8f57-f1714a5d1209

$ gnatprove -P main.gpr  stack_package.ads 
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

stack_package.ads:9:13: error: function with "in out" parameter is not allowed in SPARK
    9 |   function Pop (S : in out Stack) return Element;
      |            ^~~
  violation of aspect SPARK_Mode at line 2
    2 |  with SPARK_Mode => On
      |       ^ here
gnatprove: error during flow analysis and proof

But if it didn't contain the SPARK_Mode aspect, as in previous examples, the output would differ.

[gusthoff]

Ok, now I get what you mean. And yes, this is indeed an issue that has to be fixed. Thanks for reporting!

(I was confused because I was testing the zip file that contains all source-code example, while you were referring to the zip file downloaded via the "download" button of a specific code example.)

In the meantime, I recommend downloading the zip file that contains all source-code examples from learn: https://learn.adacore.com/zip/learning-ada_code.zip

The code examples from that zip file have the same output as you see on the website.

[gusthoff]

Fixed with #1036