8. Using GNAT SAS in GNAT Studio

8.1. Prerequisites

We recommend using a matching version of GNAT SAS and GNAT Studio. GNAT Studio is also designed to be backward compatible with older versions of GNAT SAS. Using an older version of GNAT Studio with a newer version of GNAT SAS is not supported, but it can work in some cases.

If the compiler for your project is not GNAT, make sure you have properly setup your project file, as explained in Use of Libraries Installed with GNAT.

8.2. Running GNAT SAS Analysis

When GNAT SAS is installed and found on your PATH, GNAT Studio will automatically detect it and provide a new GNATSAS top level menu.

Analyze All launches the default analysis. Analyze... opens a dialog when you can select more precisely the kind of analysis performed and in particular to add or override GNAT SAS switches defined in your project file.

After an analysis finishes, GNAT Studio automatically opens the Report Window. The Report Window can be also opened manually by choosing Display Code Review.

See also

See GNAT SAS menu for a detailed description of the GNATSAS menu.

8.3. Viewing GNAT SAS Output in GNAT Studio

8.3.1. Selecting the Results to Display

GNAT Studio has the following three behaviors:

• New results are automatically displayed in the GNAT SAS Report Window after each analysis done from GNAT Studio.

• You can display the results from the last run (even after having just opened GNAT Studio) by clicking on the menu GNATSAS ‣ Display Code Review.

• With the menu GNATSAS ‣ Advanced ‣ Regenerate Report…, you may:

  • Display the results of an arbitrary run. The last run is displayed by default. To select another run, specify the --timeline <TIMELINE> switch to the command-line.

  • Compare that run to an arbitrary SAM file (ignoring the baseline), with the field Compare with. This maps to the --compare-with <sam-file> switch.

  • Customize report generation by passing arbitrary gnatsas report switches to the command-line.

  See also

  Refer to Timelines for more information about timelines and to GNAT SAS CLI Reference for more details about the GNAT SAS command line usage.

• With the menu GNATSAS ‣ Advanced ‣ Display Result File…, you can select an arbitrary SAM file and display the results it contains.

8.3.2. GNAT SAS Report Window

When you open a GNAT SAS report (see Selecting the Results to Display), the Locations View is filled with messages from the GNAT SAS run, and the Report Window is displayed.

The top part of the Report Window shows information about the baseline run and the current run. For each of them, the following data is displayed:

• the name of the run's SAM file as <sam-file-name>.sam, or <run_name> (<sam-file-name>.sam) if a name was set with --run-name

• the absolute and relative date of the run

• the corresponding command-line, which can be useful to remind you of any specific switches used, like the analysis mode.

Note

The above information is also available in a structured format in the SAM file corresponding to the run.

Shortcut buttons to execute baseline actions (bumping the baseline, setting a new baseline or replacing the current run) are also available, corresponding to the Baseline submenu (see GNAT SAS menu).

Warning

The above actions will only apply to the timeline corresponding to the last run. To execute such actions for different timelines, either run an analysis with an explicit --timeline TIMELINE switch beforehand, or use the GNAT SAS command line. Refer to Timelines for more information about timelines and to GNAT SAS CLI Reference for more details about the GNAT SAS command line usage.

The Report Window has two tabs: Messages and Race conditions. The first tab provides a summary of all messages and filtering capabilities, and the second provides a summary of potential race conditions found. The race conditions tab is only meaningful when GNAT SAS is run in deep analysis mode.

On the left side of the messages window, there is a main area listing all files for which messages have been generated, with information organized hierarchically by project, file and subprograms. You can click on any file to display the first message on this file in the Locations View. See Using the Locations View for more details on the use of the Locations View.

Similarly, you can double click on any file or subprogram to jump to the corresponding source editor, which will be displayed with their corresponding Inspector annotations (if Inspector was enabled during the analysis).

For each of these entities, three columns displaying the number of high, medium and low messages corresponding to the current filter selection (see Using Filters).

Different kinds of filters are available on the right side of the window. Clicking on each of these filters will show/hide the corresponding messages in the Locations View. This way, you can easily concentrate on e.g. high ranking messages only, or on a specific category (e.g. validity check) during your review of the messages.

The filters are divided into four kinds:

