Polyspace
®
Products for C 8
Getting Started Guide
How to Contact MathWorks
www.mathworks.
comp.soft-sys.matlab Newsgroup
www.mathworks.com/contact_TS.html Technical Support
suggest@mathworks.com Product enhancement suggestions
bugs@mathwo
doc@mathworks.com Documentation error reports
service@mathworks.com Order status, license renewals, passcodes
info@mathwo
com
rks.com
rks.com
Web
Bug reports
Sales, prici
ng, and general information
508-647-7000 (Phone)
508-647-7001 (Fax)
The MathWorks, Inc.
3 Apple Hill Drive
Natick, MA 01760-2098
For contact information about worldwide offices, see the MathWorks Web site.
®
Polyspace
© COPYRIGHT 1997–2010 by The MathWorks, Inc.
The software desc ribed in this document is furnished under a license agreeme nt. The software may be used
or copied only under the terms of the license agreement. No part of this manual may be photocopied or
reproduced in any form without prior written consent from The MathWorks, Inc.
FEDERAL ACQUISITION: This provision applies to all acquisitions of the Program and Documentation
by, for, or through the federal government of the United States. By accepting delivery of the Program
or Docum entation, the government hereby agrees that this software or documentation qualifies as
commercial computer software or commercial computer software documentation as such terms are used
or defined in FAR 12.212, DFARS Part 227.72, and DFARS 252.227-7014. Accordingly, the terms and
conditions of this Agreement and only those rights specified in this Agreement, shall pertain to and govern
theuse,modification,reproduction,release,performance,display,anddisclosureoftheProgramand
Documentation by the federal government (or other entity acquiring for or through the federal governme nt)
and shall supersede any conflicti ng contractual terms or conditions. If this License fails to meet the
government’s needs or is inconsistent in any respect with federal procurement law, the government agrees
to return the Program and Documentation, unused , to The MathWorks, Inc.
Trademarks
MATLAB and Simulink are registered trademarks of The M athWorks, Inc. See
www.mathworks.com/trademarks for a list of additional trademarks. Other product or brand
names may be trademarks or registered trademarks of their respective holders.
Patents
MathWorks products are protected by one or more U.S. patents. Please see
www.mathworks.com/patents for more information.
Products for C Getting Started Guide
Revision History
March 2008 First printing Revised for Version 5.1 (Release 2008a)
October 2008 Second printing Revised for Version 6.0 (Release 2008b)
March 2009 Third printing Revised for Version 7.0 (Release 2009a)
September 2009 O nline only Revised for Version 7.1 (Release 2009b)
March 2010 Online only Revised for Version 7.2 (Release 2010a)
September 2010 Fourth Printing Revised for Version 8.0 (Release 2010b)
Introduction to Polyspace Products for
Verifying C Code
1
Product Overview ................................. 1-2
Overview of Polyspace Verificat ion
The Value of Polyspace Verification
................... 1-2
................... 1-2
Contents
Product Components
Polyspace Products for C
Polyspace Verification En vi r onment
Other Polyspace Components
Installing Polyspace Products
Finding the Installation Instructions
Obtaining L icenses for Polyspace
Polyspace
Working with Polyspace Software
Basic Workflow
Tutorials in This Guide
Additional Information and Support
Product Help
MathWorks Online
Related Products
Polyspace Products for Verifying C++ Code
Polyspace Products for Verifying Ada Code
Polyspace Products for Linking to Models
®
Server for C/C++ ...................... 1-11
..................................... 1-15
.............................. 1-5
........................... 1-5
........................ 1-9
...................... 1-11
®
Client for C/C++ and
................................... 1-12
............................. 1-13
................................ 1-15
.................................. 1-16
.................. 1-5
................. 1-11
................... 1-12
................ 1-15
............ 1-16
............. 1-16
.............. 1-16
v
Setting Up a Polyspace Project
2
About Setting Up a Project Tutorial ................. 2-2
Overview
Example Files
........................................ 2-2
.................................... 2-2
Creating a New Project
What Is a Project?
Preparing Project Folders
Opening Polyspace Verification Environment
Creating a New Project to Verify the Example C File
............................ 2-3
................................. 2-3
........................... 2-3
........... 2-4
Running a Verification
3
About Running a Verification Tutorial .............. 3-2
Overview
Before You Start
Preparing for Verification
Opening the Project
Specifying Source Files to Verify
Launching Server Verification from Project
Manager
Starting the Verification
Monitoring Progress of the Verification
Removing Verification Results from the Server
Troubleshooting a Failed Verification
........................................ 3-2
.................................. 3-3
.......................... 3-4
................................ 3-4
..................... 3-4
........................................ 3-6
............................ 3-6
................ 3-7
......... 3-13
................. 3-15
.... 2-7
vi Contents
Using Polysp a ce In One Clic k to Launch V erification
Overview of Polyspace In One Click
Setting the Active Project
Sending Files to Polyspace Software
........................... 3-18
................... 3-18
.................. 3-20
.. 3-18
Launching Client Verification from Project
Manager
Starting the Verification
Monitoring the Progress of the Verification
Completing Verification
Stopping the Verification Before It is Complete
........................................ 3-25
............................ 3-25
............ 3-26
............................ 3-28
......... 3-28
Reviewing Verification Results
4
About Reviewing Verification Results Tutorial ....... 4-2
Overview
Before You Start
........................................ 4-2
.................................. 4-2
Opening Verification Results
Opening Run-Time Checks Perspective
Opening Verification Res ults
Exploring Run-Time Checks Perspective
Overview
Reviewing the Run-Time Checks Pane
Reviewing Results in Expert Mode
What Is Expert Mode?
Switching to Expert Mode
Reviewing Checks in Expert Mode
Reviewing Additional E xamples of Checks
Filtering Checks
Reviewing Results in Assistant Mode
What Is Assistant Mode?
Switching to Assistant Mode
Selecting the Methodology and Criterion Level
Exploring Methodology for C
Reviewing Checks
Defining a Custom Methodology
........................................ 4-4
............................. 4-8
.................................. 4-19
................................. 4-26
....................... 4-3
................ 4-3
........................ 4-3
................ 4-6
.................. 4-8
.......................... 4-8
.................... 4-8
................ 4-23
........................... 4-23
........................ 4-23
........................ 4-24
..................... 4-28
............ 4-4
............. 4-14
......... 4-24
Automatically Testing Unproven Code
.............. 4-30
vii
Generating Reports of Verification Results .......... 4-31
Polyspace Report Generator Overview
Generating Report for
example.c .................... 4-32
................ 4-31
Checking MISRA C Compliance
5
About Checking MISRA C Compliance Tutorial ...... 5-2
Overview
Before You Start
........................................ 5-2
.................................. 5-2
Setting Up MISRA C Checking
Opening Your Example Project
Creating New Verification
SettingMISRACCheckingOption
Creating a MISRA C Rules File
Excluding Files from the MISRA C Checking
Configuring Text and XML Editors
Saving the Project
Running a Verification with MISRA C Checking
Starting the Verification
Examining MISRA C Violations
Opening MISRA-C Report
................................. 5-12
............................ 5-13
...................... 5-3
...................... 5-3
.......................... 5-3
................... 5-6
...................... 5-7
........... 5-10
................... 5-11
...................... 5-14
.......................... 5-18
...... 5-13
Index
viii Contents
Introduction to Polyspace
Products for Verifying C
Code
• “Product Overview” on page 1-2
• “Product Components” on page 1-5
• “Installing Polyspace Products” on page 1-11
1
• “Working with Polyspace Software” on page 1-12
• “Additional Information and Support” on page 1-15
• “Related Products” on page 1-16
1 Introduction to Polyspace
®
Product Overview
Overview of Polyspace Verification
Polyspace®products verify C, C++, and Ada code by detecting run-time errors
before code is compiled and executed. P olyspace verifica t ion uses formal
methods not only to detect errors, but to prove mathem atically that certain
classes of run-time errors do not exist.
To verify the source code, you set up verification parameters in a project, run
the verification, and review the results. A graphical user interface helps you
to efficiently review verification results. Results are color-coded:
Products for Verifying C Code
In this section...
“Overview of Polyspace Verification” on page 1-2
“The Value of Polyspace Verification” on page 1-2
• Green – Indicates code that never has an error.
• Red – Indicates code that always has an error.
• Gray – Indicates unreachable code.
• Orange – Indicates unproven code (code that might have an error).
The color-coding helps you to quickly identify errors and find the exact
location of an error in the source code. After you fix errors, you can easily run
the verification again.
The Value of Polyspace Verification
Polyspace verification can help you to:
• “Ensure Software Reliability” on page 1-3
• “Decrease Development Time” on page 1-3
• “Improve the Development Process” on page 1-4
1-2
Product Overview
Ensure Software Reliability
Polyspace software ensures the reliability of your C applications by proving
code correctness and identifying run-time errors. Using advanced verification
techniques, Polyspace software performs an exhaustive verification of your
source code.
Because Polyspace software verifies all possible executions of your code, it
can identify code that:
• Never has an error
• Always has an error
• Is unreachable
• Might have an error
With this inform a t ion, you know how much of your code is free of run-time
errors, and you can improve the reliability of your code by fixing errors.
You can also improve the quality o f your code by using Polyspace verification
software to check that your code complies with MISRA C
®
standards.
Decrease Development Time
Polyspace software reduces developmenttimebyautomatingtheverification
process and helping you to efficiently review verification results. You can use
it at any point in the development process. However, using it during early
coding phases allows you to find errors when it is less costly to fix them.
YouusePolyspacesoftwaretoverifyCsource code before compile tim e. To
verify the source code, you set up verification parameters in a project, run
the verification, and review the results. This process take s significantly less
time than using manual methods or using tools that require you to modify
code or run test cases.
Color-coding of results helps you to quickly identify errors. You will spend
less time debugging because you can see the exact location of an error in the
source code. After you fix errors, you can easily run the verification again.
ISRA and MISRA C are registered trademarks of MISRA Ltd., held on behalf of the
1.M
MISRA Consortium.
1
1-3
1 Introduction to Polyspace
®
Products for Verifying C Code
Using Polyspace verification software helps you to use your time effectively.
Because you know which parts of your code are error-free, you can focus on
thecodethathasdefiniteerrors or might have errors.
Reviewing code that might have errors (orange code) can be time-consuming,
but Polyspace software helps you with the review process. You can use filters
to focus on certain types of errors or you can allow the software to identify the
code that you should review.
Improve the Development Process
Polyspace softwa r e makes it easy to share verification parameters and
results, allowing the development team to work together to improve product
reliability. Once verification parameters have been set up, developers can
reuse them for other files in the same application.
Polyspace verific ati on software supports code verification t h r oughout the
development process:
1-4
• An individual develo per can find and fix run-time errors during the initial
coding phase.
• Quality assurance engineers can check overall reliability of an application.
• Managers can monitor application reliability by generating reports from
the verification results.
Product Components
In this section...
“Polyspace Products for C” on page 1-5
“Polyspace Verification Environment” on page 1-5
“Other Polyspace Components” on page 1-9
Polyspace Products for C
The Polyspace products for verifying C code are combined with the Polyspace
products for verifying C++ code. These products are:
Product Components
• Polyspace
• Polyspace
Polyspace Client for C/C++ software is the management and visualization tool
of Polyspace products. You use it to submit jobs for execution by the Polyspace
Server, and to review verification results.
Polyspace Server for C/C++ software is the computational engine of Polyspace
products. You use it to run jobs posted by Polyspace clients, and to manage
multiple servers and queues.
®
Client™ for C/C++
®
Server™ for C/C++
Polyspace Verification Environment
The Polyspace verification environment (PVE) is the graphical user interface
of the Polyspace Client for C/C++ software. You use the Polyspace verification
environment to create Polyspace projects, launch verifications, and review
verification results.
The Polyspace verification environment consists of three perspectives:
• “Project Manager P erspective” on page 1-6
• “Coding Rules Perspective” on page 1-7
• “Run-Time Checks Perspective” on page 1-8
1-5
1 Introduction to Polyspace
®
Products for Verifying C Code
Project Manager Perspective
The Project Manager perspective allows you to create projects, set verification
parameters, and launch verifications.
Specify source files
and include folders
Specify
analysis options
1-6
Monitor progress and view logs
Product Components
You use the P roject Manager perspective in the tutorial in Chapter 2, “Setting
Up a Polyspace Project”.
Coding Rules Perspective
The Coding Rules perspective allows you to review results from the Polyspace
coding rules checker, to ensure compliance with established coding standards.
You use the Coding Rules perspective in the tutorial in Chapter 5, “Checking
MISRA C Compliance”.
1-7
1 Introduction to Polyspace
®
Products for Verifying C Code
Run-Time Checks Perspective
The Run-Time Checks perspective allows you to review verification results,
comment individual checks, and track review progress.
Coding review progress viewSelected check view
1-8
Procedural
entities view
Source code
view
Variables
view
Call tree
view
Product Components
YouusetheRun-TimeChecksperspectiveinthetutorialinChapter4,
“Reviewing Verification Results”.
Other Polyspace Components
In addition to the Polyspace verification environment, Polyspace products
provide several other components to manage verifications, improve
productivity, and track software quality. These components include:
• Polyspace Queue Manager Interface (Spooler)
• Polyspace in One Click
• Polyspace Metrics Web Interface
Polyspace Queue Manager Interface (Polyspace Spooler)
The Polyspace Queue Manager (also called the Polyspace Spooler) is the
graphical user interface of the Polyspace Server for C/C++ software. You
use the Polyspace Queue Manager Interface to move jobs within the queue,
remove jobs, m onitor the progress of individual ver if ications, and download
results.
You use the Polyspace Queue Manager in the tutorial “Launching Server
Verification from Project Manager” on page 3-6.
1-9
1 Introduction to Polyspace
®
Products for Verifying C Code
Polyspace in One Click
Polyspace in One Click is a convenie n t way to verify multip le files using the
same set of options.
After creating a project with the options that you want, you can use Polyspace
in One Click to designate that p roject as the active project, and then send
source files to Polyspace software for verification with a single mouse click.
YouusePolyspaceinOneClickinthetutorial“UsingPolyspaceInOneClick
to Launch Verification” on page 3-18.
Polyspace Metrics Web Interface
Polyspace Metrics is a web-based tool for software development managers,
quality assurance engineers, and software developers. Polyspace M etrics
allows you to evaluate software quality metrics, and monitor changes in code
metrics, coding rule violations, and run-time checks through the lifecycle
of a project.
1-10
For information on using Polyspace Metrics, see “Software Quality with
Polyspace Metrics”in the Polyspace Products for C User’s Guide.
Installing Polyspace Products
In this section...
“Finding the Installation Instructions” on page 1-11
“Obtaining Licenses for Polyspace®Client for C/C++ and Polyspace®Server
for C/C++” on page 1-11
Finding the Installation Instructions
The tutorials in this gu ide require Polyspace Client for C/C++ and Polyspace
Server for C/C++. Instructions for installing Polyspace products are in the
Polyspace Installat ion Guide. Be fore installing Polyspace products, you must
obtain the necessary licenses.
Obtaining Licenses for Polyspace Client for C/C++
and Polyspace Ser ver for C/C++
For information about obtaining licenses for Polyspace products, see
“Polyspace License Installation” in the Polyspace Installation Guide.
Installing Polyspace®Products
1-11
1 Introduction to Polyspace
®
Products for Verifying C Code
WorkingwithPolyspaceSoftware
In this section...
“Basic Workflow” on page 1-12
“Tutorials in This Guide” on page 1-13
Basic Workflow
The following graphic shows the basic workflow for using Polyspace software
to verify C source code.
1
Set up project
2
Verify code
1-12
3
Review verification results
In this workflow, you:
1 Use the Project Manager perspective to set up a project file.
2 Verify code on a server or client.
YoucanusetheProjectManagerperspectivetostarttheverificationor
you can select files from a Microsoft
®
Windows®folder and send them to
Polyspacesoftwareforverification. For verifications that run on a server,
you use the PolySpace Queue Manager Interface (PolySpace Spooler) to
Workin g with Pol y spa c e®Software
manage the verification and download the results to a client. You can set an
option to check MISRA C compliance in the first stage of the verification.
3 Use the Run-Time Check s p erspective to review verification resul ts.
TutorialsinThisGuide
The tutorials guide you through the basic workflow, including the different
options for running verifications. The following graphic shows the workflow
youfollowinthesetutorials.
1
Create new project
2
Verify code
3
Review verification results
2
4
Check MISRA C compliance
In this workflow, you:
1 Create a new project that you use for the workflow.
This step is in the tutorial in Chapter 2, “Setting Up a Polyspace Project”.
2 Verify a single C file.
ISRA and MISRA C are registered trademarks of MISRA Ltd., held on behalf of the
2.M
MISRA Consortium.
1-13
1 Introduction to Polyspace
®
Products for Verifying C Code
This step is in the tutorial in Chapter 3, “Running a Verification”. In this
tutorial, you verify the same file using three different methods of running a
verification:
• Start a verification that runs on a server using the Project Manager
perspective.
• Send files to a server for verification using Polyspace In One Click.
• Start a verification that runs on a client using the Project Manager
perspective.
3 Review the verification results.
This step is in the tutorial in Chapter 4, “Reviewi ng V erification R esults”.
4 Modify the project to include MISRA C checking and review the MISRA C
violations i n the example file.
This step is in the tutorial in Chapter 5, “Checking MISRA C Compliance”.
1-14
Additional Information and Support
In this section...
“Product Help” on page 1-15
“MathWorks Online” on page 1-15
Product Help
To access Polyspace online H elp, select Help > Help .
To access the online documentation for Polyspace products, go to:
/www.mathworks.com/access/helpdesk/help/toolbox/polyspace/polyspace.html
MathWorks Online
For additional information and support, go to:
Additional Information and Support
www.mathworks.com/products/polyspace
1-15
1 Introduction to Polyspace
Related Products
®
Products for Verifying C Code
In this section...
“Polyspace Products for Verifying C++ Code” on page 1-16
“Polyspace Products for Verifying Ada Code” on page 1-16
“Polyspace Products for Linking to Models” on page 1-16
Polyspace Products for Verifying C++ Code
For information about Polyspace products that verify C++ code, go to:
http://www.mathworks.com/products/polyspaceclientc/
http://www.mathworks.com/products/polyspaceserverc/
Polyspace Products for Verifying Ada Code
For information about Polyspace products that verify A da code, go to:
1-16
http://www.mathworks.com/products/polyspaceclientada/
http://www.mathworks.com/products/polyspaceserverada/
Polyspace Products for Linking to Models
For information about Polyspace products that link to models, g o to:
http://www.mathworks.com/products/polyspacemodelsl/
http://www.mathworks.com/products/polyspaceumlrh/
Setting Up a Polyspace
Project
• “About Setting Up a Project Tutorial” on page 2-2
• “Creating a New Project” on page 2-3
2
2 Setting Up a Polyspace Project
About Setting Up a Project Tutorial
In this section...
“Overview” on page 2-2
“Example Files” on page 2-2
Overview
You must have a project before you can run a Polyspace verification of your
source code. In this tutorial, you create the project that you use to run
verifications in later tutorials.
Example Files
This tutorial uses the source file example.c that comes with the installation.
You learn more about the files and folders required for this tutorial in
“Preparing Project Folders” on page 2-3.
2-2
Creating a New Project
In this section...
“What Is a Project?” on page 2-3
“Preparing Project Folders” on page 2-3
“Opening Polyspace Verification Environment” on page 2-4
“Creating a New Project to Verify the Example C File” on page 2-7
What Is a Project?
In Polyspace software, a project is a named set of parameters for verification
of your software project’s source files. A project includes:
• Source files
• Include f olders
• One or more configurations, specifying a set of analysis options
Creating a New Project
• One or more verifications, each of which include:
- Source (specific versions of source files used in the verification)
- Configuration (specific set of analysis options used for the verification)
- Verification results
You can create your own project or use an existing project. You create and
modify a project using the Project Manager perspective.
In this tutorial, you create a new project and save it as a configuration file
(
.cfg).
Preparing Project Folders
Before you start verifying a C file with Polyspace software, you must know
the locations of the C source file and the include files. You must also know
where you want to store the verification results.
2-3
2 Setting Up a Polyspace Project
For each project, you decide where to store source files and results. For
example, you can create a project folder, and then in that folder, create
separate folders for the source files, include files, and results.
For this tutorial, prepare a project folder as follows:
1 Create a project folder named polyspace_project.
2 Open polyspace_project, and create the following folders:
•
• includes
3 Copy the file example. c from
PolySpace_Install\Examples\Demo_C_Single-File\sources
to
polyspace_project\sources
sources
2-4
PolySpace_Install
4 Copy the files include.h and math.h from
PolySpace_Install\Examples\Demo_C_Single-File\sources
is the installation folder.
to
polyspace_project\includes.
Opening Polyspace Verification Environment
You use the Polyspace verification environment to create projects, start
verifications, and review verificatio n results.
To open the Polys pace verification environment:
1 Double-click the Polyspace icon.
Creating a New Project
2 If you have only Polyspace Client for C/C++ software installed on your
computer, skip this step. If you have both Polyspace Client for C/C++ and
Polyspace Client for Ada products on your system , the Polyspace Language
Selection dialog box opens.
3 Select Polyspace for C/C++ and click OK.
The Polyspace Verification Environment opens.
2-5
2 Setting Up a Polyspace Project
Specify source files
and include folders
Specify
analysis options
2-6
Monitor progress and view logs
By default, the Polyspace Verification Environment displays the Project
Manager perspective. The Project M anage r perspective has three main panes.
Creating a New Project
Use this
section...
Project Browser
(upper-left)
Configuration
(upper-right)
Output
(lower-right)
You can resize or hide any of these panes. You learn more about the Project
Manager perspective later in this tutorial.
For...
Specifying:
• Source files
• Include folders
• Results folder
Specifying analysis options
Monitoring the progress of a verification, and view ing
status, log messages, and general verification statistics.
Creating a New Project to Verify the Example C File
Youmusthaveaproject,savedwithfiletypecfg, to run a verification. In this
part of the tutorial, you create a new project for verifying
You create a new p roject by:
example.c.
• “Opening a New Project” on page 2-7
• “Specifying Source Files and Include Folders” on page 2-9
• “Specifying Analysis Options” o n page 2-11
• “Saving the Project” on page 2-12
Opening a New Project
To open a new project for verifying example.c:
1 Select File > New Project.
The PolySpace Project – Properties dialog box opens:
2-7
2 Setting Up a Polyspace Project
2-8
2 In the Project name field, enter example_project.
3 Clear the Default location check box.
Note Clearing the Default location check box allows you to specify
the location of y our project files. In this tutorial, you change the default
location to the project folder that you created in “Preparing Project Folders”
on page 2-3. Changing the default location makes it easier to specify source
files and include folders.
4 In the Location field, enter or navigate to the project folder that you
created earlier.
his example, the project folder is
In t
C:\PolySpace\polyspace_project.
5 In the Project language section, select C.
6 Click Finish.
The
example_project opens in the PolySpace verification environment.
Creating a New Project
Specifying Source Files and Include Folders
To specify the source files an d include folders for the verification of example.c:
2-9
2 Setting Up a Polyspace Project
1 In the Project Brow ser, select the Source folder.
2 Click the Add source icon in the upper left the Project Browser.
The PolySpace P
opens.
roject – Add Source Files and Include Folders dialog box
2-10
3 The project folder polyspace_project should appear in Look in.Ifitdoes
not, navigate to that folder.
4 Select the sources folder, then click Add Source.
example.c file appears in the Source tree for example_project.
The
5 Select the includes folder, then click Add Include.
The
includes folder appears in the Include tree for example _pro ject.
Creating a New Project
Note In addition to the include folders you specify, Polyspace software
automatically adds the standard include folders to your project:
•
PolySpace_Install/Verifier/include/include-gnu
• PolySpace_Install/Verifier/include/include-gnu/next
6 Click Finish to apply the changes and close the dialog box.
The Project Browser now looks like the following graphic.
ifying Analysis Options
Spec
The analysis options in the upper-right section of the Project Manager
perspective include parameters that Polyspacesoftwareusesduringthe
verification process. For more information about analysis options, see
“Options Description” in the Polyspace Products for C Reference.
To specify the analysis options for this tutorial:
1 Expand the Target/Compilation section.
2-11
2 Setting Up a Polyspace Project
2 In the Operating system target for PolySpace stubs drop-down list, select
no-predefined-OS.
3 Keep the default values for all other options.
The analysis options now looks like the followin g graphic.
2-12
ng the Project
Savi
To save the project, select File > Save.
PolySpace software saves your project using the Project name and Location
you specified when creating the project.
Running a Verification
• “About Running a Verification Tutorial” on page 3-2
• “Preparing for Verification” on page 3 -4
• “Launching Server Verification from Project Manag er” on page 3-6
• “Using Polyspace In One Click to Launch Verification” on page 3-18
• “Launching Client Verification from Project Manager” on page 3-25
3
3 Running a Verification
About Running a Verification Tutorial
In this section...
“Overview” on page 3-2
“Before You Start” on pag e 3-3
Overview
Once you have created the project example.cfg, as described in “Creating a
New Project” on page 2-3, you can run the verification.
You can run a verification on a server or a client.
Use... For...
Server • Best performance
• Large files (more than 800 lines of code, including comments)
3-2
• Multitasking
Client • Analternativetotheserverwhentheserverisbusy
• Small files with no multitasking
Note Verification on a client takes more time. You might
not be able to use your client computer when a verification is
running on it.
You can start a verification using either the Project Manager or Polyspace In
One Click. With either method, the verification can run on a server or a client.
Use... For...
About Running a Verification Tutorial
Project Manager
Polyspace In One Click A convenient w a y to start the verification of
In this tutorial, you learn how to run a verification on a s erve r and on a client,
and how to start a verification using the Project Manager and Polyspace In
One Click. You verify the file
each time. You use:
• Project Manager to start a verification that runs on a server.
• Polyspace In One Click to start a verification tha t runs on a server.
• Project Manager to start a verification that runs on a client.
A basic way to start a verif ica t ion.
You specify the source files in the project file.
With the project open, you click a button to start
the verification.
several files which use the same verification
options.
Once you specify the project file containing the
verification options, you s pecify the source files
by selecting them from a Microsoft Windows
folder. You start the verification by sending the
selected files to Polyspace software.
example.c three times using a different method
Each verification stores the same results in your project. You review these
results in the tutorial Chap ter 4, “Reviewing Verification R esu lts”.
Before You Start
Before you start this tutorial, you must complete Chapter 2, “Setting Up a
Polyspace Project”. You use the folders and project file,
that tutorial.
example.cfg,from
3-3
3 Running a Verification
Preparing for Verification
In this section...
“Opening the Project” on page 3-4
“Specifying Source Files to Verify” on page 3-4
Opening the Project
To run a verification, you must have an open project file. For this tutorial, you
use the project file
Polyspace Project”. If
example.cfg that you created in Chapter 2, “Setting Up a
example_project.cfg is not already open, open it.
To open
1 If the Polyspace softw are is not already open, open it.
2 Select File > O pen Project.
3 In the Look in drop-down list box, navigate to polyspace_project.
4 Select example_project.cfg.
5 Click Open to open the f ile and close the dialo g box.
example_project.cfg:
The Open a PolySpace project file dialog box opens.
Specifying Source Files to Verify
Each Polyspace project can contain multiple verifications. Each of these
verifications can analyze a specific set of source files using a specific set of
analysis options.
Therefore, before you launch a verification, you must specify which files in
your project that you want to verify. In the
there is only one file to verify.
To copy source files to a verification:
example_project in this tutorial,
3-4
1 In the Project Browser Source tree, right click example.c.
2 Select Copy Source File to > Verification_(1).
The
example.c file appears in the Source tree of Verificat ion_ (1).
Preparing for Verification
3-5
3 Running a Verification
Launching Server Verification from Project Manager
In this section...
“Starting the Verification” on page 3-6
“Monitoring Progress of the Verification” on page 3-7
“Removing Verification Results from the Server” on page 3-13
“Troubleshooting a Failed Verification” on page 3-15
Starting the Verification
In this part of the tutorial, you run the verification on a server.
To start a verification that runs on a server:
1 Select the Send to PolySpace Server check b ox in the General Analysis
options.
3-6
2 Click the Run button on the Project Manager toolbar.
Note If you see the message Verification process failed,clickOK
and go to “Troubleshooting a Failed Verification” on page 3-15.
Launching Server Verification from Pro ject Manager
The verification has three main phases:
a Checking syntax and semantics (the compile phase). Because Polyspace
software is independent of any particular C compiler, it ensures tha t
your code is portable, maintainable, and complies with ANSI
b Generating a main if the Polyspace software does not find a main and
®
standards.
you have selected the Generate a Main option. For more information
about generating a main, see “MAIN GENERATOR OPTIONS
(-main-generator) for Polyspace Software” in the Polyspace Products
for C Reference.
c A n alyzing the code for run-time errors and generating color-coded
results.
Thecompilephaseoftheverificationruns on the client. When the compile
phase is complete:
• You see the message
queued on server at the bottom of the Project
Manager persp ective . This messa ge indicates that the part of the
verification that takes place on the client is complete. The rest of the
verification runs on the server.
• A message in the Output Summary window gives you the identification
number (Analysis ID) for the verification. For this verification, the
identification number is
3 For information on any message in the log, click the message.
1.
Monitoring Progress of the Verification
Therearetwowaystomonitortheprogressofaverification:
3-7
3 Running a Verification
• Using the Project Manager – allows you to follow the progress of the
verifications you submitted to the server, as well as client verifications.
• Using the Queue Manager (Spooler) – allows you to follow the progress
of any verification job in the server queue.
Monitoring Progress Using Project Manager
You can monitor the progress of your verification by viewing the progress
monitor and logs at the bottom of the Project Manager perspective.
3-8
Theprogressmonitorhighlightsthecurrentphaseinblueanddisplaysthe
amount of time and completion percentage for that phase.
The logs report additional information about the progre ss of the verification.
To view a log, click the button for that log. The information appears in the
log display area at the bottom of the Project Manager window. Follow the
next steps to view the logs:
1 Click the Output Summary tab to display co mpile phase messages and
errors. You can search the log by entering search terms in the Search in
the log box and clicking the left arrows to search backward or the right
arrows to search forward.
2 Click the Verification Statistics tab to display statistics, such as analysis
options, stubbed functions, and the verification checks performed.
ck the Refresh button
3 Cli
ogresses.
pr
to update the display as the verification
Launching Server Verification from Pro ject Manager
4 Click the Full Log tab to display messages, errors, and statistics for all
phases of the verification.
Note You can search the logs. In the Search in the log box, enter a
search term and click the left arrows to search backward or the right
arrows to search forward.
Monitoring Progress Using Queue Manager
You monitor the progress of the verification using the Polyspace Queue
Manager (also called the Spooler).
To monitor the verification of
1 Double-click the P o lySpace Spooler icon on the d esktop.
Example_Project:
The PolySpace Queue M anager Interface opens.
3-9
3 Running a Verification
Tip You can also open the Polyspace Queue Manager Interface by
clicking the Polyspace Queue Manager icon
perspective toolbar.
2 Point anywhere in t he row for ID 1.
3 Right-click to open the context menu for this verification.
4 Select View log file.
Awind
ow opens displaying the last one-hundred lines of the verification.
on the Run-Time Checks
3-10
Launching Server Verification from Pro ject Manager
5 Click Close to close the window.
6 Select Follow Progress from the context menu.
rogress Monitor opens.
The P
3-11
3 Running a Verification
3-12
You can m
bar and
highli
comple
The logs report additional information about the progress of the verification.
To view a log, click the button for that log. The information appears in the
log display area at the bottom of the Project Manager window. Follow the
next steps to view the logs:
• Click the Output Summary tab to display com pile phase m essage s and
errors. You can search the log by entering search terms in the Search
in the log box and clicking the left arrows to search backward or the
right arrows to search forward.
• Click the Verification Statistics tab to display statistics, such
as analysis options, stubbed functions, and the verification checks
performed.
onitor the progress of the verification by watching the progress
viewing the logs at the bottom of the window. T he progress monitor
ghts the current phase in blue and displays the amount of time and
tion percentage for that phase.
Launching Server Verification from Pro ject Manager
• Click the Refresh button to update the display as the verification
progresses.
• Click the Full Log tab to display messages, errors, and statistics for all
phases of the verification.
Note You can search the logs. In the Search in the log box, en ter a
search term and click the left arrows to search backw ard or the right
arrows to search forward.
7 Select File > Quit to close the progress window.
8 Wait for the verification to finish.
When the verification is complete, the status in the PolySpace Queue
Manager Interface changes from
running to completed.
Removing Verification Results from the Server
At the end of a server verification, the server autom ati c ally down loads
verification results to the res ults folder specified in the project. You do not
need to manually download your results.
3-13
3 Running a Verification
Note You can manually download verification results to another location on
your client system, or to other client systems.
Verification results remain on the se rver until you remove them. Once your
results have been downloaded to the client, you can remove them from the
server queue.
To remove your results from the server:
1 In the PolySpace Queue Manager Interface, right-click the verification,
and select Remove From Queue.
A dialog box opens to confirm that youwanttoremovetheverification
from the queue.
3-14
2 Click Yes.
Note To download the results and remove the verification from the queue,
right-click the verification and select Download Results And Remove
From Queue. If you download results before the verification is complete,
you get partial results and the verification continues.
3 Select Operations > Exit to close the PolySpace Queue Manag er Interface.
Once the results are on your client, you can review them using the Run-Time
Checks perspective. You re view results from the verification in Chapter 4,
“Reviewing Verification Results”.
Launching Server Verification from Pro ject Manager
Troubleshooting a Failed Verification
When you see a message that the verification failed, it indicates that
Polyspace software could not perform the verification. The following sections
present some possible reasons for a failed verification.
Hardware Does Not Meet Requirements
If your computer does not have the minimum hardware requirements. the
verification fails. For information about the hardware requirements, go to:
www.mathworks.com/products/polyspaceclientc/requirements.html.
To determine if this is the cause of the failed verification, search the log for
the message:
Errors f ound when verifying host configuration.
You can:
• Upgrade your computer to meet the minimal requirements.
• In the General section of the Analysis options, select the Continue with
current configuration option and run the verification again.
You Did Not Specify the Location of Include Files
If you se e a message in the log, such as the following, either the files are
missing or you did not specify the location of include files.
include.h: No such file or folder
For information on how to specify the location of include files, see “Creating a
New Project to Verify the Example C F ile” on page 2-7.
Polyspace Software Cannot Find the Server
Ifyouseethefollowingmessageinthelog,Polyspacesoftwarecannotfind
the server.
Error: Unknown host :
3-15
3 Running a Verification
Polyspace software uses information in the preferences to locate the server.
To find the server information in the preferences:
1 Select Options > Preferences.
2 Select the Serv er Configuration tab.
3-16
Launching Server Verification from Pro ject Manager
By default, Polyspace software automatically finds the server. You can
specify the server by selecting Use the following server and port and
providing the server name and port. For information about setting up a
server, see the Polyspace Installation Guide.
3-17
3 Running a Verification
Using Polyspace In One Click to Launch Verification
In this section...
“Overview of Polyspace In One Click” on page 3-18
“Setting the Active Project” on page 3-18
“Sending Files to Poly space Software” on page 3 -20
Overview of Polyspace In One Click
In a Microsoft Windows environment, Polyspace software provides a
convenient way to streamline your work when you want to verify several
files using the same set of options. Once you have set up a project file that
has the options that you want, you designate that project as the active project,
and then send the source files to Polyspace software for verification. You do
nothavetoupdatetheprojectwithsource file information. This process is
called Polyspace In One Click.
3-18
In this part of the tutorial, using Polyspace In One Click, you learn how to:
1 Set the active project.
2 Send files to Polyspace software for verification.
Setting the Active Project
The active project is the project that Polyspace In One Click uses to verify the
files that you select. Once you have set an active project, it remains active
until you change the active project. Polyspace software uses the analysis
options from the project; it does not use the source files or results folder from
the project.
To set the active project:
1 In the taskbar area of your Windows des ktop, right-click the Polyspace In
One Click icon:
The context menu appears.
Using Polyspace®In One Click to Launch Verification
2 Select Set a
ctive project > Browse.
The Please set an active project dialog box opens.
3-19
3 Running a Verification
3 Navigate to polyspace_project.
4 Select example_project.cfg.
5 Click Open to apply the changes and close the dialog box.
Sending Files to Polyspace Software
You can send several files to Polyspace software for verification. For this
tutorial, you send one file,
example.c.
To send
1 Navigate to the folder polyspace _project\sources.
2 Right-click the file example.c.
example.c to Polyspace software for verification:
The context menu appears.
3-20
3 Select Send To > PolySpace.
Using Polyspace®In One Click to Launch Verification
The PolyS
pace basic setting s dialog box appears.
3-21
3 Running a Verification
3-22
4 Make sure that the Results folder is polyspace_project.
Using Polyspace®In One Click to Launch Verification
5 If the Send to P
6 Leave the default values for the other parameters.
olySpace Server option is not already selected, select it.
Click Start.
The verification log opens.
3-23
3 Running a Verification
The compile phase of the verification runs on the client. When the compile
phase is complete:
• You see the following message in the log:
End of PolySpace Verifier analysis
• A message in the log states that the verification was transferred to the
server and gives you the identification number (Analysis ID) for the
verification. For this verification, the identification number is
• Monitor the verification using the Spooler. For information on using the
Spooler to m o n itor a verification on a server, see “Monito ring Progress
Using Queue Manager” on page 3-9.
• When the verification is complete, download the results to
polyspace_project\results. Forinformationondownloadingresults
from a server to a client, see “Removing Verification Results from the
Server” on page 3-13
You review the results in Chapter 4, “Reviewing Verification Results”.
1.
3-24
Launching Client Verification from Project Manager
Launching Clien t Verification from Project Manager
In this section...
“Starting the Verification” on page 3-25
“Monitoring the Progress of the Verification” on page 3-26
“Completing Verification” on page 3-28
“Stopping the Verification Before It is Complete” on page 3-28
Starting the Verification
For the best performance, run verifications on a server. If the server is busy
or you want to verify a small file, you can run a verification on a client.
Note Because a verification on a client can process only a limited number
of variable assignments and function calls, the source code should have no
more than 800 lines of code.
To start a verification that runs on a client:
1 If the project example_project.cfg is not already open, open the project.
For information about opening a project, see “Preparing for Verification”
on page 3-4.
2 Clear the Send to PolySpace Server check box in the General Analysis
options.
3-25
3 Running a Verification
3 If you see a warning th at multitasking is not available when you run
a verification on the client, click OK to continue and close the message
box. This warning appears only when you clear the Send to PolySpace
Server check box.
4 Click the
5 If you see a caution that Polyspace software will remove existing results
from the results folder, click Yes to continue and close the message dialog
box.
The Output Summary and Progress Monitor windows become active,
allowing you to monitor the progress of the verification.
Note If you see the message Verification process failed,clickOK
and go to “Troubleshooting a Failed Verification” on page 3-15.
Run button
on the Project Manager toolbar.
Monitoring the Progress of the Verification
You can monitor th e progress of the verification b y viewing the progress
monitor and logs at the bottom of the Project Manager perspective.
3-26
Launching Client Verification from Project Manager
Theprogressmonitorhighlightsthecurrentphaseinblueanddisplaysthe
amount of time and completion percentage for that phase.
The logs report additional information about the progre ss of the verification.
To view a log, click the button for that log. The information appears in the
log display area at the bottom of the Project Manager window. Follow the
next steps to view the logs:
1 Click the Output Summary tab to display co mpile phase messages and
errors. You can search the log by entering search terms in the Search in
the log box and clicking the left arrows to search backward or the right
arrows to search forward.
2 Click th
options
3 Click the Refresh button to update the display as the verification
e Verification Statistics tab to display statistics, such as analysis
, stubbed functions, and the verification checks performed.
progresses.
4 Click the Full Log tab to display messages, errors, and statistics for all
phases of the verification.
Note You can search the logs. In the Search in the log box, enter a
search term and click the left arrows to search backward or the right
arrows to search forward.
3-27
3 Running a Verification
Completing Verification
When the verification is complete, the message “Verific ation Completed ”
appears at the bottom of the Project Manager window, and the results appear
in the Project Browser.
3-28
In the tutorial Chapter 4, “Reviewing Verification Results”, you open the
Run-Time Checks perspective and review the verification results.
Stopping the Verification Before It is Complete
You can stop the verification befo r e it is complete. If you stop the verification,
results are incomplete. If you start another verification, the verification starts
over from the beginning.
Launching Client Verification from Project Manager
To stop a verification:
1 Click the Stop button on the Project Manager toolbar.
A warning dialog box opens.
2 Click Yes.
The verification stop s and the message
Verification process stopped
appears.
3 Click OK to close the Message dialog box.
Note Closing the Polyspace verification environme nt window does not stop
the verification. To resume display of the verification progress, start the
Polyspacesoftwareandopentheproject.
3-29
3 Running a Verification
3-30
Reviewing Verification
Results
• “About Reviewing Verification Results Tutorial” on page 4-2
• “Opening Verification Results” on page 4-3
• “Exploring Run-Time Checks Perspective” on page 4-4
• “Reviewing Results in Expert Mode” on page 4-8
• “Reviewing Results in Assistant Mode” on page 4-23
4
• “Automatically Testing Unproven Code” on page 4-30
• “Generating Reports of Verification Results” on page 4-31
4 Reviewing Verification Results
R
About Reviewing Verification Results Tutoria l
In this section...
“Overview” on page 4-2
“Before You Start” on pag e 4-2
Overview
In the previous tutorial, Chapter 3, “Running a Verification” , you completed a
verification of
The Polyspace verification environment contains a Run-Time Checks
perspectivethatyouusetoreviewresults. In this tutorial, you learn:
1 How to use the Run-Time Checks perspective, including how to:
• Open the Run-Time Checks perspective and view verification results.
• Explore results in expert mode.
example.c. In this tutorial, you explore the verification resul ts.
4-2
• Explore results in assistant mode.
• Generate reports.
2 How to interpret the color-coding that Polyspace software uses to identify
the severity of an error.
3 How to find the location of an error in the source code.
Before You Start
Before starting this tutorial, be suretocompletethetutorialChapter3,
“Running a Verification”.
In this tutorial, you use the verification results in this file:
polyspace_project\Verification_(1)\Result_(1)\RTE_px_example_project_LAST_
Opening Verification Results
In this section...
“Opening Run-Time Checks Perspective” on page 4-3
“Opening Verification Results” on page 4-3
Opening Run-Time Checks Perspective
You use the Run-Time C hecks perspective to review verification results.
To open the Run-Time Checks perspective:
Opening Verification Results
• Select the Run Time Checks button
Verification Environment toolbar.
in the PolySpace
Opening Verification Results
To open the verification results:
1 Select File > Open Result.
The Please select a file dialog box opens.
2 Navigate to the results folder:
polyspace_project\Verification_(1)\Result_(1).
3 Select the file RTE_px_example_project_LAST_RESULTS.rt e.
4 Click Open.
The results appear in the Run-Time Checks perspective.
Note You can also open results from the Project Manager perspective by
double-clicking the results file in the Project Browser.
4-3
4 Reviewing Verification Results
Exploring Run-Time Checks Perspective
In this section...
“Overview” on page 4-4
“Reviewing the Run-Time Checks Pane” on page 4-6
Overview
The Run-Time Checks perspective looks like the following figure.
4-4
Exploring Run-Time Checks Perspective
Review StatisticsReview Details
Run-Time
Checks
Source
code
The Run-Time Checks perspective has six sections below the toolbar. Each
section provides a different view of the results. The following table describes
these views.
Variable
Access
Call
Hierarchy
4-5
4 Reviewing Verification Results
This Pane... Displays...
Run-Time Checks
(Procedural entities view)
Source
(Source code view)
Review Statistics
(Coding review progress view )
Review Details
(Selected check view)
Variable Access
(Variables view )
Call Hierarchy
(Call tree view)
You can resize or hide any o f these sections. You learn more about the
Run-Time Checks perspective later in this tutorial.
List of the checks (diagnostics) for
each file and function in the project
Source code for a selected check in
the procedural entities view
Statistics about the review progress
for checks with the same type and
category as the selected check
Details about the selected check
Information about global variables
declared in the source code
Tree structure of function calls
Reviewing the Run-Time Checks Pane
The Run-Time Checks pane displays a table with information about the
diagnostics for each file in the project. The Run-Time Checks pane is also
called the Procedural entities view
4-6
When you first open the results file from the verification of
see the follow ing procedural entities.
The file example.c is red because it has a run-time error. Polyspace software
assigns each file the color of the most severe error found in that file. The first
column of the table in the Procedural Entities View is the procedural entity
example.c,you
Exploring Run-Time Checks Perspective
(the file or function). The following table describes some of the other columns
in the procedural entities view .
Column
Indicates
Heading
Number of red checks (operations where an error always
occurs)
Number of gray checks (unreachable code)
Number of orange checks (warnings for operations where
an error might occur)
Number of green checks (operations where an error never
occurs)
Selectivity of the verification (percentage of checks that are
not orange)
This is an indication of the level of proof.
Note You can select which columns appear in the procedural entities view
by editing the preferences.
What you select in the procedural entities view determines what you see in
the other views. In the following examples, you learn how to use the views
and how they interact.
4-7
4 Reviewing Verification Results
Reviewing Results in Expert Mode
In this section...
“What Is Expert Mode?” on page 4-8
“Switching to Expert Mode” on page 4-8
“Reviewing Checks in Expert Mode ” on page 4-8
“Reviewing Additional Examples of Checks” on page 4-14
“Filtering Checks” on page 4-19
What Is Expert Mode?
In expert mode, you see all checks in the Run-Time Checks perspective. You
decide which checks to review and in what order to review them.
Switching to Expert Mode
By default, the Run-Time Checks perspective opens in assistant mode. To
switch from assistant to expert mode:
4-8
• Move the Assistant slider to Off in the Run-Time Checks toolbar.
The toolbar displays buttons and menus specific to expert mode.
Reviewing Checks in Expert Mode
In this part of the tutorial, you learn how to use the Run-Time Checks
perspective to examine verification checks. This part of the tutorial covers:
• “Selecting a Check to Review” on page 4-9
• “Displaying the Calling Sequence” on page 4-11
• “Tracking Review Progress” on page 4-11
Reviewing Results in Expert Mode
Selecting a Check to Review
In the procedural entities view, example.c is red, indicating that this file has
at least one red check. To review a red check in
1 In the procedural entities section of the Run-Time Checks pane, expand
example.c.
2 Expand the red procedure Pointer_Arithmetic().
example.c:
A color-code d list of the checks performed on
Pointer_Arithmetic() opens.
In the list of checks, each item has an acronym that identifies the type
of check and a number. For example, in
IDP.8, IDP stands for Illegal
Dereferenced Pointer. For more information, see “Check D escriptions” in
the Polyspace Products for C Reference.
3 Click the red IDP.8.
The Source pane displays the section of source code where this error occurs.
4-9
4 Reviewing Verification Results
4-10
4 At line 104 of the code, click the red code.
An error message box opens indicating that when the pointer
dereferenced, it is outside of its bounds. At line 92,
array which has 100 elements. The for loop starting at line 94 initializes
the elements of
after the last element of
array to 0. This for loop leaves p pointing to the location
array.
p points to the start of
p is
Reviewing Results in Expert Mode
Displaying the Calling Sequence
You can display the calling sequence that leads to the code associated
with a check. To see the calling sequence for the red
Pointer_Arithmetic():
1 Expand Pointer_Arithmetic().
2 Click the red IDP.8.
3 Click the call graph button in the Review Details toolbar.
A window displays the call graph.
IDP.8 check in
ThecodeassociatedwithIDP.9 is in Pointer_Arithmetic. The generated
main function calls RTE, which calls Pointer_Arithmetic.
Tracking Review Progress
You can keep track of the checks that you have reviewed by m a r k ing them . To
mark that you have reviewed the red
1 Expand Pointer_Arithmetic().
2 Click the red IDP.8.
IDP.8 check in Pointer_Arithmetic():
4-11
4 Reviewing Verification Results
The Review Statistics pane displays a table with statistics about the review
progress for that category and severity of error.
The Count column displays a ratio and the Progress column displays
the equivalent percentage.
The first row displays the ratio of justified checks to total checks that have
the same color and category as the current check. In this example, the
first row displays the ra tio of reviewed red IDP checks to total red IDP
errors in the project.
The second row displays the ratio of justified checks to total checks that
have the same color as the current check. In this example, this ratio is the
ratio of red errors reviewed to total red errors in the project.
4-12
The last row displays the ratio of the number of green checks to the total
number of checks, providing an indicator of the reliability of the software.
Information about the current check (the red
Details window (Selected Check view).
IDP.8) appears in the Review
Reviewing Results in Expert Mode
3 After you review the check, select a Classification to describe the
seriousness of the issue:
•
High
• Medium
• Low
• Not a de fect
4 Select a Status to describe how you intend to address the issue:
Fix
•
• Improve
• Investigate
• Justify with annotations
• No Action Planned
• Other
• Restart with different options
• Undecided
4-13
4 Reviewing Verification Results
5 In the comment box, enter additional information about the check.
6 Select the check box to indicate that you have justified this check.
Note You can also define your own statuses. See “Defining Custom Status
”.
The Coding review progress part of the window updates the ratios of
errors reviewed to total errors.
4-14
Reviewing Additional Examples of Checks
In this part of the tutorial, you learn about other types and categories of
errors by reviewing the following examples in
• “Example: Unreachable Code” on page 4-14
• “Example: Arithmetic Error” on page 4-15
• “Example: A Function with No Errors” on page 4-16
• “Example: Division by Zero” on page 4-17
Example: Unreachable Code
Unreachable code is code that never executes. Polys pace software displays
unreachable code in gray. In the following example, you look at an example
of unreachable code.
1 In Procedural Entities,clickUnreachable_Code().
The source code view displays the source code for this function.
example.c:
Reviewing Results in Expert Mode
2 Examine the source code.
At line 212, the code
is always false.
<0
x=x+1is never reached because the condition x
Example: Arithmetic Error
In the following example, Polyspace software detects a memory corruption
error:
1 In Procedural entities, expand the red Square_Root() function.
The source code view displays the source code for this function.
4-15
4 Reviewing Verification Results
4-16
2 Examine the source code.
Because
at line 193 is always negative.
beta is always less than 0.75, the a rgument to the sqrt() function
Example: A Function with No Errors
In the following example, Polyspace software verifies code with a large
number of iterations, and determines that the loop terminates and a variable
does not overflow:
1 In Procedural entities, click the green Non_Infinite_Loop() function.
The source code view displays the source code for this function.
Reviewing Results in Expert Mode
2 Examine the source code. The variable x never overflows because the while
loop at line 70 terminates before x can overflow.
Example
: Division by Zero
In the following example, Polyspace software detects division by zero:
1 In Procedural entities, expand Recursion().
The so
urce code view displays the source code for this function.
4-17
4 Reviewing Verification Results
4-18
2 Exa
mine the
Recursion() function.
Reviewing Results in Expert Mode
When Recursion() is called with depth less than zero, the code at line 142
results in division by zero. The o ran ge color indicates that this operation is
a potential error (depending on the value of
3 Examine the red Recursion_caller function.
depth).
The first call to
Recursion() with dept h less than zero, causing a division by zero. The
second call to
because it calls
Recursion() at line 157 is red because it calls
Recursion() at line 164 does not cause division by zero
Recursion() with depth greater than zero.
Filtering Checks
You can filter the checks that you see in the Run-Time Checks perspective so
that you can focus on certain checks. Polyspace software allows you to filter
your results in several ways. You can filter by:
• Check category (ZDV, IDP, NIP, etc.)
• Color of check (gray, orange, green)
• Justified or unju s tif ied
• Classification
• Status
To filter checks, select one of the filter buttons in the Run-Time checks toolbar.
Tip The tooltip for a filter button describes what filter the button activates.
Example: Filtering IRV Checks
You can use an RTE filter to hide a given check category, such as IRV. When
a filter is enabled, you do not see that check category.
To filter IRV checks:
4-19
4 Reviewing Verification Results
1 Expand Square_Root().
Square_Root()has seven checks: four are green, one is red, and two are
gray.
2 Click the R
3 Clear the IRV option.
TE filter icon
.
ThesoftwarehidestheIRVcheckforSquare_Root().
4-20
Reviewing Results in Expert Mode
4 Select the IRV option to redisplay the IRV check.
Note When you filter a check category, red checks of that category are not
hidden. F or example, if you filter IDP checks, you still see
Pointer_Arithmetic().
IDP.8 under
Example: Filtering Green Checks
You can use a Colo r filter to hide certain color checks. When a filter is
enabled, you do not see that color check.
To filter green checks:
1 Expand Square_Root().
Square_Root()has seven checks: four are green, one is red, and two are
gray.
2 Click the Color filter icon .
4-21
4 Reviewing Verification Results
3 Clear the Green C hecks option.
The software hides the green checks.
4-22
Reviewing Results in As sistant Mod e
In this section...
“WhatIsAssistantMode?”onpage4-23
“Switching to Assistant Mode” on page 4-23
“Selecting the Methodology and Criterion Level” on page 4-24
“Exploring Methodology for C” on page 4-24
“Reviewing Checks” on page 4-26
“Defining a Custom Methodology” on page 4-28
What Is Assistant Mode?
By default, the Run-Time Checks perspective opens in assistant mode. In
assistant mode, Polyspace software chooses the checks for you to review and
the order in which you review them. Polyspace software presents checks
in this order:
Reviewing Results in Assistant M ode
1 All red checks.
2 All blocks of gray checks (the first check in each unreachable function).
3 Orang
You le
Meth
Swit
To s
• Mov
e checks according to the methodology and criterion level you select.
arn about methodologies and criterion levels in “Selecting the
odology and Criterion Level” on page 4-24.
ching to Assistant Mode
witch from expert to assistant mode:
etheAssistantsliderto1 in the Run-Time Checks toolbar.
The Assistant Checks tab op ens, displaying the checks you need to review,
and the toolbar displays controls specific to assistant mode.
4-23
4 Reviewing Verification Results
The controls for assistant mode include:
• A menu for selecting the review methodology for orange checks.
• A slider for selecting the criterion level withi n that methodology.
• Arrows for navigating through the reviews.
Selecting the Methodology and Criterion Level
A methodology defines which orange checks you review in assistant mode.
Each methodology has three criterion levels, corresponding to different
development phases, with increasing review requirements. As the criterion
level increases, you review more checks.
To select the methodology and level for this tutorial:
1 Select Methodology for C from the methodology menu.
4-24
2 If the level slider is not already at 1, move the slider to level 1.
Exploring Methodology for C
In this part of the tutorial, you examine Methodology for C, which defines
the number of orange checks you review in assistant mode.
To examine the configuration for Methodology for C:
1 Select Options > Preferences.
Reviewing Results in Assistant M ode
The PolySpace Preferences dialog box opens.
2 Select the Assistant configuration tab.
The configuration for Methodology for C opens.
On the right side of the dialog box, a table shows the number of orange
checks that you review for a given criterion and check category.
Forexample,thetablespecifiesthatyoureviewfiveorangeZDVchecks
when you select criterion 1. The num ber of checks increases as you move
from criterion 1 to criterion 3, reflecting the changing review requirements
as you move through the development process.
4-25
4 Reviewing Verification Results
In the lower-left part of the dialog box, the section Review threshold
criterion contains text that appears in the tooltip for the criterion slider
on the Run-Time Checks toolbar.
For the configuration Methodolog y for C, the following table lists the
criterion names.
4-26
Criterion
1
2
3
These
3 Click OK to close the dialog box.
names correspond to phases of the development process.
Name in th
Fresh code
Unit tested
Code Review
eTooltip
Reviewing Checks
In assistant mode, you review checks in the order in which Polyspace software
presents them:
• All of the red checks.
• All blocks of gray checks (the first check in each unreachable function).
• Orange checks according to the selected methodology and criterion level.
Reviewing Results in Assistant M ode
Earlier in this tutorial, you selected M ethodology for C, criterion l. In th is part
of the tutorial, you review the checks for
example.c using this methodology
and criterion. To navigatethroughthesechecks:
1 Click the forward arrow .
The Assistant Checks tab shows the current check (
IDP.8).
The source code view (lower right) displays the source for this check and
the current check view (upper right) displays information about this check.
Note You can display the calling sequence and track review p rogress, as
described in “Reviewing Results in Expert Mode” on page 4-8.
4-27
4 Reviewing Verification Results
2 Continue to click the forward arrow until you have gone through all of
3 Click No.
Defining a Custom Methodology
You cannot change the predefined methodologies, s uch as Methodology for
C, but you can define your own methodology. In this part of the tutorial, you
learn how to create and use your own methodology.
the checks.
After the last check, a dialog box opens asking if you want to start again
from the first check.
4-28
The methodology that you create is the Methodology for C with one change.
To define your custom methodology:
1 Select Options > Preferences.
The PolySpace Preferences dialog box opens.
2 Select the Assistant configuration tab.
3 Select Add a set from the Configuration set menu.
4 In the Cre ate a new set dialog box, enter My methodology for the name and
click Enter to close the dialog box.
5 Under the Criterion 1 column, enter the number 1 next to IDP.Polyspace
software selects up to one orange IDP for review.
6 Click OK to save the methodology and close the dialog box.
Reviewing Results in Assistant M ode
To use My methodology:
1 Select My methodology from the methodology menu.
2 If the level slider is not already at 1, move the slider to level 1.
3 Click the forward arrow to review the checks.
With this methodology a t criterion 1, you review the orange IDP .17 (you
did not review IDP.17 earlier in the tutorial because the number of orange
IDP checks in Methodology for C, criterion 1 is zero).
4-29
4 Reviewing Verification Results
Automatically Testing Unproven Code
Reviewingorangecodetofindtrueerrors is a time-consuming task. You can
use the Automatic Orange Tester (AOT) to automatically create and run test
cases to identify errors in the orange code. The workflow for using the AOT is:
1 Set an option to indicate that you want to prepare automatic tests.
2 Run the verification to prepare the tests and verify the source code.
3 When the veri
4 Review the results.
To learn how to use the AOT, see “Automatically Testing Orange Code” in the
Polyspace Products for C User’s Guide.
fication is finished, run the test cases.
4-30
Generating Reports of Verification Results
In this section...
“Polyspace Report Generator Overview” on page 4-31
“Generating Report for example.c”onpage4-32
Polyspace Report Generator Overview
The Polyspace Report Generator allows you to generate reports about your
verification results, using p redefined report templates.
The Polyspace Report Generator provides the following report templates:
• Coding Rules Report – Provides information about compliance with
MISRA C Coding Rules, as well as Polyspace configuration settings for
the verification.
• Developer Report – Provides information useful to developers, including
summary results, detailed lists of red, orange, and gray checks, and
Polyspace configuration settings for the verification. Detailed results are
sorted by type of check (Proven Run-Time Violations, Proven Unreachable
Code Branches, Unreachable Functions, and Unproven Run-Time Checks).
Generating Repo rts of Verification Results
• Developer Review Report – Provides the same information as the
Developer Report, but reviewed results are sorted by review classification
(
High, Medium, Lo w, Not a defect) and status, and untagged checks are
sorted by file location.
• Developer with Green Checks Report – Provides the same content as
the Developer Report, but also includes a detailed list of green checks.
• Quality Report – Provides information useful to quality engineers,
including summary results, statistics about the code, graphs showing
distributions of checks per file, and Polyspace configuration settings for
the verification.
• Software Quality Objectives Report – Provides comprehensive
information on software quality objectives (SQO), including code metrics,
code analysis (coding-rules check er results), code verification ( ru n- time
checks), and the configuration settings for the verification. The code
4-31
4 Reviewing Verification Results
The Polyspace Report Generator allows you to generate verification reports in
the following formats:
• HTML
• PDF
• RTF
• Microsoft W ord
• XML
Note Microsoft Word format is not available on UNIX platforms. If you select
Word format on a UNIX platform, the software uses RTF format instead.
metrics section provides is the same information displayed in the Polyspace
Metrics web interface.
4-32
Generating Report for example.c
You can generate rep orts for any verification results using the Polyspace
Report Generator.
To generate a verification report:
1 If your verification results are not already open, open them.
2 Select Run > Run Report > Run R eport.
The Run Report dialog box opens.
Generating Repo rts of Verification Results
3 In the Select Report Template sectio n, select Developer.rpt.
4 In the Output folder section, select the \polyspace_project folder.
5 Select
6 Click Run Report.
PDF Output format.
The software creates the specified report. When report generation is
complete, the report opens.
4-33
4 Reviewing Verification Results
4-34
Loading...