Basic Usage of Gnatstudio

• 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 screen.
  • If you want to open an ads or adb file
    • make sure there is a directory containing one project only.
    • Add if necessary a main.gpr file.
    • 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 case.
• 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 "xterm -hold"
    • 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 later.
• 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).