Example Code for Testing Installation of Spark Ada
- In the following we use the Linux terminology directory for what is called in Windows
- This is an adaption of the code from the lecture sect2g/example2g-19 for testing
whether the installation works and getting started.
- Download the files from the example into a new directory.
- Easiest done by downloading the zip archive
- Choose open with and then Ark-Linux application.
- Ark is an application (similar to win-zip) for extracting zip files.
- Use option Extract to
- Select a directory
- The system displays the whole file system which includes in the Linux lab
- Locate your user name (usually your student number)
- Choose the option below to create a directory inside for extracting it to
- extract it to it
- You can as well manually move the files in
the folder example code for testing installation
to a directory you have created.
- Now open the file browser (dolphin) which is on the start menu.
- Navigate to the directory where you have put the files
- If you click on the file main.gpr (NOT main.adb or main.ads) gps should start.
This might take a while initially because it initialises some data when used the first time.
- It should approximately like the following
- Now navigate (in dolphin) to the subdirectory gnatprove
- As of 19 Oct 2017 the why3 system is not installed. So you can skip the following for the moment
- Click on the file main.mlw
- wh3 should start. It should approximately look like the following
- Close why3, we won't need it at the moment. We tried it out to test the installation.
- We can try out gps. If you closed it reopen it again.
- Please note: always open gps by clicking on the main.gpr file.
- Don't add files to gps using drag and drop
- Spark ada will only check files which are covered by the main.gpr file.
- If you drag in other files they might not be checked even so they occur on your
- If you want to open an ads or adb file
- make sure there is a directory containing one project only.
- Add if necessary a
- Then possibly close any other gps open and open the main.gpr file.
- Go to the right pane. You need to click on something with a dot only as name
- When it expands you should see your files.
- If you can't see the file common reasons are
- Your directory or one of the directories in your path contains a blank.
Rename them by replacing blanks e.g. by underscore.
- Your filename contains upper case characters. SPARK Ada allows only files in lower
- To look at file go the left pane. There is a folder with a dot.
If you click on it it should expand and show the files in this project.
- The most interesting file here is the main.adb file. Double click on it to open it.
- To compile it go to Build -> Project -> Build < current file >
(Note that the main.adb file needs to be the active file shown in the main code area)
- Compilation will only work for adb files which have no package, and only one procedure having
no parameters (usually called main.adb)
- To execute it choose Build -> Run -> Custom
- Enter as custom command -hold -e main ./main
- (main is the name of the file (main.adb) you are executing.
This command will be remembered. If you are compiling a file with a different name, you
need to replace main by the name of the file)
- The program opens in a terminal.
- It is a very simple program, asking you for a number repeating it and for a string repeating it.
- To compile all files (good for testing) use Build -> Project -> Build All
- This will compile the code but not create executables. The files can be linked
- We will not link files in this module, but use this option to test code is correct.
- To check your code for data flow analysis using spark ada use SPARK 2014 -> Examine All
- SPARK will give you an older version of SPARK Ada, we are using SPARK 2014.
- To prove your code for generating verification conditions use
SPARK -> Examine All
- I recommend to choose as proof stategy Progressively split
- To close gps use first File-> Save and then File-> Exit.
- If it says there are tasks still running it could be that you have a terminal still open
generated by executing some code. Close those terminals (called xterm).
- An older version of the test code can be found here