Example Code for Testing Installation of Spark Ada

Preliminaries

• In the following we use the Linux terminology "directory" for what is called in Windows "folder".
• 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 exampleCodeForTestingInstallations

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 exampleCodeForTestingInstallations.
    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 Screenshot
• 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 Ada installed.

Basic Usage of gnatstudio