GNAT SAS User's Guide

Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.1 or any later version published by the Free Software Foundation; with no Invariant Sections, with no Front-Cover Texts, and with no Back-Cover Texts. A copy of the license is included in the section entitled 'GNU Free Documentation License'.

• 1. Introduction
  • 1.1. About GNAT SAS
  • 1.2. Features Overview
  • 1.3. Integrated Analysis Engines
    • 1.3.1. Inspector
    • 1.3.2. Infer
    • 1.3.3. GNAT Warnings
    • 1.3.4. GNATcheck
  • 1.4. Installation
    • 1.4.1. Prerequisites
    • 1.4.2. Installation under Windows
    • 1.4.3. Installation under GNU/Linux
• 2. Getting Started
  • 2.1. Quick Start example
    • 2.1.1. Analyzing the project
    • 2.1.2. Viewing the results
    • 2.1.3. Reviewing the results
  • 2.2. More Resources
• 3. Project Setup
  • 3.1. Configuration for Third Party Compilers
  • 3.2. Creating a Project File
    • 3.2.1. Creating a Project File with GNAT Studio
    • 3.2.2. Creating a Project File Manually
    • 3.2.3. Generating a Project File
  • 3.3. Ensuring compatibility with GNAT SAS
    • 3.3.1. Using GNAT SAS-Specific Project Settings
    • 3.3.2. Support for UTF-8 encoding
    • 3.3.3. Use of Libraries Installed with GNAT
    • 3.3.4. Use of Predefined Ada Packages
    • 3.3.5. Use of Compiler-Specific Packages
    • 3.3.6. Using Preprocessing
    • 3.3.7. Arbitrary Naming Scheme
    • 3.3.8. Ada Language Version
    • 3.3.9. Representation Clauses
    • 3.3.10. Target Configuration File
    • 3.3.11. Using the GNAT Target Runtime Directory
    • 3.3.12. Configuration of System Package (system.ads)
    • 3.3.13. Ignoring Pragmas
    • 3.3.14. Providing Stubs for Missing Generic Bodies
  • 3.4. Configuring the Analysis
    • 3.4.1. Analyzer package attributes
    • 3.4.2. Partial Analysis
    • 3.4.3. Configuring GNATcheck
    • 3.4.4. Configuring Infer
    • 3.4.5. Configuring GNAT Warnings
    • 3.4.6. Configuring Inspector
• 4. Analyzing Code
  • 4.1. Running GNAT SAS Analysis
    • 4.1.1. Running GNAT SAS from the Command Line
    • 4.1.2. Running GNAT SAS from GNAT Studio
  • 4.2. Analysis modes
  • 4.3. Timelines
    • 4.3.1. Using custom timelines
    • 4.3.2. Displaying timeline information
  • 4.4. Getting the Right GNAT SAS Settings
    • 4.4.1. Analyze Messages
    • 4.4.2. Run GNAT SAS Faster
• 5. Viewing Results
  • 5.1. GNAT SAS Report Command
    • 5.1.1. Supported Report Formats
    • 5.1.2. Selecting the Results to Display
    • 5.1.3. Filtering Messages
  • 5.2. Comparing GNAT SAS Runs
    • 5.2.1. Classifying Messages as Unchanged, Added, and Removed
  • 5.3. Viewing GNAT SAS Output in IDEs
    • 5.3.1. In GNAT Studio
    • 5.3.2. In Visual Studio Code
  • 5.4. Report Formats in detail
    • 5.4.1. Text Output
    • 5.4.2. HTML Output
    • 5.4.3. CSV Output
    • 5.4.4. Security Report
    • 5.4.5. CodeClimate Export
    • 5.4.6. SARIF Export
    • 5.4.7. Exit Code
• 6. Reviewing Results and Improving Code
  • 6.1. Reviewing Messages
    • 6.1.1. Through GNAT Studio
    • 6.1.2. Through a CSV File
    • 6.1.3. Through Pragma Annotate / Justification in Source Code
    • 6.1.4. Viewing Reviews in the HTML Interface
    • 6.1.5. Custom Review Status
  • 6.2. Improve Your Code Specification
    • 6.2.1. Using Pragmas Assert and Assume
    • 6.2.2. Pragma Annotate / Modified in Source Code
    • 6.2.3. Pragma Annotate / Identifying Race conditions
    • 6.2.4. Using Pre and Post conditions
