Polyspace for C/C++ Code Verification

View schedule and enroll

Course Details

This two-day, hands-on course discusses the use of Polyspace Bug Finder™ and Polyspace Code Prover™ to prove code correctness, improve software quality metrics, and ensure product integrity. The course is intended for engineers who develop software or models targeting embedded systems.

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 3

Polyspace Workflow Overview

Objective: Become familiar with Polyspace Bug Finder and Polyspace Code Prover and work through an introductory example.

Code verification workflows
Running a Bug Finder analysis
Running a Code Prover verification
Analyzing and fixing software problems

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.

Creating a Polyspace project
Common run-time environment artifacts
Handling processor-specific code
Setting target hardware information
Analyzing defects in Polyspace Bug Finder
Analyzing MISRA C rule violations
Measuring code metrics
Template projects

Analyzing Polyspace Code Prover Results

Objective: Become proficient at interpreting Polyspace Code Prover results.

Overview of abstract interpretation
Analyzing the call tree
Navigating through source code
Interpreting Polyspace Code Prover results
Viewing global variable usage in source code

Code Verification Checks

Objective: Find run-time errors using diagnostics available in Polyspace Code Prover.

Overview of C source code checks
Polyspace Code Prover run-time error checks
Relevant verification options

Day 2 of 3

Managing Polyspace Code Prover Verifications and Results

Objective: Handle verification results that contain large amounts of unproven checks.

Code Prover verification workflows
Controlling program execution sequence
Prioritizing orange run-time error checks

Adding Precision to Polyspace Code Prover Verifications

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
Automatic stubbing
Data range specification
Manual stubbing

Integration Analysis with Polyspace Access

Objective: Learn how to manage verification results with increasing code complexity using Polyspace Access™, and how to interpret and compare integrated analysis with robust analysis.

Post-submit workflows with Polyspace Access
Contextual verification
Detecting integration defects and run-time errors

Application Analysis

Objective: Review procedures and options that are useful when verifying complete applications.

Application software concerns
Analyzing concurrent data access issues
Replacing assembly or hardware functions
Handling third-party code in Polyspace
Creating documentation

Day 3 of 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

Appendix F: Integration Analysis with Polyspace Desktop

Objective: Learn how to manage verifications with increasing code complexity, and how to interpret and compare integrated analysis with robust analysis.

Contextual verification
Creating new modules
Detecting integration defects and run-time errors

Level: Intermediate

Prerequisites:

Strong knowledge of C or C++

Duration: 2 days

Languages: English, 中文, 日本語, 한국어