CodePeer User’s Guide

Copyright (C) 2009-2017, 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 Unix
    • 1.2.3. Installation under different locations
• 2. How to Run CodePeer
  • 2.1. System Requirements
  • 2.2. Basic Project File Set Up
    • 2.2.1. Basic Set Up
    • 2.2.2. Configuring IDEs to Drive Tools
    • 2.2.3. Simple Naming Scheme
    • 2.2.4. Ada Language Version
    • 2.2.5. 32bits Mode
    • 2.2.6. Representation Clauses
    • 2.2.7. Use of Predefined Ada Packages
    • 2.2.8. Use of Compiler Specific Packages
    • 2.2.9. Project Attributes
    • 2.2.10. Project File Example
  • 2.3. Advanced Project File Set Up
    • 2.3.1. Arbitrary Naming Scheme
    • 2.3.2. Target Configuration File
    • 2.3.3. Using the GNAT Target Runtime Directory
    • 2.3.4. Configuration of System Package (system.ads)
    • 2.3.5. Using Preprocessing
    • 2.3.6. Ignoring Pragmas
    • 2.3.7. Providing Stubs for Missing Generic Bodies
    • 2.3.8. Detection of Floating Point Overflow
    • 2.3.9. CodePeer Specific Project Settings
    • 2.3.10. Ignoring Source File Timestamp Mismatch
    • 2.3.11. Ignoring Exception Handlers
    • 2.3.12. Handling Enumeration Representation Clauses
  • 2.4. Running CodePeer
    • 2.4.1. Running CodePeer from the Command Line
    • 2.4.2. Running CodePeer from GPS
    • 2.4.3. Running CodePeer from GNATbench
    • 2.4.4. Running CodePeer from Jenkins
  • 2.5. Running CodePeer Faster
    • 2.5.1. Relevant Switches
    • 2.5.2. Disabling Analysis of Subprograms or Files
  • 2.6. Running CodePeer in Compiler Mode
  • 2.7. CodePeer Baselines
  • 2.8. Incremental Analysis via Persistent Annotations
  • 2.9. Integrating External tools
    • 2.9.1. Integrating GNAT Warnings
    • 2.9.2. Integrating GNATcheck
  • 2.10. Reducing the Number of False Alarms
  • 2.11. Partial Analysis
    • 2.11.1. Excluding Subprograms or Packages From Analysis
    • 2.11.2. Excluding Files From Analysis
    • 2.11.3. Excluding Directories From Analysis
    • 2.11.4. Excluding Projects From Analysis
  • 2.12. 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. Backtraces view
    • 3.1.6. Using the source editor’s tooltip to display values
    • 3.1.7. Source Navigation
  • 3.2. Viewing CodePeer Output in GNATbench
    • 3.2.1. CodePeer Problem Details View
    • 3.2.2. Reviewing CodePeer Messages in GNATbench
    • 3.2.3. CodePeer Annotation Details View
    • 3.2.4. Race Condition Details View
  • 3.3. HTML Output
    • 3.3.1. Browser Requirements
    • 3.3.2. Location and Format of Output
    • 3.3.3. Running the CodePeer Web Server
    • 3.3.4. Back and Forward Buttons
    • 3.3.5. Main Window
    • 3.3.6. Race Conditions Window
    • 3.3.7. Message History Window
    • 3.3.8. Message Status
    • 3.3.9. Message Category Table
    • 3.3.10. Source File Table
    • 3.3.11. Navigating to the Per-File Message Status Window
    • 3.3.12. Per-File Message Status Window/Editing Messages
    • 3.3.13. Edit Message Window (Provide Message Review)
    • 3.3.14. View Message Window (View Message Ranking)
    • 3.3.15. Annotations Report
  • 3.4. Text Output
  • 3.5. Report File
  • 3.6. CSV Output
• 4. How to Use CodePeer in a Team
  • 4.1. Possible Workflows
  • 4.2. Viewing CodePeer Results
    • 4.2.1. Accessing Results Remotely
    • 4.2.2. Copying Results Locally
  • 4.3. Reviewing Messages
    • 4.3.1. Through CodePeer Web Server and HTML Output
    • 4.3.2. Through a Shared Database and GPS or GNATbench Annotations
    • 4.3.3. Through a CSV File
    • 4.3.4. Through Pragma Annotate in Source Code
  • 4.4. Exporting/Importing Message Reviews
  • 4.5. Rerunning CodePeer Locally
    • 4.5.1. When Results Were Copied Locally
    • 4.5.2. When the Database Is on a Shared Drive
    • 4.5.3. When the Project File Is on a Shared Drive
  • 4.6. Saving CodePeer Results in Configuration Management
• 5. Messages and Annotations
  • 5.1. Description of Messages
    • 5.1.1. Run-Time Checks
    • 5.1.2. User Checks
    • 5.1.3. Uninitialized and Invalid Variables
    • 5.1.4. Warning Messages
    • 5.1.5. Race Condition Messages
    • 5.1.6. Information Messages
    • 5.1.7. External Messages
  • 5.2. Categorization of Messages
  • 5.3. Description of Annotations
  • 5.4. Understanding the differences between preconditions and run-time errors
  • 5.5. Support for CWE
    • 5.5.1. CWE Categorization of Messages
    • 5.5.2. Support for CWE/SANS Top 25 Most Dangerous Software Errors
• 6. CodePeer Usage Scenarios
  • 6.1. Initial setup
  • 6.2. Find Defects in Existing Code
    • 6.2.1. Start with the most simple analysis
    • 6.2.2. Analyze High / Medium messages
    • 6.2.3. Customize message ranking
    • 6.2.4. Add message review pragmas
    • 6.2.5. Improve your code specification
  • 6.3. Performing a Change Impact Analysis
    • 6.3.1. Running the First CodePeer Baseline
    • 6.3.2. Making the Change
    • 6.3.3. Viewing the Impact of the Change
    • 6.3.4. Fixing the Code in Case of Problems
  • 6.4. Use Annotations for Code Reviews
  • 6.5. Identify Possible Race Conditions
  • 6.6. Provide Evidence for Program Verification
• 7. CodePeer by Example
  • 7.1. Basic Examples
    • 7.1.1. Scalar Assignment
    • 7.1.2. Aggregate Assignment
    • 7.1.3. Branching
    • 7.1.4. Call Statement
  • 7.2. Loop Examples
    • 7.2.1. Induction Variables
    • 7.2.2. Array Scanning
    • 7.2.3. Array Increments
    • 7.2.4. Array Treatments
    • 7.2.5. Limitations
  • 7.3. Pointer Examples
    • 7.3.1. Dereference
    • 7.3.2. Aliasing
  • 7.4. Unknown Subprograms
• 8. Appendix
  • 8.1. Command Line Invocation
  • 8.2. Advanced Command Line Options
  • 8.3. Return Codes
  • 8.4. CodePeer_Bridge Tool
  • 8.5. GPS Preferences
  • 8.6. Format of MessagePatterns.xml File
    • 8.6.1. Structure of the File
    • 8.6.2. Matching of rules
    • 8.6.3. Defining patterns
    • 8.6.4. Example
  • 8.7. How does CodePeer Work?
  • 8.8. What’s the Difference between CodePeer and SPARK?
  • 8.9. Directories and Files Produced by CodePeer
  • 8.10. CodePeer Messages and Compiler Warnings
  • 8.11. Partitioning of Analysis
  • 8.12. CodePeer Limitations and Heuristics
    • 8.12.1. Evaluation Order
    • 8.12.2. CodePeer Presumptions
    • 8.12.3. Handling of Generic Units
    • 8.12.4. Loop Unrolling
    • 8.12.5. Calls to Unknown Subprograms
    • 8.12.6. Skipped Subprograms or Files
    • 8.12.7. Dispatching Calls and Access to Subprograms
    • 8.12.8. Null Array Bounds
    • 8.12.9. Time Limitations
• 9. GNU Free Documentation License