• 7. Workflows
  • 7.1. Use on a developer machine
  • 7.2. Nightly Runs on a Server
  • 7.3. Continuous Runs on a Server after Each Change
  • 7.4. Importing GNAT SAS Results
  • 7.5. Importing and Sharing GNAT SAS User Reviews
  • 7.6. Using GNAT SAS with a Jenkins Automation Server
    • 7.6.1. Jenkins Agent Setup
    • 7.6.2. Running the Analysis
    • 7.6.3. Getting Analysis Results
    • 7.6.4. Example Pipeline script
    • 7.6.5. Warnings Next Generation usage
  • 7.7. Easier Review of SAM files stored in Git
  • 7.8. Using GNAT SAS in a GitLab Pipeline
    • 7.8.1. Pre-requisites
    • 7.8.2. Running the Analysis
    • 7.8.3. Getting Analysis Results
    • 7.8.4. Example Pipeline script
    • 7.8.5. Advanced integration
• 8. Using GNAT SAS in GNAT Studio
  • 8.1. Prerequisites
  • 8.2. Running GNAT SAS Analysis
  • 8.3. Viewing GNAT SAS Output in GNAT Studio
    • 8.3.1. Selecting the Results to Display
    • 8.3.2. GNAT SAS Report Window
    • 8.3.3. Using the Locations View
    • 8.3.4. Exploring Inspector Annotations
    • 8.3.5. Source Navigation
  • 8.4. Reviewing messages through GNAT Studio
    • 8.4.1. Manual review
    • 8.4.2. Annotating the source
  • 8.5. GNAT SAS entry points
    • 8.5.1. GNAT SAS menu
    • 8.5.2. Preferences and Project Properties
• 9. Using GNAT SAS in Visual Studio Code
  • 9.1. Prerequisites
  • 9.2. Running GNAT SAS in Visual Studio Code
    • 9.2.1. Using the integrated terminal
    • 9.2.2. Using pre-defined tasks
  • 9.3. Viewing GNAT SAS Output in Visual Studio Code
• 10. GNAT SAS Files Reference
  • 10.1. Message Files
  • 10.2. Review File
  • 10.3. Additional artifacts
    • 10.3.1. runs_info file
    • 10.3.2. GNAT SAS logs
    • 10.3.3. Engine-specific outputs
    • 10.3.4. Inspector annotations
• 11. GNAT SAS Messages Reference
  • 11.1. Categorization of Messages
  • 11.2. CWE Categorization of Messages
    • 11.2.1. CWE to GNAT SAS Message Mapping
    • 11.2.2. CWE-676 Use of Potentially Dangerous Function
    • 11.2.3. CWE Top 25 Most Dangerous Software Errors
  • 11.3. GNATcheck Messages
  • 11.4. Infer Messages
  • 11.5. GNAT Warnings Messages
  • 11.6. Inspector Messages
    • 11.6.1. Run-Time Checks
    • 11.6.2. User Checks
    • 11.6.3. Uninitialized and Invalid Variables
    • 11.6.4. Warning Messages
    • 11.6.5. Information Messages
    • 11.6.6. Race Condition Messages
    • 11.6.7. Understanding the Differences between Preconditions and Run-time Errors
  • 11.7. Inspector Annotations
    • 11.7.1. Annotations
    • 11.7.2. Annotation Syntax
    • 11.7.3. Use Annotations generated by Inspector for Code Reviews