• Message categories

  This section (the first column on the right of the file summary) lists all the message categories found in the current analysis in two groups: warnings and checks. In addition, it lists all CWEs found in the current analysis when displaying of CWEs is enabled. By default, all categories found are enabled, and you can select/unselect all categories in each group at once by clicking on the check box left to the Warning categories (or Check categories, or CWE categories) label, or individually by checking each item. See GNAT SAS Messages Reference for more details on the meaning of each category.

  CWE categories filter applies for all kinds of messages. When some CWE is selected in filter all messages with this CWE are displayed (even when not selected in Warning categories and Check categories filters). Precondition messages are displayed when related checks have the chosen CWE.

• Message history

  By default, added and unchanged messages are displayed (with respect to baseline). You can also select old removed messages that are no longer present in the last run, or concentrate on added messages only and ignore unchanged messages. This is particularly useful when using GNAT SAS on legacy code, without having to review previously found messages, and concentrate on messages found after new changes, to analyze the impact of these new changes.

• Message ranking

  By default, GNAT Studio only displays the most interesting messages (ranked medium and high). Once you have reviewed these messages, reviewing the low messages can be useful. It can also help understanding some messages to display the low and/or info messages, which can provide additional information.

• Message review status

  By default, GNAT Studio displays all the messages except for the ones that have a review of review status kind Not_A_Bug (i.e. with review status not a bug, false positive, intentional, or any Custom Review Status of this kind). You can change this default setting by checking or unchecking the corresponding boxes.

On the top of the race conditions window, there is a list of shared objects. Clicking on shared object will open a list of entry points in the bottom of the race conditions window and automatically scroll the Locations window to simplify access to locations where shared objects are used.

On the bottom side of the race conditions window, a list of entry points and kind of access is displayed for the currently selected shared object. Clicking on row of this view opens source editor at scroll it to point of access to shared object.

8.3.3. Using the Locations View

When you open a GNAT SAS report (see Running GNAT SAS Analysis), the Locations View at the bottom part of GNAT Studio is filled with messages from the GNAT SAS run.

You can click on any of these messages, and GNAT Studio will open a source editor containing the relevant source file, at the listed source location. You can also use the Filter panel available from the contextual menu in the Locations View in order to display only messages containing a specific text pattern.

When a precondition related message is displayed, extra information may be provided by GNAT SAS as secondary locations associated with the message, giving source locations that are related to the precondition check such as calls forming a call stack, as well as actual checks (e.g. range check) related to the precondition message. Each of these secondary locations can be clicked to see the corresponding source code and ease understanding these messages. In other words, these secondary locations are places where GNAT SAS learned about the range of values of the variables or expressions mentioned in the message, and in particular, provides the call stack that would lead to the selected potential precondition failure.

For more details on how to use the Locations View, see the GNAT Studio documentation directly, which explains how this view is managed.

In addition, an Edit icon is displayed in front of each GNAT SAS message. Clicking on this icon allows you to post a manual review, or a source review (through a pragma Annotate), of the message. It is possible to review single or multiple messages at once. See Reviewing Messages for more information about use of message review dialogs.

8.3.4. Exploring Inspector Annotations

Inspector generates annotations as-built documentation for each subprogram that it analyzes. This documentation is presented in the form of virtual comments at the beginning of each subprogram in a source-editor window. This as-built documentation includes annotations in the form of Preconditions, Presumptions, Postconditions, etc. which characterize the functioning of the subprogram, as determined by a global static analysis of the subprogram and the routines that it calls, directly or indirectly.

See also

• For more details on the form of these annotations, see Inspector Annotations.

• For more details on using these annotations as part of code review, see Use Annotations generated by Inspector for Code Reviews.

The annotations are not actually added to your source code; they are only visible when viewing the source in a GNAT Studio source-editor window. You may hide the annotations using the GNATSAS ‣ Hide annotations item in the source editor's contextual menu. You may display them again using the contextual menu item GNATSAS ‣ Show annotations.

Note

By default, Inspector's annotations will be imported and displayed in the source editor. This step can take a significant amount of time for large projects and can be disabled globally via the Preferences and Project Properties.

8.3.5. Source Navigation

Using the GNAT Studio source navigation can be very useful for understanding GNAT Studio messages, verifying that messages are indeed relevant, and modifying the source code.

In particular, using the Find all references and Find all local references contextual menu, as well as Goto body will help significantly with reviewing messages.

