CodePeer User’s Guide

Copyright (C) 2009-2019, AdaCore

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 CodePeer
  • 1.2. How to Install CodePeer
    • 1.2.1. Installation under Windows
    • 1.2.2. Installation under GNU/Linux
    • 1.2.3. Installation under different locations
  • 1.3. System Requirements
  • 1.4. Basic Project File Setup
    • 1.4.1. Basic Setup
    • 1.4.2. Configuring IDEs to Drive Tools
  • 1.5. Project File Setup
    • 1.5.1. Project File Creation
    • 1.5.2. Naming Scheme
    • 1.5.3. Ada Language Version
    • 1.5.4. 32bits Mode
    • 1.5.5. Representation Clauses
    • 1.5.6. Use of Predefined Ada Packages
    • 1.5.7. Use of Compiler Specific Packages
    • 1.5.8. Project Attributes
    • 1.5.9. Project File Example
  • 1.6. Advanced Project File Setup
    • 1.6.1. Arbitrary Naming Scheme
    • 1.6.2. Target Configuration File
    • 1.6.3. Using the GNAT Target Runtime Directory
    • 1.6.4. Configuration of System Package (system.ads)
    • 1.6.5. Using Preprocessing
    • 1.6.6. Ignoring Pragmas
    • 1.6.7. Providing Stubs for Missing Generic Bodies
    • 1.6.8. Detection of Floating Point Overflow
    • 1.6.9. CodePeer Specific Project Settings
    • 1.6.10. Ignoring Source File Timestamp Mismatch
    • 1.6.11. Ignoring Exception Handlers
    • 1.6.12. Handling Enumeration Representation Clauses
• 2. How to Run CodePeer
  • 2.1. Running CodePeer
    • 2.1.1. Running CodePeer from the Command Line
    • 2.1.2. Running CodePeer from GPS
    • 2.1.3. Running CodePeer from GNATbench
    • 2.1.4. Running CodePeer from Jenkins
  • 2.2. Getting the Right CodePeer Settings
    • 2.2.1. Analyze messages
    • 2.2.2. Run CodePeer Faster
  • 2.3. Running CodePeer in Compiler Mode
  • 2.4. Reducing the Number of False Alarms
  • 2.5. CodePeer Levels
  • 2.6. Provide Evidence for Program Verification
  • 2.7. CodePeer Baselines
    • 2.7.1. Classifying messages as unchanged, added, and removed
  • 2.8. External Tools Integration
    • 2.8.1. GNAT Warnings Integration
    • 2.8.2. GNATcheck Integration
    • 2.8.3. Libadalang Checkers Integration
  • 2.9. Partial Analysis
    • 2.9.1. Excluding Subprograms or Packages From Analysis
    • 2.9.2. Excluding Files From Analysis
    • 2.9.3. Excluding Directories From Analysis
    • 2.9.4. Excluding Projects From Analysis
  • 2.10. Source Annotations
• 3. How to View CodePeer Output
  • 3.1. Viewing CodePeer Output in GPS
    • 3.1.1. CodePeer Report Window
    • 3.1.2. Using the Locations View and Reviewing Messages
    • 3.1.3. Reviewing Messages
    • 3.1.4. Reviewing CodePeer Annotations
    • 3.1.5. Using the source editor’s tooltip to display values
    • 3.1.6. Source Navigation
    • 3.1.7. Accessing Results Remotely (IDE Server)
    • 3.1.8. Accessing Results Remotely (shared database)
    • 3.1.9. Copying Remote Results Locally
  • 3.2. HTML Output
    • 3.2.1. HTML generation
    • 3.2.2. Browser Requirements
    • 3.2.3. Location and Format of Output
    • 3.2.4. Running the CodePeer Web Server
    • 3.2.5. Message Review
  • 3.3. Viewing CodePeer Output in GNATbench
    • 3.3.1. CodePeer Problem Details View
    • 3.3.2. Reviewing CodePeer Messages in GNATbench
    • 3.3.3. CodePeer Annotation Details View
    • 3.3.4. Race Condition Details View
  • 3.4. Reviewing Messages
    • 3.4.1. Through CodePeer Web Server and HTML Output
    • 3.4.2. Through GPS and CodePeer IDE Server
    • 3.4.3. Through Pragma Annotate in Source Code
    • 3.4.4. Through a Shared Database
    • 3.4.5. Through a CSV File
    • 3.4.6. Improve Your Code Specification
    • 3.4.7. Exporting/Importing User Reviews
  • 3.5. Text Output
  • 3.6. Report File
  • 3.7. CSV Output
  • 3.8. Security Report
  • 3.9. Saving CodePeer Results in Configuration Management
