Customise Your Training
TechSource Systems is MathWorks Authorised Reseller and Training Partner
Polyspace for C/C++ Code Verification
Learn to analyze and verify C code for unsafe constructs, coding rule compliance, and run-time errors
Course
Highlights
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.
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
Who Should
Attend
Engineers who develop software and model for embedded system target.
Course
Prerequisites
Strong knowledge of C or C++
Course
Benefits
Upon the completion of this training, attendee will be able to:
- Verify a basic C file and view verification results
- Verify code that contains deviations from ANSI standard
- Set verification options that properly emulate the code’s target environment
- Analyze code verification results
- Create a stub for a missing function
- Restrict range of function inputs, missing function outputs, and global
variables for use in code verification - Identify verification options that affect specific types of verification checks
- Prioritize unproven verification results based upon severity and verification accuracy
- Use automated methods to review verification results.
- Analyze source code for MISRA-C violations
- Share verification results and justification with others
- Interpret code verification results properly when an automatically generated
main function is not used
Partners
Upcoming Program
- Please keep me posted on the next schedule
- Please contact me to arrange customized/ in-house training
Course Outline
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.
Measuring code metrics
- 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
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
Managing Polyspace Code Prover Verifications and Results
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
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
- Function stubbing
- Data range specification
- Manual stubbing
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