Example Code for Testing Installation of Spark Ada
On Linux Machines in the Linux Lab, please follow
Testing Installation of SPARK Ada on Linux Machines in the Linux Lab
- In the following we use the Linux terminology
"directory" for what is called in Windows
- The example code for testing SPARK Ada is an adaption of the code from the lecture sect6/example6-19.
- Download the git repository following the instructions
for downloading the git repository
- The example code for testing can be found in the subdirectory
Trying out gnatstudio
- You can start gnatstudio directly as an application.
- Then you can open from the starting menu or
file menu SPARK Ada project
file main.gpr located in the directory
This file may be called something like GNAT project file.
- You can as well associate gnatstudio as default application for
files with extension gpr, so that it will be opened from
SPARK Ada project files.
This might be already the case if you have
installed SPARK Ada yourself on a Windows computer.
- In this case you can start gnatstudio directly from the
main.gpr file in the directory
exampleCodeForTestingInstallations (called "project file" in windows)
- Opening gnatstudio might take a while initially because it initialises some data.
- It should look approximately like the following
- There should be a menu item SPARK on the top.
If you don't have this item, you have only installed
Ada but not SPARK Ada.
- If you execute SPARK → Examine all, you should see
at the buttom a script running which should check your code
successfully, provided you have the correct version of SPARK
- Please note:
- Always open gnatstudio by clicking on the main.gpr file.
- Don't add files to gnatstudio 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 gnatstudio 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
- Under Windows use the option "run in an external terminal"
which will open a
command shell. From there you can run the program
which is usually called main.exe.
- Under Linux make sure you have set it up as follows
- In gnatstudio, go to
edit → preferences → External commands → on right side
change "xterm -hold -e" to "xterm -hold"
- Just delete -e, don't copy from the webpage since it might replace - by a
similar but different symbol.
- If you accidentially changed it or have problems later just enter from the keyboard
- After setting it up when you execute
Run → Custom
the command "xterm -hold" should be shown.
- Now you click on both "Run in executables directory"
and "Run in an external terminal".
- In case your executable file is not main.adb but myfile.adb type in ./myfile
- You can keep that terminal open and use it for executing the executable again
- When doing those steps the program should open 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 → Examine All
- To prove your code for generating verification conditions use
SPARK → Prove All
- I recommend to choose as proof stategy Progressively split
- To close gnatstudio use first File→ Save an`d 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 under Linux).