• 4. Messages and Annotations
  • 4.1. Description of Messages
    • 4.1.1. Run-Time Checks
    • 4.1.2. User Checks
    • 4.1.3. Uninitialized and Invalid Variables
    • 4.1.4. Warning Messages
    • 4.1.5. Race Condition Messages
    • 4.1.6. Information Messages
    • 4.1.7. External Messages
    • 4.1.8. Listing All Message Kinds
  • 4.2. Description of Annotations
    • 4.2.1. Annotations
    • 4.2.2. Annotation Syntax
    • 4.2.3. Use Annotations for Code Reviews
  • 4.3. Filtering Messages
  • 4.4. Categorization of Messages
  • 4.5. Understanding the differences between preconditions and run-time errors
  • 4.6. Support for CWE
    • 4.6.1. CWE Categorization of Messages
    • 4.6.2. Support for CWE/SANS Top 25 Most Dangerous Software Errors
• 5. CodePeer Workflows
  • 5.1. Analyzing code locally prior to commit
  • 5.2. Nightly runs on a server
  • 5.3. Continuous runs on a server after each change
  • 5.4. Combined desktop/nightly run
  • 5.5. Combined continuous/nightly run
  • 5.6. Combined desktop/continuous/nightly run
  • 5.7. Software customization per project
  • 5.8. Compare local changes with master
  • 5.9. Multiple teams analyzing multiple subsystems
  • 5.10. Use CodePeer to generate a security report
• 6. CodePeer by Example
  • 6.1. Basic Examples
    • 6.1.1. Scalar Assignment
    • 6.1.2. Aggregate Assignment
    • 6.1.3. Branching
    • 6.1.4. Call Statement
  • 6.2. Loop Examples
    • 6.2.1. Induction Variables
    • 6.2.2. Array Scanning
    • 6.2.3. Array Increments
    • 6.2.4. Array Treatments
    • 6.2.5. Limitations
  • 6.3. Pointer Examples
    • 6.3.1. Dereference
    • 6.3.2. Aliasing
  • 6.4. Unknown Subprograms
• 7. Appendix
  • 7.1. Command Line Invocation
  • 7.2. -output-msg switches
  • 7.3. Advanced Command Line Options
  • 7.4. Return Codes
  • 7.5. CodePeer_Bridge Tool
  • 7.6. GPS Preferences
  • 7.7. Format of MessagePatterns.xml File
    • 7.7.1. Structure of the File
    • 7.7.2. Matching of rules
    • 7.7.3. Defining patterns
    • 7.7.4. Example
  • 7.8. How does CodePeer Work?
  • 7.9. What’s the Difference between CodePeer and SPARK?
  • 7.10. Directories and Files Produced by CodePeer
  • 7.11. CodePeer Messages and Compiler Warnings
  • 7.12. Partitioning of Analysis
  • 7.13. CodePeer Limitations and Heuristics
    • 7.13.1. Evaluation Order
    • 7.13.2. CodePeer Presumptions
    • 7.13.3. Handling of Generic Units
    • 7.13.4. Loop Unrolling
    • 7.13.5. Calls to Unknown Subprograms
    • 7.13.6. Skipped Subprograms or Files
    • 7.13.7. Call Too Complex
    • 7.13.8. Dispatching Calls and Access to Subprograms
    • 7.13.9. Null Array Bounds
    • 7.13.10. Handling of ‘Valid
  • 7.14. HTML Output (legacy)
    • 7.14.1. Browser Requirements
    • 7.14.2. Location and Format of Output
    • 7.14.3. Running the CodePeer Web Server
    • 7.14.4. Back and Forward Buttons
    • 7.14.5. Main Window
    • 7.14.6. Race Conditions Window
    • 7.14.7. Message History Window
    • 7.14.8. Message Status
    • 7.14.9. Message Category Table
    • 7.14.10. Source File Table
    • 7.14.11. Navigating to the Per-File Message Status Window
    • 7.14.12. Per-File Message Status Window/Editing Messages
    • 7.14.13. Edit Message Window (Provide Message Review)
    • 7.14.14. View Message Window (View Message Ranking)
    • 7.14.15. Annotations Report
• 8. GNU Free Documentation License