|
|
|
| R2012a Documentation → Polyspace | |
Learn more about Polyspace |
|
| Contents | Index |
When you run a verification on a Polyspace server, the Polyspace software automatically downloads the results to the client system that launched the verification. The results are also stored on the Polyspace server, and you can download the results from the server to other client systems.
Note If you download results before the verification is complete, you get partial results and the verification continues. |
To download verification results from a server to a client system:
Double-click the Polyspace Spooler icon.
The Polyspace Queue Manager Interface opens.
Right-click the job that you want to view, and select Download Results .
Note After downloading your results, to remove the job from the queue , from the context menu, select Download Results And Remove From Queue . |
The Save dialog box opens.
Select the folder into which you want to download results.
Click Save to download the results and close the dialog box.
When the download is complete, a dialog box opens asking if you want to open the Polyspace results.
Click Yes to open the results.
Once you download results, they remain on the client. You can review them at any time using the Polyspace Results Manager perspective.
You can download verification results at the command line using the psqueue-download command.
To download your results, enter the following command:
Polyspace_Common/RemoteLauncher/bin/psqueue-download <id> <results dir>
The verification <id> is downloaded into the results folder <results dir>.
Note If you download results before the verification is complete, you get partial results and the verification continues. |
Once you download results, they remain on the client. You can review them at any time using the Polyspace Results Manager perspective.
The psqueue-download command has the following options:
[-f] force download (without interactivity)
-admin -p <password> allows administrator to download results.
[-server <name>[:port]] selects a specific Queue Manager.
[-v|version] gives release number.
Note When downloading a unit-by-unit verification group, all the unit results are downloaded and a summary of the download status for each unit is displayed. |
For more information on managing verification jobs at the command line, see Managing Verifications in Batch.
If you run a unit-by-unit verification, each source file is sent to thePolyspace Server individually. The queue manager displays a job for the full verification group, as well as jobs for each unit (using a tree structure).
You can download and view verification results for the entire project or for individual units.
To download the results from unit-by-unit verifications:
To download results for an individual unit, right-click the job for that unit, then select Download Results.
The individual results are downloaded and can be viewed as any other verification results are viewed.
To download results for a verification group, right-click the group job, then select Download Results.
The results for all unit verifications are downloaded, as well as an HTML summary of results for the entire verification group.
You can open verification results directly from the Project Browser in the Project Manager perspective. Because each Polyspace project can contain multiple verifications, the Project Browser allows you to quickly identify and open the results that you want to review.
To open verification results from the Project Manager:
Open the project containing the results that you want to review.
In the Project Browser Source tree, navigate to the results that you want to review.
Double-click the results file.
The results open in the Results Manager perspective.
Use the Results Manager perspective to review verification results. If you know the location of the results file that you want to review, you can open it directly from the Results Manager perspective.
Note You can also browse and open results from the Project Browser in the Project Manager perspective. |
To open verification results from the Results Manager perspective:
On the Polyspace verification environment toolbar,
click the Results
Manager button
.
Select File > Open Result
The Open results dialog box opens.
Select the results file that you want to view.
Click Open.
The results open in the Results Manager perspective.
The Results Manager perspective looks like the following figure.
The Results Manager perspective has six sections below the toolbar. Each section provides a different view of the results. The following table describes these views.
| This Pane or Tab ... | Displays ... |
|---|---|
| Results Explorer\Results Summary (Procedural entities view) | List of checks (diagnostics) for each file and function in the project |
| Source (Source code view) | Source code for a selected check in the procedural entities view |
| Check Details (Selected check view) | Details about the selected check |
| Check Review\Review Statistics (Coding review progress view) | Review information
about selected check Statistics about the review progress for checks with the same type and category as the selected check |
| Variable Access (Variables view ) | Information about global variables declared in the source code |
| Call Hierarchy (Call tree view) | Tree structure of function calls |
You can resize or hide any of these sections.
The Results Explorer tab displays a table with information about the diagnostics for each file in the project. The Results Explorer tab is also called the Procedural entities view.
The checks in the Procedural entities view are colored as follows:
Red — Indicates code that always has an error (errors occur every time the code is executed).
Gray — Indicates unreachable code (dead code).
Orange — Indicates unproven code (code might have a run-time error).
Purple. — Indicates coding rule violation
Green — Indicates code that never has a run-time error (safe code).
Polyspace software assigns files and functions the color of the most severe error found in that file. For example, the file example.c is red because it has run-time errors.
The first column of the table is the procedural entity (the file or function). The following table describes some of the other columns in the procedural entities view.
| Column Heading | Indicates |
|---|---|
| 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 purple checks (coding rule violations) |
| Number of green checks (operations where an error never occurs) |
| Selectivity of the verification (percentage of checks that are not orange), which is an indication of the level of proof. |
You can select which columns appear in the procedural entities view by right-clicking the Procedural entities column heading and selecting the columns you want to display.
Tip
If you see three dots in place of a heading,
|
Code Coverage Metrics. In the Procedual entities view, the software displays two metrics for the project:
unp — Number of unreachable procedures (functions) as a fraction of the total number of procedures (functions)
cov — Percentage of elementary operations in executable procedures (functions) covered by verification
These metrics provide:
A measure of the code coverage achieved by the Polyspace verification.
Indicators about the validity of your Polyspace configuration. For example, a large unp value and a low cov value may indicate an early red check or missing function call.
Unreachable Functions. If the verification detects functions that cannot be reached from the main program, it does not verify them. The software considers these functions to be unreachable, and highlights them in gray in the procedural entities view.
In this example, the function Unreachable_Code is considered unreachable, and therefore is not verified.
The Source pane shows the source code with colored checks highlighted. The Source Pane is also called the Source code view.
Tooltips. Placing your cursor over a check displays a tooltip that provides ranges for variables, operands, function parameters, and return values. For more information on tooltips, see Using Range Information in the Results Manager Perspective.
Examining Source Code. In the Source pane, if you right-click a text string, the context menu provides options that help you to examine your code. For example, right-click the global variable PowerLevel:
Use the following options to examine and navigate through your code:
Search "PowerLevel" in current source code — List all occurrences of the string in the Search pane.
Go To Line — Open the Go to line dialog box. If you specify a line number and click Enter, the software displays the specified line of code.
Go to Definition — If the selected text is a global variable or function, display the line of code that contains the declaration.
Open Source File — Open the source file with your text editor.
Managing Multiple Files in Source Pane. You can view multiple source files in the Source pane. By default, the files are displayed as tabs in the Source pane.
On the Source pane toolbar, right-click any tab to manage source files.
From the Source pane context menu, you can:
Close – Close the currently selected source file.
Close Others – Close all source files except the currently selected file.
Close All – Close all source files.
Next – Display the next tab.
Previous – Display the previous tab.
New Horizontal Group – Split the Source window horizontally to display the selected source file below another file.
New Vertical Group – Split the Source window vertically to display the selected source file side-by-side with another file.
Floating – Display the current source file in a new window, outside the Source pane.
The Check Details pane displays information about the current check. The Check Details pane is also called the Selected check view.
Error Call Graph. Click the Show error call graph icon
in the Check Details pane
toolbar to display the call sequence that leads to the code associated
with a check.
For more information, see Displaying the Call Sequence for a Check.
When reviewing checks, use the Check Review tab to mark checks as Justified, and enter comments to describe the results of your review. This helps you track the progress of your review and avoid reviewing the same check twice.
For more information, see Reviewing and Commenting Checks .
The Review Statistics tab displays statistics about how many checks you have reviewed. As you review checks, the software updates these statistics.
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 of the current check. In this example, the first row displays the ratio 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 color of the current check. In this example, this is the ratio of red errors reviewed to total red errors in the project.
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.
The Variable Access pane, which is also called the Variables view, displays global variables. The pane shows where in the source code the variables are read or written to, and provides:
Information about the variables and associated fields. For example, number of read/write access operations, data type, and value range. For global variables that are integers (signed and unsigned) or floating point variables (float and double), the software provides range information for both the individual read/write access operations within a file and the union of these operations.
A hierarchical view of structured variables.
The software does not treat the addressing operation on a global variable or object (in C++) as a read or write access operation. For example, consider the following C++ code.
class C0
{
public:
C0() {}
int get_flag()
{
volatile int rd;
return rd;
}
~C0() {}
private:
int a; /* Never read/written */
};
C0 c0; /* c0 is unreachable */
int main()
{
if (c0.get_flag()) /* Uses address of the method */
{
int *ptr = take_addr_of_x();
return 1;
}
else
return 0;
}The object c0 is unreachable (gray). However, you will not see the method call c0.get_flag() in the Variable Access pane because the call is an addressing operation on the method belonging to the object c0.
Concurrent Access Graph. Click the Show Access Graph button
in the Variable Access pane
toolbar to display a graph of read and write access for the selected
variable.
For more information, see Displaying the Access Graph for Variables.
Non Shared Variables. Click the Non-Shared Variables button
in the Variable Access pane toolbar
to show or hide non-shared variables.
Read and Write Access in Dead Code. If a read or write access operation on a global variable lies
within dead code, then Polyspace colors the operation gray in
the Variable Access pane. When you examine verification
results, you can hide these operations by clicking the filter button
.
Legend Information. To display the legend for a variable, right-click the variable and select Show legend.
The Call Hierarchy pane displays the call tree of functions in the source code. You can use the call tree view to easily navigate up and down the call tree. The Call Hierarchy pane is also called the Call Tree view.
Callers and Callees. Click the buttons
in the Call Tree View toolbar to show
or hide callers and callees.
Function Definitions. To go directly to the definition of a function, right-click the function call and select Go to definition.
On the Results Manager toolbar, use the slider to specify the review level.
You can review results from five different levels:
0 — Display purple checks that are violations of coding rules with state Error and red and gray run-time checks (default). You can also display orange checks that are potential run-time errors. On the Polyspace Preferences > Review Configuration tab, specify the type of potential run-time errors that you are interested in. See Reviewing Results at Level 0.
1, 2, and 3 — Display all purple checks and red, gray, and green checks. In addition, display orange checks according to values specified on the Polyspace Preferences > Review Configuration tab. You can use either a predefined or custom methodology to specify the number of orange checks per category. See Viewing Methodology Requirements for Levels 1, 2, and 3 and Defining a Custom Methodology for Levels 1, 2, and 3.
All — Display all checks.
The default setting is 1.
You can search your results and source code using the Search feature in the Results Manager perspective toolbar.
The Search toolbar allows you to quickly enter search terms, specify search options, and set the scope for your search.
You can limit the scope of your search to only file content, only expanded nodes, or you can search the complete hierarchy.
When you perform a search, your search results are reported in the Search tab.
Search results are organized by location:
Source Code View
Results Explorer View
Call Hierarchy View
Variable Access View
On the Search tab toolbar, you can use the four filter buttons to hide results from any of these locations.
If the source files that you want to verify are created on an operating system that uses different character encoding than your current system (for example, when viewing files containing Japanese characters), you receive an error message when you view the source file or run certain macros.
The Character encoding option allows you to view source files created on an operating system that uses different character encoding than your current system.
To set the character encoding for a source file:
Select Options > Preferences.
In the Polyspace Preferences dialog box, select the Character encoding tab.
Select the character encoding used by the operating system on which the source file was created.
Click OK.
Close and restart the Polyspace verification environment to use the new character encoding settings.
When opening results for automatically generated code, the software must know which code generator created the code, so that it can interpret comments and create back-to-source links in the Results Manager perspective.
If you launched the verification using the Polyspace Model Link SL or Polyspace Model Link TL products, the software automatically creates a file in the results folder called code_generator_used.txt to provide this information. However, if you did not use these products to launch verification, you must provide this information manually.
To manually specify which code generator created the code:
Open your results in the Results Manager perspective.
Select Review > Code Generator Support > code_generator
To avoid specifying the code generator each time you open your results, you can manually create a file named code_generator_used.txt in your results folder. The software then automatically uses this file each time you open the results.
The format of this file is:
<Code generator> MATLABROOT=<Path to MATLAB> ModelVersion=<model name>:<model version>
<Code generator> can be either RTWEmbeddedCoder or TargetLink.
For example:
RTWEmbeddedCoder MATLABROOT=C:\MATLAB\R2010b ModelVersion=demo_ml:1.94
 | Before You Review Polyspace Results | Reviewing Results Systematically |  |
| © 1984-2012- The MathWorks, Inc. - Site Help - Patents - Trademarks - Privacy Policy - Preventing Piracy - RSS |