For more information on GNAT Studio source-navigation capabilities, see the GNAT Studio User's Guide..

8.4. Reviewing messages through GNAT Studio

This section explains how to review GNAT SAS messages directly from GNAT Studio.

See also

For more information about the general review process, refer to Reviewing Results and Improving Code.

In GNAT Studio, when clicking the Edit icon at the left side of message in the Locations View (see Using the Locations View), you can choose between Manual review or Annotate. The default action to use can be configured through the "Default review action" in Preferences and Project Properties.

8.4.1. Manual review

When clicking on Manual review, you get two possible review dialogs: one to review a single message and another to review multiple messages. Which dialog will be used depends on how many messages are selected in the Locations View before clicking on the edit icon.

The New Status drop-down box allows selecting the review status of the message. The review status is initially set to Uncategorized and can be set to Pending, Not A Bug, Intentional, False Positive, Bug or any Custom Review Status.

Note

The review status impacts the behavior of GNAT Studio: by default, GNAT Studio hides any messages that have as review status either Intentional` or False Positive. In addition, in the Locations View, GNAT Studio highlights messages with different colors depending on the review status.

The Approved By text box allows the name of the reviewer to be recorded.

The Comment text box allows the reviewer to enter an explanation/justification for the message.

The single-message review dialog displays a history of the changes related to that message, while the multiple-message review dialog displays a list of messages to be reviewed along with their ranking and review status.

8.4.2. Annotating the source

When selecting Annotate, GNAT Studio automatically inserts a pragma Annotate at the correct source position. You are left with updating its content accordingly to your review, see Through Pragma Annotate / Justification in Source Code.

8.5. GNAT SAS entry points

8.5.1. GNAT SAS menu

The main entry point to run GNAT SAS and display analysis results is the GNAT Studio menu GNATSAS. This section provides a complete description of this menu.

• Analyze All

  Launches the default analysis, and load the GNAT SAS report window. See Viewing GNAT SAS Output in GNAT Studio for more details on the Report Window. This menu item will use the GNAT SAS switches set in your project files, if any.

• Analyze...

  Open a dialog where you can choose the kind of analysis you want to do. This dialog lets you select graphically the options described below. If there is a conflict between the selected options and the ones set in your project file, the ones set in this menu take precedence.

  Multiprocessing	Specify the number of processes to generate SCIL files and analyze files (0 means use as many cores as available on the machine). Maps to the -j switch.
  Analysis mode	Set the analysis mode to either fast (the default) or deep (see Analysis modes). Maps to the --mode switch.
  Root project only	GNAT SAS will only analyze the source files associated with the root project file (presuming your application uses a tree of project files to represent all of its constituents). Maps to the --no-subprojects switch.
  Force analysis	Force generation of all SCIL files and analysis of all files (without incrementality). Maps to the -f switch.
  Enable GNAT Warnings	Enable/disable launching GNAT front end and collecting its warnings, see Configuring GNAT Warnings. Maps to the --gnat switch.
  Enable Infer	Enable/disable Infer analysis (enabled by default). Maps to the --infer/--no-infer switches.
  Enable Inspector	Enable/disable Inspector analysis (enabled by default). Maps to the --inspector/--no-inspector switches.
  Enable GNATcheck	Enable/disable GNATcheck analysis (enabled by default). Maps to the --gnatcheck/--no-gnatcheck switches.

  Once the selection is done, click on the Execute button to get a behavior similar to Analyze All.

• Analyze File

  Perform a default analysis of the current source file only. This menu is only available when a source file is selected in GNAT Studio.

  Note that this makes Inspector's analysis ignore effects of calls to functions outside the selected file (this only affects deep mode analysis).

  Note that analyzing a generic unit will have no effect: you need to analyze one of its instantiations to get messages on a generic unit. Analyzing a subunit (separate unit) will trigger an analysis on the enclosing unit.

  In order to set more switches when analyzing a single file, you can either set those switches in your project files, or use Analyze..., and append --file %F to the end of the command line.

• Display Code Review

  Load the GNAT SAS results and review information from the disk, and display a summary. See Viewing GNAT SAS Output in GNAT Studio for more details.

• Generate HTML Report...

  Generate a GNAT SAS report in HTML format. This menu must be run after a GNAT SAS analysis has completed. See HTML Output for more information. The following switch can be specified to refine the information generated, as part of an intermediate dialog:

  Show info messages

  Show messages of kind info (hidden by default).

• Generate CSV Report...

  Generate a GNAT SAS report in CSV format, and open the report in a source editor. This menu must be run after a GNAT SAS analysis has completed. It will open an intermediate dialog with the following options.

  Show annotations	Show Inspector's annotations in addition to messages (hidden by default).
  Show info messages	Show messages of kind info (hidden by default).
  Show removed	Show messages removed from the baseline run (hidden by default).
  Hide low messages	Hide messages that have a low ranking (shown by default).

  See CSV Output for more details on the CSV output.

• Baseline

  This submenu provides baseline manipulation actions (see Comparing GNAT SAS Runs).

  • Bump Baseline to Current Run

    Make the last run the new baseline for following runs in the current timeline.

  • Set Baseline to Run...

    Select a new baseline. This opens a menu to select a SAM file.

  • Replace Current Run with Run...

    Select a SAM file that will be set as the current run (see Importing GNAT SAS Results).

  Warning

  The above actions will only apply to the timeline corresponding to the last run. To execute such actions for different timelines, either run an analysis with an explicit --timeline TIMELINE switch beforehand, or use the GNAT SAS command line. Refer to Timelines for more information about timelines and to GNAT SAS CLI Reference for more details about the GNAT SAS command line usage.

• Advanced

  This submenu provides advanced capabilities, less often needed:

  • Regenerate Report...

    Run GNAT SAS to regenerate a report without performing a new analysis. This can be used in order to:

    • Display the results of an arbitrary run. The last run is displayed by default. To select another run, specify the --timeline <TIMELINE> switch to the command-line.

    • Do a one-off comparison of that run with another arbitrary run using Compare with. If no file is selected, the baseline of the specified timeline (or the last run if none specified) is used for comparison.

    • Customize report generation by passing arbitrary gnatsas report switches to the command-line.

  • Display Result File...

    Select any SAM file and generate a report from it. You should ensure that the selected SAM file corresponds to a run on the project currently opened.

  • GNAT SAS Log

    Open a text editor with the low level log file produced by GNAT SAS. This can be useful for example to understand why GNAT SAS did not generate the expected output, or to send GNAT SAS bug reports.

Note that most of the menus will launch commands that can be configured or tuned using the Edit ‣ Preferences menu, in the Build Targets section. See the GNAT Studio documentation for more details on the build targets.

8.5.2. Preferences and Project Properties

The GNAT SAS plug-in for GNAT Studio adds the following preferences in Edit ‣ Preferences...:

• GNATSAS

  Import Inspector annotations

  Controls whether to import and display GNAT SAS annotations generated by Inspector analysis such as generated contracts and values of variables in the source editor. Note that importing GNAT SAS annotations can take a significant amount of time for large projects.

  Default review action

  Choose the default action performed when clicking on a review action. 'Review' to add a manual review; 'Annotate' to add a pragma Annotate to the code; or 'Both' to let the user choose the method for each review.

  Color for 'removed' messages

  Color to use for the foreground of removed messages in the Locations view.

The plug-in also adds the following properties to edit the Analyzer package of your project file in Edit ‣ Project Properties...:

• GNATSAS

  This menu lets you specify the GNAT SAS project attributes described in Analyzer package attributes, with the exception of the Switches attribute that is customizable with the interfaces listed below.

• Build/Switches/GNATSAS analyze

  This menu sets switches that impacts all analysis.

  Multiprocessing

  Specify the number of processes to generate SCIL files and analyze files (0 means use as many cores as available on the machine). Maps to the -j switch.

  Enable GNAT Warnings

  Enable/disable launching GNAT front end and collecting its warnings, see Configuring GNAT Warnings.

  Enable Infer

  Enable/disable Infer analysis (enabled by default).

  Enable Inspector

  Enable/disable Inspector analysis (enabled by default).

  Enable GNATcheck

  Enable/disable GNATcheck analysis (enabled by default).

• Build/Switches/GNATSAS inspector

  This menu sets switches specific to the Inspector analysis engine.

  Ignore representation clauses

  Perform analysis as if representation clauses had been stripped from the source code (see Representation Clauses).

  Unconstrained float overflow

  Check for overflow on unconstrained floating point types (see Detection of Floating Point Overflow).