• 12. GNAT SAS CLI Reference
  • 12.1. gnatsas
    • 12.1.1. NAME
    • 12.1.2. SYNOPSIS
    • 12.1.3. DESCRIPTION
    • 12.1.4. COMMANDS
    • 12.1.5. COMMON OPTIONS
    • 12.1.6. MORE HELP
    • 12.1.7. EXIT STATUS
    • 12.1.8. BUGS
  • 12.2. gnatsas-analyze
    • 12.2.1. NAME
    • 12.2.2. SYNOPSIS
    • 12.2.3. DESCRIPTION
    • 12.2.4. OPTIONS
    • 12.2.5. COMMON OPTIONS
    • 12.2.6. MORE HELP
    • 12.2.7. EXIT STATUS
    • 12.2.8. BUGS
    • 12.2.9. SEE ALSO
  • 12.3. gnatsas-baseline
    • 12.3.1. NAME
    • 12.3.2. SYNOPSIS
    • 12.3.3. DESCRIPTION
    • 12.3.4. OPTIONS
    • 12.3.5. COMMON OPTIONS
    • 12.3.6. MORE HELP
    • 12.3.7. EXIT STATUS
    • 12.3.8. BUGS
    • 12.3.9. SEE ALSO
  • 12.4. gnatsas-help
    • 12.4.1. NAME
    • 12.4.2. SYNOPSIS
    • 12.4.3. DESCRIPTION
    • 12.4.4. ARGUMENTS
    • 12.4.5. OPTIONS
    • 12.4.6. COMMON OPTIONS
    • 12.4.7. MORE HELP
    • 12.4.8. EXIT STATUS
    • 12.4.9. BUGS
    • 12.4.10. SEE ALSO
  • 12.5. gnatsas-report
    • 12.5.1. NAME
    • 12.5.2. SYNOPSIS
    • 12.5.3. DESCRIPTION
    • 12.5.4. COMMANDS
    • 12.5.5. ARGUMENTS
    • 12.5.6. OPTIONS
    • 12.5.7. COMMON OPTIONS
    • 12.5.8. SHOW OPTION FORMATTING
    • 12.5.9. SHOW OPTION DEFAULT VALUE
    • 12.5.10. SHOW OPTION EXAMPLES
    • 12.5.11. MORE HELP
    • 12.5.12. EXIT STATUS
    • 12.5.13. BUGS
    • 12.5.14. SEE ALSO
  • 12.6. gnatsas-review
    • 12.6.1. NAME
    • 12.6.2. SYNOPSIS
    • 12.6.3. DESCRIPTION
    • 12.6.4. OPTIONS
    • 12.6.5. COMMON OPTIONS
    • 12.6.6. MORE HELP
    • 12.6.7. EXIT STATUS
    • 12.6.8. BUGS
    • 12.6.9. SEE ALSO
  • 12.7. gnatsas-report-code-climate
    • 12.7.1. NAME
    • 12.7.2. SYNOPSIS
    • 12.7.3. ARGUMENTS
    • 12.7.4. OPTIONS
    • 12.7.5. COMMON OPTIONS
    • 12.7.6. EXIT STATUS
    • 12.7.7. SEE ALSO
  • 12.8. gnatsas-report-csv
    • 12.8.1. NAME
    • 12.8.2. SYNOPSIS
    • 12.8.3. ARGUMENTS
    • 12.8.4. OPTIONS
    • 12.8.5. COMMON OPTIONS
    • 12.8.6. EXIT STATUS
    • 12.8.7. SEE ALSO
  • 12.9. gnatsas-report-exit-code
    • 12.9.1. NAME
    • 12.9.2. SYNOPSIS
    • 12.9.3. ARGUMENTS
    • 12.9.4. OPTIONS
    • 12.9.5. COMMON OPTIONS
    • 12.9.6. EXIT STATUS
    • 12.9.7. SEE ALSO
  • 12.10. gnatsas-report-html
    • 12.10.1. NAME
    • 12.10.2. SYNOPSIS
    • 12.10.3. ARGUMENTS
    • 12.10.4. OPTIONS
    • 12.10.5. COMMON OPTIONS
    • 12.10.6. EXIT STATUS
    • 12.10.7. SEE ALSO
  • 12.11. gnatsas-report-sarif
    • 12.11.1. NAME
    • 12.11.2. SYNOPSIS
    • 12.11.3. ARGUMENTS
    • 12.11.4. OPTIONS
    • 12.11.5. COMMON OPTIONS
    • 12.11.6. EXIT STATUS
    • 12.11.7. SEE ALSO
  • 12.12. gnatsas-report-security
    • 12.12.1. NAME
    • 12.12.2. SYNOPSIS
    • 12.12.3. ARGUMENTS
    • 12.12.4. OPTIONS
    • 12.12.5. COMMON OPTIONS
    • 12.12.6. EXIT STATUS
    • 12.12.7. SEE ALSO
  • 12.13. gnatsas-report-text
    • 12.13.1. NAME
    • 12.13.2. SYNOPSIS
    • 12.13.3. ARGUMENTS
    • 12.13.4. OPTIONS
    • 12.13.5. COMMON OPTIONS
    • 12.13.6. EXIT STATUS
    • 12.13.7. SEE ALSO
• 13. FAQ
  • 13.1. Migrating Away from the Historical CodePeer Database
    • 13.1.1. GNAT SAS Switches Changes
    • 13.1.2. sam-from-db
  • 13.2. What is the Difference between GNAT SAS and SPARK?
  • 13.3. What is the difference between GNAT SAS Messages and Compiler Warnings?
  • 13.4. Common Issues
    • 13.4.1. Compilation Errors
• 14. Appendix
  • 14.1. Inspector Reference
    • 14.1.1. How Does Inspector Work?
    • 14.1.2. Partitioning of Analysis
    • 14.1.3. Inspector Limitations and Heuristics
    • 14.1.4. Advanced Inspector Command Line Switches
    • 14.1.5. Format of MessagePatterns.xml File
  • 14.2. Inspector By Example
    • 14.2.1. Basic Examples
    • 14.2.2. Loop Examples
    • 14.2.3. Pointer Examples
    • 14.2.4. Unknown Subprograms
• 15. GNU Free Documentation License