New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
SPARK Overiew: downloaded examples do not contain SPARK_Mode in main.adc #1020
Comments
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
Also, If I run
So, again, it'd be great if could point me to a code example that doesn't work for you. Thanks! |
Strange, I reproduce the problem with that same example. I use the Download button from: My downloaded zip file doesn't contain any
This is the md5sum of the downloaded file: Content:
Browser: Mozilla Firefox snap for Ubuntu 123.0.1 (64-bit) URL according to Firefox Downloads window: $ 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. |
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. |
Fixed with #1036 |
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:
The included
main.adc
is not the same as the one used in the web. Only when you addpragma 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.
The text was updated successfully, but these errors were encountered: