CodePeer User’s Guide¶
Copyright (C) 2009-2021, 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.3. System Requirements
- 1.4. Basic Project File Setup
- 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. Use of libraries installed with GNAT
- 1.5.9. Project Attributes
- 1.5.10. 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.2. Getting the Right CodePeer Settings
- 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.8. External Tools Integration
- 2.9. Partial Analysis
- 2.10. Source Annotations
- 3. How to View CodePeer Output
- 3.1. Viewing CodePeer Output in GNAT Studio
- 3.1.1. CodePeer Report Window
- 3.1.2. Using the Locations View
- 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.3. Viewing HTML Output in Jenkins
- 3.4. Viewing CodePeer Output in GNATbench
- 3.5. Reviewing Messages
- 3.5.1. Through CodePeer Web Server and HTML Output
- 3.5.2. Through GNAT Studio and CodePeer IDE Server
- 3.5.3. Through Pragma Annotate / Justification in Source Code
- 3.5.4. Through Pragma Annotate / Modified in Source Code
- 3.5.5. Through a Shared Database
- 3.5.6. Through a CSV File
- 3.5.7. Custom Review Status
- 3.5.8. Improve Your Code Specification
- 3.5.9. Exporting/Importing User Reviews
- 3.6. Text Output
- 3.7. Report File
- 3.8. CSV Output
- 3.9. Security Report
- 3.10. Saving CodePeer Results in Configuration Management
- 3.1. Viewing CodePeer Output in GNAT Studio
- 4. Messages and Annotations
- 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
- 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. GNAT Studio Preferences
- 7.7. Format of
MessagePatterns.xml
File - 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
- 8. GNU Free Documentation License