Polyspace for C/C++ Code Verification
Course Details
This two-day course discusses the use of Polyspace® Code Prover™ to prove code correctness, improve software quality metrics, and ensure product integrity. This hands-on course is intended for engineers who develop software or models targeting embedded systems. Note that day 3 is optional and is only available for private trainings
Topics include:
- Creating a verification project
- Reviewing and understanding verification results
- Emulating target execution environments
- Handling missing functions and data
- Managing unproven code (color-coded in orange by Polyspace products)
- Applying MISRA-C® rules
- Reporting analysis results
Day 1 of 2
Polyspace Workflow Overview
Objective: Become familiar with Polyspace Bug Finder and Polyspace Code Prover and work through an introductory example.
- Software development workflows with Polyspace
- Simple verification example
- Analyzing defects and run-time errors
Polyspace Bug Finder Analysis
Objective: Analyze code that may not be ANSI C compliant and account for the run-time environment, and correct defects and coding rule violations using Polyspace Bug Finder.
- Common run-time environment artifacts
- Handling processor-specific code
- Defining the execution context
- Setting target hardware information
- Analyzing and managing Polyspace Bug Finder defects
- Detecting coding rule violations
- Measuring code metrics
Analyzing Polyspace Code Prover Results
Objective: Become proficient at interpreting Polyspace Code Prover results.
- Overview of abstract interpretation
- Call tree analysis
- Source code navigation
- Execution paths
- Variable ranges
- Global variables
Code Verification Checks
Objective: Find run-time errors using diagnostics available in Polyspace Code Prover.
- Overview of C source code checks
- Location of checks in source code
- Description of checks
- Relevant verification options
Day 2 of 2
Managing Polyspace Code Prover Verifications and Results
Objective: Learn how Polyspace Code Prover treats missing code during verification, and how to affect this behavior to produce more meaningful verifications.
- Robustness verification and contextual verification
- Function stubbing
- Data range specification
- Manual stubbing
Adding Precision to Polyspace Code Prover Verifications
Objective: Handle verification results that contain large amounts of unproven checks.
- Determining verification effort
- Performing a quick review
- Performing a selective orange review
- Setting verification precision
- Prioritizing orange checks
- Reviewing orange checks
Integration Analysis
Objective: Learn how to manage verifications with increasing code complexity, and how to interpret and compare integrated analysis with robust analysis.
- Managing code modules
- Analyzing integration defects and rule violations with Polyspace Bug Finder and Polyspace Code Prover
- Importing comments
Application Analysis
Objective: Review procedures and options that are useful when verifying complete applications.
- Setting up an application verification
- Improving the results of an application verification
- Detecting concurrency issues
- Comparing robustness and contextual verification
- Creating documentation
Day 3 (optional, available with private training only)
Hands-On Instruction (Optional)
Objective: Spend time reviewing what you have learned and applying Polyspace directly to your own project. Potential topics include:
- Polyspace Bug Finder checks
- C++ code verification
- Tasking and shared data analysis
- Generated code verification
- Development process review
- Workflow integration
- Client/server software installation
- Polyspace configuration for project code
- Results interpretation
Level: Intermediate
Prerequisites:
- Strong knowledge of C or C++
Duration: 2 days
Languages: English, 日本語, 한국어, 中文
You can also select a web site from the following list:
Americas
- América Latina (Español)
- Canada (English)
- United States (English)
Europe
- Belgium (English)
- Denmark (English)
- Deutschland (Deutsch)
- España (Español)
- Finland (English)
- France (Français)
- Ireland (English)
- Italia (Italiano)
- Luxembourg (English)
- Netherlands (English)
- Norway (English)
- Österreich (Deutsch)
- Portugal (English)
- Sweden (English)
- Switzerland
- United Kingdom (English)
Asia Pacific
- Australia (English)
- India (English)
- New Zealand (English)
- 中国
- 日本Japanese (日本語)
- 한국Korean (한국어)