.. _Getting_Started: *************** Getting Started *************** This chapter provides a quick introduction to GNAT SAS by illustrating the main concepts: analysis, report and review. The user is guided through a simple command-line example which does not require any particular configuration. .. note:: This chapter assumes that: * the user environment is a `bash` terminal; * GNAT SAS has been installed according to :ref:`Installation`. It also provides links to more advanced resources in :ref:`Resources`. The chapter does not try to cover all features or more advanced use cases. Refer to other chapters for more comprehensive documentation. Quick Start example =================== This section will illustrate how to run an analysis with GNAT SAS and view the analysis results, before showing how results can be reviewed and the code fixed. Let's first change the directory to the directory containing our example project :file:`/share/examples/gnatsas/uninitialized/`: .. code-block:: sh $ cd /share/examples/gnatsas/uninitialized/ This example namely contains: * a README file * a GPR project file :file:`uninitialized.gpr` (if that is new to you, refer to :ref:`Creating_Project_File`). * Ada source code (:file:`*.adb/*.ads` files). The project file is configured to use :file:`uninit.adb` as the main unit, and to use GNAT SAS in :ref:`deep mode`. .. seealso:: Refer to :ref:`Analysis_modes` for a description of the `fast` and `deep` modes provided by GNAT SAS. Analyzing the project --------------------- To analyze the project, run the ``gnatsas analyze`` command by specifying the name of the project file (the extension is optional): .. code-block:: sh $ gnatsas analyze -P uninitialized [gnatsas]: launching GNATcheck [gnatsas]: launching Infer [gnatsas]: launching Inspector Compile [Ada] uninit.adb [Ada] adt.adb Bind [gprbind] uninit.bexch [Ada] uninit.ali no partitioning needed. starting the analysis of adt.scil analyzed adt.scil in 0.00 seconds starting the analysis of adt__body.scil analyzed adt__body.scil in 0.00 seconds re-starting the analysis of adt.scil re-analyzed adt.scil in 0.00 seconds starting the analysis of uninit__body.scil analyzed uninit__body.scil in 0.00 seconds starting the analysis of uninit.scil analyzed uninit.scil in 0.00 seconds starting the analysis of b__uninit.scil analyzed b__uninit.scil in 0.00 seconds starting the analysis of b__uninit__body.scil analyzed b__uninit__body.scil in 0.00 seconds re-starting the analysis of b__uninit.scil re-analyzed b__uninit.scil in 0.00 seconds analysis complete. 6 .scil files processed; 14 subprograms analyzed. In the above output, we can see that GNAT SAS launched the following integrated engines and returned successfully (with exit code ``0``): * GNATcheck * Infer * Inspector There is some verbose output, in particular about the Inspector analysis, telling us that some files were compiled, and 14 subprograms were analyzed in total. Upon analysis GNAT SAS analysis artifacts were generated and stored under a directory :file:`gnatsas`, which in particular contains the **output directory** :file:`gnatsas/uninitialized.outputs` (hereafter referred to as :file:``). That directory contains important files among others: * a :ref:`Message file` containing messages found during the current analysis run: :file:`uninitialized.deep.sam` * the baseline for this run: :file:`uninitialized.deep.baseline.sam`. However, ``gnatsas analyze`` does not directly display the results. That is done by the ``gnatsas report`` command as we will see next. .. note:: The version of engines in the output (e.g. ``gnatcheck 25.0w (20231112)`` may vary depending on the GNAT SAS version). .. seealso:: * Refer to :ref:`Analyzing_Code` for a comprehensive description of GNAT SAS analysis. * Refer to :ref:`GNAT_SAS_Files` for a description of GNAT SAS artifacts. Viewing the results ------------------- Printing the text report ^^^^^^^^^^^^^^^^^^^^^^^^ The resuts from the Message file :file:`/uninitialized.deep.sam` can be displayed with the ``gnatsas report`` command that is run similarly by specifying the project file name: .. code-block:: sh $ gnatsas report -P uninitialized which outputs the following list of messages in text format on standard output: .. code-block:: text uninit.adb:7:4: high: validity check [CWE 457] (Infer): `X.B1` is read without initialization during the call to `adt.update` uninit.adb:7:4: medium: precondition [CWE 190] (Inspector): precondition might fail on call to adt.update; requires not X.B1 or X.DZ /= Integer_32'Last The messages are formatted such as: .. code-block:: text filename:line:column: rank: kind (analysis engine name): message contents Here, for instance, the first message is emitted by Infer, has a `high` ranking, and is reported on :file:`uninit.adb` at line 7, column 4: .. code-block:: ada :linenos: with ADT; use ADT; procedure Uninit is T : ADT_Type; begin Initialise (T); Update (T); -- high validity check reported here end Uninit; The `kind` of the message is ``validity check [CWE 457]``, which means that GNAT SAS reports a potential error due to accessing an uninitialized variable. The ``[CWE 457]`` part indicates that this kind of message has the identifier ``457`` in the `Common Weakness Enumeration (CWE) `_; it is optional, not all messages can be linked to a CWE weakness. The description of the specific potential violation corresponding to this kind is detailed in the `message contents` that lets us know that ``X.B1`` is read without initialization when calling ``adt.update``. Note that this is an example of performing analysis across multiple units. .. note:: Such check requiring cross-unit analysis can only be done in deep mode with the Inspector engine (the analysis mode only influences the results of Inspector and the result of Infer is not impacted). If you want to compare to the results in fast mode, you can quickly run: .. code-block:: sh $ gnatsas analyze -P uninitialized --mode=fast $ gnatsas report -P uninitialized That will only report the Infer message. Indeed, if we look at how the body of :file:`adt.adb`, we can see that ``X.B1`` is never initialized: .. code-block:: ada :linenos: package body ADT is ---------------- -- Initialise -- ---------------- procedure Initialise (X : out ADT_Type) is begin X.V1 := 1; -- we didn't initialize X.B1 nor X.DZ end Initialise; ------------ -- Update -- ------------ procedure Update (X : in out ADT_Type) is begin if X.B1 then -- read uninitialized field X.B1 X.V1 := X.V1 +2; X.DZ := X.DZ +1; -- read uninitialized field X.DZ end if; end Update; end ADT; .. seealso:: * We will not describe other messages here; refer to :ref:`Messages_and_Annotations` for more information about all supported checks and related message kinds. * For more information about the CWEs supported by GNAT SAS, refer to :ref:`CWE_Support`. * In this example the results are reported as text, but GNAT SAS supports various other formats (e.g. CSV, SARIF...). Refer to :ref:`How_To_View_GNAT_SAS_Output` for a comprehensive description of GNAT SAS reporting capabilities. Looking at backtraces ^^^^^^^^^^^^^^^^^^^^^ Messages reported by GNAT SAS may contain even more details, by showing us the backtraces associated to the potential issues. To enable displaying backtraces, simply run with ``--show-backtraces``: .. code-block:: sh $ gnatsas report -P uninitialized --show-backtraces The first message is now reported as: .. code-block:: text uninit.adb:7:4: high: validity check [CWE 457] (Infer): `X.B1` is read without initialization during the call to `adt.update` struct field address `B1` created at uninit.adb:4:4 when calling `adt.update` here at uninit.adb:7:4 parameter `X` of adt.update at adt.adb:16:4 read to uninitialized value occurs here at adt.adb:18:10 The backtrace provides more information: * first, ``X.B1`` is created as a record field when declaring the variable ``T`` with type ``ADT_Type`` in :file:`uninit.adb`:4:4 * then ``T`` is passed as argument to ``ADT.Update`` where the corresponding formal parameter ``X`` has its field ``X.B1`` read without initialization in :file:`adt.adb`:18:10. .. seealso:: Refer to :ref:`CLI_Reference` for more information about command-line switches. Filtering messages ^^^^^^^^^^^^^^^^^^ The ``gnatsas report`` command also supports advanced filtering of messages. For example, say that as a first step, we are only interested in seeing messages of `high` ranking. This is specified with ``--show rank=high``: .. code-block:: sh $ gnatsas report -P uninitialized --show rank=high Only `high` ranked messages are reported (one in this case): .. code-block:: text uninit.adb:7:4: high: validity check [CWE 457] (Infer): `X.B1` is read without initialization during the call to `adt.update` .. seealso:: * The ``--show`` switch provides much flexibility. See :ref:`Filtering_Messages` for a full description. * The ranking described above corresponds to a message categorization done by GNAT SAS, depending on how interesting and likely to happen they are. See :ref:`Categorization_of_Messages`. Reviewing the results --------------------- Triaging ^^^^^^^^ The first step of a review is to "triage" the message depending on its nature: false positive, intentional violation, or actual bug. Then, depending on the use cases, the review information may be shared with other developers, validated, before the code is fixed if needed. Or you may want to fix the code directly if the error is introduced in your development branch. .. seealso:: Refer to :ref:`GNAT_SAS_Workflows` for example use cases and recommended workflows. In this example, we'll consider the case where we want to store the review information. We will use the :ref:`review through CSV file ` method to review the first message described above, which we already identified as being a bug. Following this method we will: * output messages in CSV format * add the review information to the CSV file * tell GNAT SAS to import the review information. First, let's output only the Infer messages with `high` ranking, this time in a CSV format using ``gnatsas report csv``, and store them in a file :file:`messages.csv` with the ``-o`` switch: .. code-block:: sh $ gnatsas report csv -P uninitialized --show rank=high,tool=infer -o messages.csv :file:`messages.csv` contents is as below, containing exactly one message in this example: .. code-block:: text project,basename,path,subp,line,column,category,history,ranking,tool,message,cwe,kind,related_checks,key,key_seq,review_from_source,review_kind,review_date,review_status,review_author,review_text uninitialized.gpr,uninit.adb,uninit.adb,uninit,7,4,check,unchanged,high,Infer,`X.B1` is read without initialization during the call to `adt.update`,457,validity check,,6c2d263aed531f7fcb81e1f2c3a864c6,1,false,uncategorized,,,, Now, let's modify the fields, then save the modified file as :file:`reviews.csv`: * ``review_status`` with ``bug`` * ``review_author`` with your name (e.g. ``Jules Verne``) * ``review_text`` with a comment (e.g. ``Missing initialization of ADT_Type.B1 field``). which now contains: .. code-block:: text project,basename,path,subp,line,column,category,history,ranking,tool,message,cwe,kind,related_checks,key,key_seq,review_from_source,review_kind,review_date,review_status,review_author,review_text uninitialized.gpr,uninit.adb,uninit.adb,uninit,7,4,check,unchanged,high,Infer,`X.B1` is read without initialization during the call to `adt.update`,457,validity check,,6c2d263aed531f7fcb81e1f2c3a864c6,1,false,uncategorized,,bug,Jules Verne,Missing initialization of ADT_Type.B1 field Finally, let's inform GNAT SAS about this new review information with the ``gnatsas review`` command: .. code-block:: sh $ gnatsas review -P uninitialized --from-csv reviews.csv [gnatsas | review]: reviews imported The `output directory` should now contain a :ref:`Review_File` named :file:`/uninitialized.sar` containing the review information in a GNAT SAS format. Let's display again the messages (e.g. as text with ``--show-reviews``) to confirm that the review has been associated to the corresponding message: .. code-block:: sh $ gnatsas report -P uninitialized --show-reviews .. code-block:: text uninit.adb:7:4: high: validity check [CWE 457] (Infer): `X.B1` is read without initialization during the call to `adt.update`. review: 2023-11-30 13:05:42: Bug, Bug, approved by Jules Verne: Missing initialization of ADT_Type.B1 field uninit.adb:7:4: medium: precondition [CWE 190] (Inspector): precondition might fail on call to adt.update; requires not X.B1 or X.DZ /= Integer_32'Last As you can see above, the first message now has review information available. .. seealso:: Refer to :ref:`Reviewing_Results_And_Improving_Code` for a comprehensive description of the reviewing capabilities in GNAT SAS. Fixing the code ^^^^^^^^^^^^^^^ Now that we have examined the first message reported and triaged it as a bug with relevant review information, let's fix it by editing the ``Initialize`` procedure in :file:`adt.adb` to initialize ``X.B1``: .. code-block:: ada :linenos: package body ADT is ---------------- -- Initialise -- ---------------- procedure Initialise (X : out ADT_Type) is begin X.V1 := 1; X.B1 := True; -- fixed end Initialise; Let's run the analysis again and display the results (filtering Infer messages only for the example) to confirm that the issue has been fixed: .. code-block:: sh $ gnatsas analyze -P uninitialized $ gnatsas report -P uninitialized --show tool=infer .. code-block:: text uninit.adb:7:4: [added] high: validity check [CWE 457] (Infer): `X.DZ` is read without initialization during the call to `adt.update` The first message related to the missing initialization of ``X.B1`` has disappeared from the output and we now have another message related to a similar issue with ``X.DZ``, showing as ``[added]``. Comparing runs ^^^^^^^^^^^^^^ Another useful GNAT SAS feature is the capability to compare analysis runs. By default, ``gnatsas report`` will automatically compare the results of the analysis with the results of the previous run *(of the same timeline, see* :ref:`Timeline` *for more details)*. This is why the new message was tagged as ``[added]``. We can also force the display of removed messages with ``--show age+removed``: .. code-block:: sh $ gnatsas report -P uninitialized --show tool=infer,age+removed --show-reviews The list of messages now shows the previously fixed message as ``[removed]``: .. code-block:: text uninit.adb:7:4: [removed] high: validity check [CWE 457] (Infer): `X.B1` is read without initialization during the call to `adt.update`. review: 2023-11-30 13:05:42: Bug, Bug, approved by Jules Verne: Missing initialization of ADT_Type.B1 field uninit.adb:7:4: [added] high: validity check [CWE 457] (Infer): `X.DZ` is read without initialization during the call to `adt.update` .. seealso:: * See :ref:`Filtering_Messages` for a full description of the ``--show`` switch. * You may also compare arbitrary runs; refer to :ref:`GNAT_SAS_Baseline` for more details. .. _Resources: More Resources ============== * Several other example projects are available: * under `/share/examples/gnatsas` * or via the :menuselection:`Help --> GNATSAS --> Examples` menu in GNAT Studio. * For an advanced tutorial focusing particularly on the use of GNAT SAS in GNAT Studio and on the Inspector analysis engine, refer to the GNAT SAS tutorial available: * under `/share/doc/gnatsas/tutorial` * or via the :menuselection:`Help --> GNATSAS --> GNATSAS Tutorial` menu in GNAT Studio.