GNAT Programming Studio

This chapter presents an introduction to the GNAT Programming Studio (GPS), which provides an IDE to develop applications in Ada. For a detailed overview, please refer to the GPS tutorial. Also, you can refer to the GPS product page for some introductory videos.

In this chapter, all indications using "→" refer to options from the GPS menu that you can click in order to execute commands.

Start-up

The first step is to start-up the GNAT Programming Studio. The actual step depends on your platform.

Windows

  • You may find an icon (shortcut to GPS) on your desktop.
  • Otherwise, start GPS by typing gps on the command prompt.

Linux

  • Start GPS by typing gps on a shell.

Creating projects

After starting-up GPS, you can create a project. These are the steps:

  • Click on Create new project in the welcome window

    • Alternatively, if the wizard (which let's you customize new projects) isn't already opened, click on FileNew Project... to open it.
    • You should see a window with this title: Create Project from Template
  • Select one of the options from the list and click on Next.

    • The simplest one is Basic > Simple Ada Project, which creates a project containing a main application.
  • Select the project location and basic settings, and click on Apply.

    • If you selected "Simple Ada Project" in the previous step, you may now select the name of the project and of the main file.
    • Note that you can select any name for the main file.

You should now have a working project file.

Building

As soon as you've created a project file, you can use it to build an application. These are the required steps:

  • Click on ProjectBuildBuild All

    • You can also click on this icon:
../../../_images/gnat_windows_build_opt.png
  • Alternatively, you can click on ProjectBuildBuild & Run<name of your main application>

    • You can also click on this icon:
../../../_images/gnat_windows_build_run_opt.png
  • You can also use the keyboard for building and running the main application:

    • Press F4 to open a window that allows you to build the main application and click on Execute.
    • Then, press Shift + F2 to open a window that allows you to run the application, and click on Execute.

Debugging

Debug information

Before you can debug a project, you need to make sure that debugging symbols have been included in the binary build. You can do this by manually adding a debug version into your project, as described in the previous chapter (see GPRbuild).

Alternatively, you can change the project properties directly in GPS. In order to do that, click on EditProject Properties..., which opens the following window:

../../../_images/gnat_windows_project_debug_opt.png

Click on BuildSwitchesAda on this window, and make sure that the Debug Information option is selected.

Improving main application

If you selected "Simple Ada Project" while creating your project in the beginning, you probably still have a very simple main application that doesn't do anything useful. Therefore, in order to make the debugging activity more interesting, please enter some statements to your application. For example:

with Ada.Text_IO; use Ada.Text_IO;

procedure Main is
begin
   Put_Line ("Hello World!");
   Put_Line ("Hello again!");
end Main;

Debugging the application

You can now build and debug the application by clicking on ProjectBuildBuild & Debug<name of your main application>.

You can then click on DebugRun... to open a window that allows you to start the application. Alternatively, you can press Shift + F9. As soon as the application has started, you can press F5 to step through the application or press F6 to execute until the next line. Both commands are available in the menu by clicking on DebugStep or DebugNext.

When you've finished debugging your application, you need to terminate the debugger. To do this, you can click on DebugTerminate.

Formal verification

In order to see how SPARK can detect issues, let's creating a simple application that accumulates values in a variable A:

procedure Main
  with SPARK_Mode is

   procedure Acc (A : in out Natural;
                  V :        Natural) is
   begin
      A := A + V;
   end Acc;

   A : Natural := 0;
begin
   Acc (A, Natural'Last);
   Acc (A, 1);
end Main;

You can now click on SPARKProve All, which opens a window with various options. For example, on this window, you can select the proof level — varying between 0 and 4 — on the Proof level list. Next, click on Execute. After the prover has completed its analysis, you'll see a list of issues found in the source code of your application.

For the example above, the prover complains about an overflow check that might fail. This is due to the fact that, in the Acc procedure, we're not dealing with the possibility that the result of the addition might be out of range. In order to fix this, we could define a new saturating addition Sat_Add that makes use of a custom type T with an extended range. For example:

procedure Main
  with SPARK_Mode is

   function Sat_Add (A : Natural;
                     V : Natural) return Natural
   is
      type T is range Natural'First .. Natural'Last * 2;

      A2     : T          := T (A);
      V2     : constant T := T (V);
      A_Last : constant T := T (Natural'Last);
   begin
      A2 := A2 + V2;

      --  Saturate result if needed
      if A2 > A_Last then
         A2 := A_Last;
      end if;

      return Natural (A2);
   end Sat_Add;

   procedure Acc (A : in out Natural;
                  V :        Natural) is
   begin
      A := Sat_Add (A, V);
   end Acc;

   A : Natural := 0;
begin
   Acc (A, Natural'Last);
   Acc (A, 1);
end Main;

Now, when running the prover again with the modified code, no issues are found.