Documentation

Polyspace Products for Ada Release Notes

R2015b

New Features, Bug Fixes, Compatibility Considerations

Improved Review Capability: View result details and add review comments in one window

In R2015b, the Check Details pane is renamed Result Details. On this pane, in addition to viewing details about a result, you can now enter review information such as Classification, Status, and comments. For more information, see Add Review Comments to Results.

Improvements in Polyspace Plugin for Eclipse

In R2015b, the following improvements have been made to the Polyspace® plugin for Eclipse™:

  • When you select a result in the Results Summary view, the Result Details view displays additional information about the result. In the Result Details view, if you click the button next to the result name, you can see a brief description and examples of the result.

  • You can switch to a Polyspace perspective that shows only the information relevant to a Polyspace verification. To open the perspective, select Window > Open Perspective > Other.

Including options multiple times

You can now specify analysis options multiple times. This feature is available only at the command line or using the command-line names in the Advanced options dialog box in the user interface. Customize pre-made configurations without having to find the changed options in the options file.

If you specify an option multiple times, only the last setting is used. The user interface also follows this rule. If you specify m68k for Target processor type and -target i386 for Advanced options, this counts as multiple analysis option specifications. Polyspace uses the target specified in the Advanced options box, i386.

Compatibility Considerations

If your current configuration specifies analysis options multiple times, change the configuration by either:

  • Removing the unnecessary analysis options.

  • Moving the desired analysis options to the end of the configuration.

Renaming of labels in Polyspace user interface

The labels associated with specifying constraints have changed as follows:

  • On the Configuration pane, the field Variable/function range setup is changed to Constraint setup.

  • On the Results Summary and Result Details pane, the field Classification is changed to Severity. You assign a Severity such as High, Medium and Low to a defect to indicate how critical you consider the issue.

  • When you click the icon beside the Constraint setup field, a new window opens. The window name is changed from Load DRS file to Load a constraint file.

Changes in analysis options

In R2015b, the following options have been added or removed:

OptionStatusDescription
-known-NTCRemovedPolyspace includes this behavior by default. Remove this option from any existing configurations.
-permissiveRemovedUse -continue-with-in-out-niv instead.
-automatic-stubbingRemovedPolyspace includes this behavior by default. Remove this option from any existing configurations.
-float-overflowsRemovedPolyspace includes this behavior by default. Remove this option from any existing configurations.
-continue-with-exisiting-hostRemovedPolyspace includes this behavior by default. Remove this option from any existing configurations.
-allow-unsupported-linuxRemovedPolyspace includes this behavior by default. Remove this option from any existing configurations.
-passes-timeRemovedPolyspace includes this behavior by default. Remove this option from any existing configurations.
-continue-with-red-errorRemovedPolyspace includes this behavior by default. Remove this option from any existing configurations.
-voaRemovedPolyspace includes this behavior by default. Remove this option from any existing configurations.
-machine-architectureRemovedPolyspace includes this behavior by default. Remove this option from any existing configurations.
-strictRemovedThis option is no longer supported. Remove this option from any existing configurations.
-continue-with-compile-errorRemovedThis option is no longer supported. Remove this option from any existing configurations.

Compatibility Considerations

If you use scripts that contain any of the removed or updated options, change your scripts accordingly.

R2015a

New Features

Simplified workflow for project setup and results review with a unified user interface

In R2015a, the Project and Results Manager perspectives are now unified. You can run verification and review results without switching between two perspectives.

The major changes are:

  • You can start a new verification during your results review. Previously, you started a new verification only from the Project Manager perspective.

  • After a verification, the result opens automatically. If you are looking at a previous result when a verification is over, you can load the new result or retain the previous one on the Results Summary pane. If you retain the previous results, you can later open the new results from the Project Browser. The new results are highlighted.

  • You can have any of the panes open in the unified interface.

    Previously, you could open the following panes only in one of the two perspectives.

    Project ManagerResults Manager
    • Project Browser: Set up project.

    • Configuration: Specify analysis options for your project.

    • Output Summary: Monitor progress of verification.

    • Full Log: Find all information about a verification.

    • Results Summary: View Polyspace results.

    • Source: View read-only form of source code color coded with Polyspace results.

    • Check Details: View details of a particular result.

    • Check Review: Comment on a particular result.

    • Variable Access: View global variables and read/write operations on them.

    • Call Hierarchy: View callers and callees of a function.

    • Results Properties: Same as Full Log, but associated with results instead of a project. This pane has been removed.

    • Settings: Same information as Configuration, but associated with results instead of a project. This pane has been removed.

    • Orange Sources: View sources of orange checks.

    • Sensitivity Context: For a check that has a different color for different function calls, view the check color for each function call.

Code complexity metrics available in user interface

In R2015a, you can view code complexity metrics in the Polyspace user interface. Previously, this information was available only in the Polyspace Metrics web interface.

In the user interface, you can:

  • Specify a limit for the value of a metric. If the metric value for your source code exceeds this limit, the metric appears red on the Results Summary pane.

  • Justify the value of a metric. If a metric value exceeds specified limits and appears red, you can add a comment with the rationale.

  • Generate a report containing the metric values and associated comments and justifications.

Combining these actions, you can enforce coding standards across your organization.

Reducing the complexity of your code improves code readability, reduces the possibility of coding errors, and allows more precise Polyspace verification.

For more information, see Code Metrics.

Review of global variable usage

In R2015a, you can comment and justify global variable usage on the Results Summary pane. Previously, you viewed global variable usage on the Variable Access pane, but could not comment on them.

On the Results Summary pane, global variables are classified into one of the following categories.

CategoryColorMeaning
SharedPotentially unprotected Orange

Global variables shared between multiple tasks but possibly not protected from concurrent access by the tasks

ProtectedGreen

Global variables shared between multiple tasks and protected from concurrent access by the tasks

Not sharedUnusedGray

Global variables used in a single task

UsedBlack

Global variables declared but not used

For code that you do not intend for multitasking, all variables are nonshared and can be either used or unused. For code that you intend for multitasking, you can specify tasks and protections through the analysis options for multitasking. For more information, see Entry points, Critical section details and Temporally exclusive tasks.

You can still view the global variables on the Variable Access pane.

  • To comment and justify potentially unprotected and unused global variables, use the Results Summary pane.

  • To find all read and write operations on a global variable, use the Variable Access pane.

For more information, see Global Variables.

Review of latest results compared to last run

In R2015a, you can review only new results compared to the previous run.

If you rerun your verification, the new results are displayed with an asterisk (*) against them on the Results Summary pane. To filter only these new checks, select the New results box.

If you make changes in your source code, you can use this feature to see only the checks introduced due to those changes. You can avoid reviewing checks in the source code that you did not change.

Improvements in search capability in the user interface

In R2015a, the Search pane allows you to search for a string in various panes of the user interface.

To search for a string in the new user interface:

  1. If the Search pane is not visible, open it. Select Window > Show/Hide View > Search.

  2. Enter your string in the search box.

  3. From the drop-down list beside the box, select names of panes you want to search.

The Search pane consolidates all the search options previously available:

  • In the Project Manager perspective, the global search box allowed you to search on the Configuration pane.

  • In the Results Manager perspective, the global search box allowed you to search on the Source, Results Summary, Call Hierarchy, and Variable Access panes.

  • Search boxes on the Output Summary and Full Log panes allowed you to search on those panes.

Simplified results infrastructure

Polyspace results folders are reorganized and simplified. Files have been removed, combined, renamed, or moved. The changes do not affect the results that you see in the Polyspace environment.

Some important changes and file locations:

  • The main results file is now encrypted and renamed ps_results.rte. You can view results only in the Polyspace environment.

  • The log file, Polyspace_R2015a_project_date-time.log has not changed.

For more information, see Results Folder Contents.

R2014b

New Features, Bug Fixes, Compatibility Considerations

Polyspace Client for Ada Product

Code Editor for Editing Source Files in Polyspace User Interface

In R2014b, by default, you can edit your source files inside the Polyspace user interface.

  • In the Project Manager perspective, on the Project Browser tree, double-click your source file.

  • In the Results Manager perspective, right-click the Source pane and select Open Source File.

Your source files appear on a Code Editor tab. On this tab, you can edit and save your source files.

To use an external text editor, change your preferences.

  1. Select Tools > Preferences.

  2. Specify an external editor on the Editors tab.

For more information, see Specify External Text Editor.

Contextual help for verification options and checks

In R2014b, contextual help is available for verification options in the Polyspace interface and its plug-ins. To view the contextual help:

  1. Hover your cursor over a verification option in the Configuration window.

  2. Inside the tooltip, select the "More Help" link.

    The documentation for that analysis option appears in a new window.

Contextual help is available in the Polyspace interface for checks. To view the contextual help:

  1. In the Results Manager perspective, select a runtime error.

  2. Inside the Check Details window, select .

    The documentation for that check appears in a dockable window.

For more information about getting help in the Polyspace interfaces, see Learning More.

Default verification level changed

In R2014b, unless you specify a verification level explicitly, Polyspace verification performs two passes on your source code instead of four. For instance:

  • In the user interface, on the Output Summary tab, you can see that the verification continues to Level2. For more passes, on the Configuration pane, under the Precision node, select a Verification level.

  • At the command line, the verification implicitly uses -to pass2. For more passes, use the -to option explicitly with a higher pass value.

The default verification is completed in much less time.

For more information, see Verification level.

Compatibility Considerations

If you do not specify a verification level explicitly in your polypsace-ada command, your verification runs to Software Safety Analysis Level 2. In most cases, this verification level produces only slightly more orange checks than Software Safety Analysis Level 4. However, if you see a significant change in your results, to reproduce your earlier results:

  • In the user interface, select Software Safety Analysis Level 4 for Verification level.

  • At the command line, use the option -to pass4 with the polypsace-ada command.

Improved global menu in user interface

The global menu in the Polyspace user interface has been updated. The following table lists the current location for the existing global menu options.

GoalPrior to R2014bR2014b
Open the Polyspace Metrics interface in your web browser.File > Open Metrics Web InterfaceMetrics > Open Metrics
Upload results from the Polyspace user interface to Polyspace Metrics.File > Upload in Polyspace Metrics repositoryMetrics > Upload to Metrics
Update results stored in Polyspace Metrics with your review comments and justifications.File > Save in Polyspace Metrics repositoryMetrics > Save comments to Metrics
Generate a report from results after verification.Run > Run Report > Run ReportReporting > Run Report
Open generated report.Run > Run Report > Open ReportReporting > Open Report
Import review comments from previous verification.Review > ImportTools > Import Comments
Specify settings that apply to all Polyspace projects.Options > PreferencesTools > Preferences
Specify settings for remote verification.Options > Metrics and Remote Server SettingsMetrics > Metrics and Remote Server Settings

Improved Project Manager perspective

The following changes have been made in the Project Manager perspective:

  • The Progress Monitor tab does not exist anymore. Instead, after you start a verification, you can view its progress on the Output Summary tab.

  • In the Project Browser, projects appear sorted in alphabetical order instead of order of creation.

Improved Results Manager perspective

The following changes have been made in the Results Manager perspective:

  • To prioritize your orange check review, use the Show menu on the Results Summary pane. This menu replaces the previously available methodologies for the same purpose.

    • To display red, gray and orange checks likely to be run-time errors, from the Show menu, select Critical checks. This option replaces the First checks to review methodology.

    • To display all checks, from the Show menu, select All checks. This option replaces the All checks methodology.

    • The methodologies Methodology for Ada > Light and Methodology for Ada > Moderate no longer exist.

    • To create your own subset of orange checks to review, select Tools > Preferences. On the Review Scope tab, specify the number or percentage of orange checks of each type to review. The options on this tab replace the options on the Review Configuration tab.

  • To group your checks, use the Group by menu on the Results Summary pane.

    • To leave your checks ungrouped, instead of List of Checks, select Group by > None.

    • To group checks by check color and type, instead of Checks by Family, select Group by > Family.

    • To group checks by file and function, instead of Checks by File/Function, select Group by > File.

  • To view the percentage of checks that you have justified, instead of the Review Statistics pane, use the Justified column on the Results Summary pane. On this pane:

    • To view the percentage of checks that you justified broken down by color/type, select Group by > Family.

    • To view the percentage of checks that you justified broken down by file/function, select Group by > File.

Remote launcher and queue manager renamed

Polyspace has renamed the remote launcher and the queue manager that shows jobs sent for remote verification. The server computer that manages all other server computers is still called the Queue Manager server.

Previous nameUse insteadMore information
polyspace-rl-managerpolyspace-server-settingsOnly the binary name has changed. The interface title, Metrics and Remote Server Settings, is unchanged.
polyspace-spoolerpolyspace-job-monitorThe binary and the interface titles have changed. Interface labels have changed in the Polyspace interface and all its plug-ins.
Queue Manager or SpoolerJob Monitor

Compatibility Considerations

You receive a warning if you use the old binaries or functions.

Polyspace Server for Ada Product

Remote launcher and queue manager renamed

Polyspace has renamed the remote launcher and the queue manager that shows jobs sent for remote verification. The server computer that manages all other server computers is still the Queue Manager server.

Previous nameUse insteadMore information
polyspace-rl-manager.exepolyspace-server-settings.exeOnly the binary name has changed. The interface title, Metrics and Remote Server Settings, is unchanged.
polyspace-spooler.exepolyspace-job-monitor.exeThe binary and the interface titles have changed. Interface labels have changed in the Polyspace interface and all its plug-ins.
Queue Manager or SpoolerJob Monitor

Compatibility Considerations

You receive a warning if you use the old binaries or functions.

Local unit-by-unit verification

In R2014b, you can verify your source code file by file on your local installation of Polyspace. Each file is verified independently of the other files in your module. Previously, you could perform such unit-by-unit verification only on a remote server. However, you still require a Polyspace Server™ license.

For more information, see Running Verification Unit-by-Unit.

R2014a

New Features, Bug Fixes

Polyspace Client for Ada Product

Default Text Editor

In R2014a, Polyspace uses a default text editor for opening source files. The editor is:

  • WordPad in Windows®

  • vi in Linux®

You can change the text editor from the Editors tab under Options > Preferences. For more information, see Specify Text Editor.

Support for Windows 8 and Windows Server 2012

Polyspace supports installation and analysis on Windows 8 and Windows Server® 2012 in compatibility mode.

Before installing the product in these operating systems:

  • Right-click setup.exe and select Properties.

  • Select the Compatibility tab.

  • Check the Run this program in compatibility mode for box and from the drop-down list, select Windows 7.

For further installation instructions, see Install the Polyspace Software.

Polyspace Server for Ada Product

Support for Windows 8 and Windows Server 2012

Polyspace supports installation and analysis on Windows 8 and Windows Server 2012 in compatibility mode.

Before installing the product in these operating systems:

  • Right-click setup.exe and select Properties.

  • Select the Compatibility tab.

  • Check the Run this program in compatibility mode for box and from the drop-down list, select Windows 7.

For further installation instructions, see Install the Polyspace Software.

R2013b

New Features, Bug Fixes

Polyspace Client for Ada Product

Display call context analysis within a procedure

The software displays call context information for checks contained in a given procedure. For example, if one call of the procedure results in a red check, and another call results in a green check, the call information and color for both calls is kept in the procedure check.

User interface support for Japanese language

The software supports a Japanese user interface.

Project level statistics such as code covered by verification and itemization of checks

In R2013b, in the Project Manager interface, percentage code covered by verification and check distribution are shown in a graphic format in the Verification Statistics view.

  • Code covered by verification — Ratio of unproven code lines to total code lines, expressed as a percentage. Shown in a column graph format.

  • Check distribution — Number of checks of each color. Shown in a pie chart format.

New "results statistics" in the results review user interface

In R2013b, in the Results Manager interface, percentage code covered by verification and check distribution are shown in a graphic format in the Results Statistics view.

  • Code covered by verification — Ratio of unproven code lines to total code lines, expressed as a percentage. Shown in a column graph format.

  • Check distribution — Number of checks of each color. Shown in a pie chart format.

Improved filtering, grouping and ordering of results in "results summary" view

In R2013b, the Results Summary and the Results Explorer view have been merged into a more organized Results Summary view.

  • In the Results Summary view, the error names are shown in an expanded format. Previously, a division-by-zero error appeared as ZDV.num in the Results Explorer view. Now it appears as Division by Zero in the revised Results Summary view.

  • You can now group checks by File/Function,Check and Package. In addition to check color, grouping by Check divides checks into categories related to the origin of the check, such as Control flow, Data flow, and Numerical.

  • You can now filter checks by File, Package and Function, in addition to existing filters. You can filter checks using the columns in the Results Summary view. If you have applied a filter, the column heading changes to indicate that all results are not displayed. You can also define custom filters.

  • You can use one of four predefined methodologies to restrict number and type of checks displayed (replacing review levels 0,1,2, and 3). The methodologies are :

    • First checks to review

    • Methodology for Ada > Light

    • Methodology for Ada > Moderate

    • All checks

    You can also use custom methodologies to restrict checks displayed.

  • You can navigate the Results Summary view using the keyboard or GUI buttons. Both means of navigation respect the grouping, filters, and methodology used to display results.

Project configuration file extension renamed

The software saves project configuration files with the .psprj extension. Previously, the file extension was .cfg.

No generation of Excel output

In R2013b, the following features are not supported:

  • Export of review comments to an Excel® spreadsheet.

  • Generation of Excel reports for verification results.

Starting an R2013a remote verification

If the R2013a and R2013b versions of Polyspace are installed on a client computer, submitting a R2013a remote verification from the client generates an error. For example:

/etc/Polyspace/polyspace.conf, line 7: Error: Duplicate entry for Polyspace for Ada 6.5 (R2013a).

As a temporary workaround, remove the R2013b version from the client configuration:

  1. Select Options > Metrics and Remote Server Settings.

  2. In the Polyspace Server Settings section, remove the product entry for R2013b.

  3. Click Apply.

Changes to verification results

None

Changes to analysis options

Changes to existing options

The -max-processes option is available only from the command line.

Options removed

The option -code-metrics has been removed. By default, the software computes code complexity metrics.

Polyspace Server for Ada Product

Call context analysis during verification of procedure

The software considers context in the analysis of a procedure. For example, if one call of the procedure results in a red check, and another call results in a green check, the call information and color for both calls is kept in the procedure check.

Polyspace Remote Launcher Manager dialog box renamed

To configure your Polyspace server, use the Metrics and Remote Server Settings dialog box. Previously, this dialog box was called the Polyspace Remote Launcher Manager.

The name of the line command, polyspace-rl-manager, is unchanged.

R2013a

New Features, Bug Fixes

Polyspace Client for Ada Product

Modified Polyspace installer

In R2013a:

  • The Polyspace installer does not create the Polyspace_Common folder.

  • The Polyspace product does not depend on environment variables, that is, the installer does not create POLYSPACE_* variables.

  • The Remote Launcher Manager does not open automatically during the installation process. In addition, if the service or daemon was running before the installation of the new product, the service or daemon is not automatically restarted. You must manually open the Remote Launcher Manager, configure your Polyspace Server, and then start the service or daemon.

  • You must manually install Polyspace plug-in (or add-in) files. The Polyspace installer does not automatically activate these files. For example, before you run a verification from the Eclipse IDE, you must manually install the Polyspace plug-in file.

The following table provides information about new locations for files and folders.

Binary filesLocation in previous releaseLocation in R2013a
Polyspace verification environment

Polyspace_Install\PVE\Polyspace.exe

Polyspace_Install/PVE/bin/polyspace

Polyspace_Install\polyspace\bin\polyspace[.exe]

Polyspace for Ada

Polyspace_Install\Verifier\wbin

Polyspace_Install/Verifier/bin

Polyspace_Install\polyspace\bin
Spooler

Polyspace_Common\RemoteLauncher\wbin\PSQueueSpooler.exe

Polyspace_Common/RemoteLauncher/bin/polyspace-spooler

Polyspace_Install\polyspace\bin\polyspace-spooler[.exe]
Polyspace plug-in for EclipsePolyspace_Common\PolyspaceForEclipse Polyspace_Install\polyspace\plugin\eclipse

Polyspace plug-in for IBM® Rational® Rhapsody®

Polyspace_Common\PolyspaceUMLLinkPolyspace_Install\polyspace\plugin\rhapsody
Remote Launcher Polyspace_Common\RemoteLauncher Polyspace_Install\polyspace\bin
Report GeneratorPolyspace_Common\ReportGenerator Polyspace_Install\polyspace\bin\polyspace-report-generator

Verification uses native binary file

In R2013a, the Polyspace verification is run using the native binary file for your computer architecture. Previously, you specified a 32-bit or 64-bit verification through the option -machine-architecture option_value. Now, if you specify -machine-architecture, the software ignores the option and generates the following warning:

Option "-machine-architecture option_value" is obsolete.
Verification run using native binary file for your computer architecture.

Previously, the default option value (auto) specified 32-bit verification. Now, on a Linux system, the Polyspace verification is 64-bit. You may observe an increase in verification time compared to previous releases. The increase depends on the application being verified and the architecture of your machine.

    Note:   For Linux systems, only the Polyspace 64-bit Client and Server products are supported.

Exact representation of floating point numbers

Polyspace uses the exact value of a representable floating point number during code verification. Consider the floating point value of 1.0. Previously, Polyspace represented this value as a range 0.9999 – 1.0001. Now, Polyspace uses the exact value, that is 1.0.

Changes to verification results

None

Changes to analysis options

New options

None

Changes to existing options

None

Options removed

The -machine-architecture option has been removed. See Verification uses native binary file.

Polyspace Server for Ada Product

Improved Polyspace Metrics security with HTTPS

You can now configure the Polyspace Metrics Web server with a secure HTTPS protocol. This configuration enables encrypted communication between the Polyspace server and the Polyspace Metrics Web interface. See Configure Polyspace Metrics Web Interface.

R2012b

New Features, Bug Fixes

Polyspace Client for Ada Product

Review of verification results improvement

Check filters in results summary view

The Results Summary toolbar provides check filters, which previously were available only in the Results Explorer view.

You can apply the check filters from either view. For example, if you filter checks by color and category in the Results Summary view, the software also filters out these checks from the Results Explorer view. For more information, see Filtering Checks.

Justify and comment a group of checks

You can now select a group of checks in either the Results Explorer or Result Summary view, and then justify and add review information to those checks. For more information, see Reviewing and Commenting Checks.

Variable values in tooltips

The display of variable values in Source view tooltips is improved, providing information that narrows the range of the variable. For example, the tooltip might indicate whether the variable values are multiples of a number. The following table has examples of how tooltips display variable range values.

PreviouslyR2012b
0 or 2 or 4 or [6 .. 2147483642 (0x7FFFFFFA)] even values in [0 .. 2147483642 (0x7FFFFFFA)]
[-56 ..110] or [112 .. 166] even values in [-56 .. 166]
[-1265 .. -46] or -23 or 0 multiples of 23 in [-1265 .. 0]
[0 .. 22] or 44 0 or 22 or 44

You might also see the following type of tooltip for variables:

1008 or 4800 or 14400 or 23040 (values are multiples of 48)

This enhancement might affect the contents of the text file Your_Project_Variable_View.txt file, which your verification generates in the …\results\Polyspace-Doc folder. Instead of only an interval list for a variable, you might see, for example, the following conventions in the file:

  • multiples of (a constant) in (the interval list)

  • even values in (the interval list)

  • odd values in (the interval list)

Reorganized Configuration pane

The Project Manager perspective of the Polyspace verification environment provides a reorganized Configuration pane that allows improved management of verification options.

The configuration process for code verification consists of different parts, for example, specifying your target environment and compiler behavior. The Configuration pane contains a tree with nodes that represent different parts of the configuration process. For example, to choose your target environment and compiler, select the Target & Compiler node and then specify your options.

You can specify the following option from the command line or through the Configuration > Machine Configuration > Non-official options field.

From command lineRemoved from Configuration pane
-keep-all-filesKeep all preliminary results files

Polyspace plug-in for Eclipse with GNATbench

The Polyspace plug-in for the Eclipse IDE now supports Ada projects generated by GNATbench.

You can run verifications for Ada projects from the Eclipse IDE. However, Polyspace settings are not extracted from the Eclipse project.

Report content filtering

Previously, you used the MATLAB® Report Generator™ software to apply filters to report templates through only the Run-time Check Details Ordered by Color/File component. The software provides a new component, Report Customization (Filtering), which allows you to apply filters from any point of the report hierarchy.

For more information, see Customizing Verification Reports.

Parent folder for verification results

You can now specify a parent folder for your verification results through the Project and result folder tab of the Polyspace Preferences dialog box. If you do not specify a parent folder, the software uses the active module folder as the parent folder. For more information, see Specify Parent Folder for Results.

Support for relative paths

The Polyspace Project Manager now supports relative paths outside the project hierarchy. For example, paths for source files in a folder above the project location. Previously, relative paths were supported only for subfolders of the project.

Absolute paths are still supported.

Intermediate verification level support

From the Polyspace verification environment, you can no longer specify the value CDFA or "Control and Data Flow Analysis" for the option -to. If this value is specified in a project configuration file (.cfg), the software replaces the value with compile or "Source Compliance Checking". However, from the command line, you can still specify CDFA or "Control and Data Flow Analysis" for -to.

Automatic import of comments and justifications

You can specify the batch option -import-comments polyspace_results_folder_path to automatically import comments and justifications from a previous verification. For more information, see Batch Options.

Storage of temporary files

If you specify the new option -tmp-dir-in-results-dir, Polyspace does not use the standard /tmp or C:\Temp folder to store temporary files. Instead, Polyspace uses a subfolder of the results folder. If the results folder is mounted on a network drive, this action might affect processing speed. Use this option only when the temporary folder partition is not large enough and troubleshooting is required.

For more information, see Batch Options.

Removal of Polyspace in One Click

The Polyspace in One Click feature will be removed in a future release.

Changes to verification results

None

Changes to analysis options

New options

None

Changes to existing options

Analysis options have been reorganized in the Project Manager. See Reorganized Configuration pane.

OptionProject Manager perspectiveSee also ...
Previous labelR2012b labelLocation on R2012b Configuration pane
-add-to-results-repositoryAdd automatically to results repositoryAdd to results repository Machine Configuration 
-array-expansion-sizeMax size of global array variablesUnchangedPrecision 
-base-type-directly-visibleRemove comparison operators ambiguitiesUnchangedTarget & Compiler 
-code-metricsCalculate code metricsCalculate code complexity metricsCode Metrics 
-continue-with-all-nivContinue after non initialized variablesUnchangedVerification Assumptions 
-continue-with-in-out-nivContinue with non-initialized in/out parametersUnchangedVerification Assumptions 
-critical-section-begin and -critical-section-endCritical section detailsUnchangedVerification Mode 
-DDefined Preprocessor MacrosPreprocessor definitionsTargets & Compler > Macros  
-data-range-specificationsVariable/function range setupUnchangedVerification Mode > Inputs & Stubbing 
-entry-pointsEntry points or interruptionEntry pointsVerification Mode 
-export-are-not-volatileTreat export as non volatileUnchangedVerification Assumptions 
-extensions-for-spec-filesFiles extensionsUnchangedTarget & Compiler  
-extra-flags Non-official optionsMachine Configuration 
-ignore-float-roundingIgnore float roundingUnchangedVerification Assumptions 
-import-are-not-volatileTreat import as non volatileUnchangedVerification Assumptions 
-init-stubbing-vars-random or -init-stubbing-vars-zero-or-randomInitialize of uninitialized global variablesInitialization of uninitialized global variablesVerification Mode > Inputs & Stubbing  
-keep-all-filesKeep all preliminary results filesCommand line only  
-known-NTCFunctions known to cause NTCProcedures known to cause NTCVerification Assumptions  
-machine-architectureRun verification in 32 or 64-bit modeUnchangedMachine Configuration 
-main-generatorGenerate a mainVerify moduleVerification Mode 
-max-processesNumber of processes for multiple core systemUnchangedMachine Configuration 
-modules-precisionSpecific precisionUnchangedPrecision 
-no-automatic-stubbingNo automatic stubbingUnchangedVerification Mode > Inputs & Stubbing 
-OPrecision LevelPrecision levelPrecision 
-OS-targetTarget operating systemUnchangedTarget & Compiler 
-path-sensitivity-deltaImprove Precision of interprocedural analysisUnchangedPrecision 
-permissivePermissiveCommand line only  
-post-analysis-commandCommand to apply after the end of the verificationUnchangedPost Verification 
-pre-analysis-commandCommand/script to apply before start of the code verificationUnchangedEnvironment Settings 
-report-output-formatReport output formatOutput formatReporting 
-report-templateReport templateReport template nameReporting 
-serverSend to Polyspace ServerUnchangedMachine Configuration 
-storage-unitValue of the constant Storage_UnitUnchangedTarget & Compiler 
-strictStrictCommand line only  
-targetTarget processor typeUnchangedTarget & Compiler 
-temporal-exclusions-fileTemporal exclusion pointTemporally exclusive tasksVerification Mode 
-timeoutVerification time limitUnchangedPrecision 
-toTo end ofVerification levelPrecisionIntermediate verification level support
-UUndefined Preprocessor MacrosUndefine preprocessor definitionsTargets & Compler > Macros 
-unit-by-unitRun a verification unit by unitRun unit by unit verificationVerification Mode 
-unit-by-unit-common-sourceUnit by unit common source filesUnchangedVerification Mode 
-variables-expansion-depthExpansion limit for a structureUnchangedPrecision 
-variables-to-expandVariables to expandUnchangedPrecision 

Options removed

None

Polyspace Server for Ada Product

Password-protected access to projects in Polyspace Metrics

You can now restrict access to a project by specifying a password:

  • When you run a verification with Polyspace Metrics enabled or upload results to the Polyspace Metrics repository.

  • After the creation of a project.

For more information, see Protect Access to Project Metrics.

R2012a

New Features, Bug Fixes, Compatibility Considerations

Polyspace Client for Ada Product

Compilation Environment Templates

Polyspace software now provides predefined compilation environment templates to help you configure verification projects.

These templates automatically set analysis options for the selected compiler, and help you locate the required include folders.

When creating a new project, you can select a template for your compiler.

For more information, see Creating a Project.

Predefined Templates

Predefined templates are available for:

  • Aonix – Ada 95 Application Targeting the Aonix Compiler

  • Baseline – Generic Ada95 application

  • Gnat – Ada 95 Application Targeting the Gnat Compiler

  • Greenhills – Ada 95 Application Targeting the Greenhills Compiler

  • Rational – Ada 95 Application Targeting the Rational Compiler

Custom Templates

You can also create custom templates from existing Project configurations, and use them to configure future projects.

For more information, see Creating Custom Project Templates.

Suppression of NTC, NTL and UNR Checks Caused by Red Checks

Previously, the software would generate red NTC and NTL checks that were a consequence of other red checks. Now, the software does not generate these red checks. However, the software still gives the information that these red checks provided. The software highlights the corresponding call or loop identifier by applying a dashed underline to the identifier.

If the cause of the problem is known, the software provides this information in a tooltip for the underlined call or loop identifier. In addition, when you right-click the identifier, the context menu provides a Go to Cause item. Selecting this item takes you to the red check that is the cause.

The software:

  • Does not generate gray UNR checks if the cause is a red check

  • Still generates red NTC, NTL, and K-NTC checks for a call or loop identifier if the corresponding code contains orange checks.

  • Does not generate NTC checks for the statements exit and abort, but provides tooltips for these statements. For example, abort, which does not correspond to an error, prevents the execution of a sequence of statements.

Compatibility Considerations

As a result of this new feature, you might observe a significant reduction in the total number of red and gray checks when compared to previous versions of the software.

Redefinition of Successful Verification

Previously, if a Polyspace verification failed, for example, during pass1 (Software Safety Analysis level 1), the software communicated the failure through log messages and the Project Browser. However, if you clicked the xx_LAST_RESULTS.exe file within the Project Browser, the software displayed any results (colored checks) that had been generated by the verification. Now, the software deems a verification successful provided some results have been generated.

Polyspace Report Generator Enhancements

You can:

  • Generate multiple reports in the Results Manager perspective. See Generating Verification Reports.

  • Customize report templates with MATLAB Report Generator software, which allows you to filter results by:

    • Justification status — Display all, justified, or unjustified checks.

    • Type — Display only listed types of run-time checks.

    • Function — Display only run-time checks from specified functions.

    For more information, see Customizing Verification Reports.

Polyspace In One Click (POC) Enhancement

The POC software has been rewritten. The software that replaces the previous Send To functionality now runs verifications without requesting additional settings. See Using Polyspace In One Click.

    Note:   Support for the Send To feature will be removed in a future release.

Header Files Without Run-Time Checks

It is quite common for code to contain header files with library inline functions that are never called. Previously, these files were listed in the Results Explorer view, which could slow down your review of results. Now, if header files do not contain run-time checks, the software does not list these header files in the Results Explorer view.

Improved Access to Polyspace Demos

In the Polyspace verification environment, you can now open supplied Demo projects through the Help menu.

Changes to Verification Results

Compatibility Considerations

Verification results might change when compared to previous versions of the software. Some checks might change color, and the Selectivity rate of your results might change.

Changes to Analysis Options

New Options

None

Changes to Existing Options

No name changes to existing options

Options Removed

None

Polyspace Server for Ada Product

Enhanced Polyspace Metrics Project Index

The enhanced project index enables you to display projects as categories, which is useful when you have a large number of projects to manage. Now, you can:

  • Create multiple-level project categories.

  • Move projects between categories by dragging and dropping projects.

  • Rename and remove categories. You can remove categories without deleting the projects within the categories. The software moves these projects back to the root level.

For more information, see Organizing Polyspace Metrics Projects.

Redefinition of Successful Verification

Previously, if a Polyspace verification failed, for example, during pass1 (Software Safety Analysis level 1), the software communicated the failure through log messages and the Project Browser. However, if you clicked the xx_LAST_RESULTS.exe file within the Project Browser, the software displayed any results (colored checks) that had been generated by the verification. Now, the software deems a verification successful provided some results have been generated.

R2011b

New Features, Bug Fixes, Compatibility Considerations

Polyspace Client for Ada Product

Review Orange Checks that are Potential Run-Time Errors

Previously, there were two modes in which you could review verification results — manual and assistant. For the manual mode, you set the Assistant slider to Off and the software displayed all orange checks (in addition to the red and green checks) . With the assistant mode, there were three levels of review — corresponding to settings 1, 2, and 3 of the Assistant slider. You could specify the number of orange checks to display through the Assistant Configuration tab in the Polyspace Preference dialog box.

Now, Polyspace allows you to review results at five different levels. You can set the Review slider to 0, 1, 2, 3, or All:

  • 0 — Display red and gray checks. In addition, display orange checks that are potential run-time errors. On the Polyspace Preference > Review Configuration tab, you can specify the type of potential run-time errors that you are interested in. You have the option of not displaying any orange checks.

  • 1, 2, and 3 — This functionality is unchanged. Display red, gray, and green checks. In addition, display orange checks according to values specified on the Polyspace Preference > Review Configuration tab.

  • All — Display red, gray, green, and all orange checks.

The Assistant Configuration tab is renamed the Review Configuration tab.

No Gray Checks in Unreachable Code

The only gray checks that Polyspace generates now are UNR checks for unreachable branches of code. In addition, Polyspace generates the UNR check only at the highest level of a branch. You no longer see nested UNR checks , that is, UNR checks in sub-branches.

In addition, the software displays two new metrics for the project in the procedural entities view:

  • 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.

See Results Explorer Tab.

Compatibility Considerations

Due to the removal of non-UNR gray checks and nested UNR checks, verification results may change when compared to previous versions of the software.

Global Variable Range Information

In the Variable Access pane, Polyspace displays range information for read and write access operations on global variables within each source file. Previously, the displayed value was the union of all access operations on the global variable within a file. The software did not display range information for individual operations. Now, for global variables that are signed or unsigned integers, Polyspace also provides range information for the individual access operations from which the union value is obtained.

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 new filter button . See Variable Access Pane.

Run All Verifications in Project

You can have many verifications within a project, each verification being associated with an active configuration. Previously, you could only run one verification at a time from the Polyspace verification environment (PVE). Now, if you select a project and click the button , Polyspace will run all verifications in the project. See Running a Verification.

Green NIV check for Unchecked_Conversion Function

Previously, the software produced an orange NIV check for each call to an instance of the Ada generic library function Unchecked_Conversion. Now by default, the software produces a green NIV check for each call. If you want to revert to the previous behavior, run your verification with the option -D POLYSPACE_UNCHECKED_CONVERSION_NO_INIT.

Polyspace Server for Ada Product

Running Multiple Verifications Simultaneously

If you purchase more than one license for a Polyspace server, you can now configure the server to run multiple verifications at the same time. This can improve the performance of server verifications.

To configure your server to run multiple verifications, open the Remote Launcher Manager, then set the Number of Polyspace verifications that can run simultaneously on this server to the number of licenses you have activated for your server.

Compatibility Considerations

If you configure your server to run more than one verification simultaneously, the server will not be able to run verifications using older versions of the software.

For example, if your server has both R2011a and R2011b software installed, you cannot run a verification using the R2011a software.

Polyspace Metrics

Review Changes between Results of Successive Verifications

You can specify a version of a project and review only the differences between verification results of the specified version and the previous verification. See Review New Findings.

File Modules with Quality Levels

If you have projects with two or more file modules in the Polyspace verification environment, by default Polyspace Metrics displays verification results using the same module structure. However, Polyspace Metrics also allows you to create or delete file modules. You can group files into a module and specify a quality level for the module, which applies to all files within the module. This feature allows you to specify different quality levels for your files in the review of verification results. See Creating a File Module and Specifying Quality Level.

Enhanced Graphs and Charts

Polyspace Metrics displays enhanced graphs and charts.

If you specify a range of project versions:

  • On the Summary tab, Run-Time Defects are plotted as separate categories, High, Medium, and Low.

  • On the Run-Time Checks tab:

    • Under Confirmed Defects, you see separate plots for the defect categories, High, Medium, and Low.

    • Under Run-Time Findings, you see separate plots for red checks, NTC checks, and gray checks.

If you specify a single version of a project, Polyspace Metrics displays file defect information, ordering the files according to the number of defects in each file. Use the new # items field to specify the maximum number of files for which information is displayed. See Displaying Metrics for Single Project Version.

R2011a

New Features, Bug Fixes, Compatibility Considerations

Polyspace Client for Ada Product

Code Metrics

Polyspace Metrics now generates Ada code metrics, giving you the number of:

  • Protected shared variables

  • Unprotected shared variables

  • Files

  • Lines of code

  • Packages

  • Packages that appear in with statements

  • Subprograms that appear in with statements

You can view the metrics by:

  • Using a Web browser to access the Code Metrics view of your project in Polyspace Metrics

  • Examining the XML file that the software generates

Saving Polyspace Metrics Review

Previously, when you saved your project (Ctrl+S) after a review of results from Polyspace Metrics, the software would save your comments and justifications both locally and in the Polyspace Metrics repository.

Now, if you save your project (Ctrl+S), the software saves your review to a local folder only. A new button is available on the Run-Time Checks toolbar. If you click this button, the software saves your comments and justifications to a local folder and the Polyspace Metrics repository.

This feature allows you to upload your review to the repository only when you are satisfied that your review is, for example, correct and complete.

You can still configure your software to display the previous behavior.

Support for Rational and Aonix Compilers

The software now provides support for the IBM Rational Apex and Aonix® compilers. For more information, see Operating system target for Standard Libraries compatibility in the Polyspace Products for Ada Reference.

Multi-Core Support

On multi-core computers, you can reduce verification time by specifying the use of core processors simultaneously to perform the verification. The software provides a new command line option –max-processes, which uses a default value of 4. You can specify any value between 1 and 128. For more information, see Number of processes for multiple CPU core systems in the Polyspace Products for Ada Reference.

Generated Main with Explicit Tasks and Accept Statements

If you select the option Generate a main and there are explicit tasks in the source code, then task bodies are verified like subprograms and accept statements are not executed. After verification, code associated with the accept statements is gray. For more information, see Generate a main in the Polyspace Products for Ada Reference.

Compatibility Considerations

Previously, if there were explicit tasks and accept statements in the source code, a verification run could have generated red, green, or orange checks for code within the accept statements. Now, verification colors the code within these accept statements gray.

Enhancements in Run-Time Checks Perspective

Within the source code view, you can investigate checks with tooltips that provide range information about variables.

In addition, when you click a check, the software provides information about the check in the Review Details pane.

Compatibility Considerations

Because of these enhancements, the IPT and VOA checks are no longer required, and the software does not generate these checks anymore.

UOVFL and UNFL Checks Removed

The software no longer generates UOVFL and UNFL checks, but generates OVFL checks in place of these checks.

Compatibility Considerations

Due to the replacement of UOVFL and UNFL checks by the OVFL check, the number of green checks may decrease when compared with previous versions of the software. For example, a combination of an orange OVFL and a green UNFL generated by a previous version may be replaced by a single orange OVFL.

NIV Checks for Universal Constants

The software now generates NIV checks for read operations on universal constants. If the constants are used in your code, the NIV checks are green. If the constants are in unreacheable code, the NIV checks are gray.

Compatibility Considerations

This enhancement may change the check metrics and selectivity of the verification. The number of green and gray checks may be higher compared to the number generated by previous versions of the software.

Variable Range Inconsistency between Variable Access Pane and Tooltips

The range given for a variable in the Variable Access Pane (Variables View) can differ from the range given by tooltips on the reads of a variable in the Source code view. The range provided by the tooltip will be wider than the range given in the Variables View.

This difference is due to imprecision in the tooltip. The Variables View provides the correct range for the variable.

For example:

  • Variables View states that variable X is in range [0..4000]

  • Tooltip on a read of X states that the range is [0,7000].

In this case, [0..4000] is the correct range. The tooltip range is caused by imprecision that may be fixed in future releases.

Verification Time Limit

You can now specify a time limit for verifications using the -timeout option. If the verification does not complete within the specified time, the verification fails.

For more information, see "Verification Time Limit" in the Polyspace Products for Ada Reference.

Automatic Addition of Specifications for Selected Source Files

When launching a verification from the Eclipse IDE or the Polyspace Verification Environment, the software automatically searches for the package specifications associated with the selected source files, and adds them to the set of sources to verify.

As a result, the verification may contain more source files than you select.

Stubbed Tasks

Programs with stubbed tasks, such as those using Ada rendezvous, previously caused compilation errors. These programs can now be verified.

Scaling Issue for Large Applications with Nested Structures/Arrays

With R2011a, you may experience scaling problems for large applications that manipulate strongly nested structures or arrays. When verifying such applications, the verification may fail during the "Software Safety Analysis Level 0" phase. No verification results are generated, although the data dictionaries (Variable View and Call-Graph View) are accessible.

With previous releases, such applications could be verified, but the verification required several days to complete, and produced results with very low selectivity.

If you experience this problem, try performing a unit-by-unit verification. For more information, see Running Verification Unit-by-Unit in the Polyspace Products for Ada User's Guide.

Compatibility Considerations

Verification may fail for code that was previously verified with an earlier version of the product.

Product Name Change in Files and Folders

The Polyspace product name has changed from "PolySpace" to "Polyspace" in R2011a. This change impacts the name of all files and folders created by the software.

For example:

  • PolySpace-Doc folder has changed to Polyspace-Doc

  • PolySpace_xxxx.log file has changed to Polyspace_xxxx.log

Compatibility Considerations

If you have existing folders that use the previous product name (for example, PolySpace/PolySpace_Common) the R2011a installation will continue to use these existing folders. However, files or folders created during or after installation will use the new name.

If you have shortcuts or scripts that are case-sensitive, you should update them to use the new name.

License Manager Support

The License Manager for Polyspace products has been upgraded to FlexNet® 11.9.

You may need to upgrade your FlexNet server and daemon.

Changes to Verification Results

Compatibility Considerations

Verification results may change when compared to previous versions of the software. Some checks may change color, and the Selectivity rate of your results may change.

Refer to the following sections for information on the specific changes.

Write Access in Data Table with Main Generator and Protected Objects

In previous releases, when using the -main-generator option, an incorrect write access could appear in the data-table when entries of protected objects were called.

In R2011a, the data-table no longer includes locations with critical section names.

There may be less write accesses with protected objects that have defined entries when you use the option -main-generator.

NIV for Variables Initialized at Declaration

In previous releases, there is no NIV check when a variable is initialized at the declaration.

In R2011a, verification always puts NIV checks on variables and constants. OVFL checks are not put on constants.

The total number of checks may change when compared with previous releases.

Range Error with greenhills OS Target

In previous releases, verification could report a false red when using "Ada.interrupts.Interrupt_ID" in source code designed for the greenhills compiler.

In R2011a, when you use the type Ada.interrupts.Interrupt_ID, and set the -OS-target to greenhills, the bounds of the type Interrupt_ID have changed.

Verification results may change when compared to previous versions of the software. Some checks may change color, and the Selectivity rate of your results may change.

UOVFL and UNFL Checks Removed

The software no longer generates UOVFL and UNFL checks, but generates OVFL checks in place of these checks.

The number of checks may decrease compared to previous versions of the software.

NIV Checks for Universal Constants

The software now generates NIV checks for read operations on universal constants. If the constants are used in your code, the NIV checks are green. If the constants are in unreacheable code, the NIV checks are gray.

Verification results may change when compared to previous versions of the software. The number of green and gray checks may be higher compared to the number generated by previous versions of the software.

Constants Defined in Package System

In previous releases, constants defined in package system were ignored.

For example:

Max_Binary_Modulus    : constant := 16#100000000#; 
Max_Nonbinary_Modulus : constant := 16#FFFFFFFF#; 
In R2011a, values of constants defined in the package system that are used in the program to be verified are taken into account for the verification. This may impact the results.

Initialization of Variables Declared and Assigned in Specs

In previous releases, verification could incorrectly report a red ZDV check for a variable of a type with default values, when the variable is global.

In R2011a, when using the option -main-generator, components with initial values of global variables of composite types that are not initialized are considered full range.

Verification results may change when compared to previous versions of the software. Some checks may change color, and the Selectivity rate of your results may change.

Parameterless Protected Procedure as Entry Point

In previous releases, when a parameterless protected procedure is used as an entry point via the option -entry-points, the verification fails.

In R2011a, parameterless protected procedures applied to a global object are now accepted as values of the option -entry-points.

Changes to Analysis Options

New Options

Changes to Existing Options

None

Deprecated Options

None

Polyspace Server for Ada Product

Code Metrics

Polyspace Metrics now generates Ada code metrics, giving you the number of:

  • Protected shared variables

  • Unprotected shared variables

  • Files

  • Lines of code

  • Packages

  • Packages that appear in with statements

  • Subprograms that appear in with statements

You can view the metrics by:

  • Using a Web browser to access the Code Metrics view of your project in Polyspace Metrics

  • Examining the XML file that the software generates

Saving Polyspace Metrics Review

Previously, when you saved your project (Ctrl+S) after a review of results from Polyspace Metrics, the software would save your comments and justifications both locally and in the Polyspace Metrics repository.

Now, if you save your project (Ctrl+S), the software saves your review to a local folder only. A new button is available on the Run-Time Checks toolbar. If you click this button, the software saves your comments and justifications to a local folder and the Polyspace Metrics repository.

This feature allows you to upload your review to the repository only when you are satisfied that your review is, for example, correct and complete.

You can still configure your software to display the previous behavior.

Multi-Core Support

On multi-core computers, you can reduce verification time by specifying the use of core processors simultaneously to perform the verification. The software provides a new command line option –max-processes, which uses a default value of 4. You can specify any value between 1 and 128.

Generated Main with Explicit Tasks and Accept Statements

If you select the option Generate a main and there are explicit tasks in the source code, then task bodies are verified like subprograms and accept statements are not executed. After verification, code associated with the accept statements is gray. For more information, see Generate a main in the Polyspace Products for Ada Reference.

Compatibility Considerations

Previously, if there were explicit tasks and accept statements in the source code, a verification run could have generated red, green, or orange checks for code within the accept statements. Now, verification colors the code within these accept statements gray.

Automatic Comment Import for Server Verifications

When you download results from the Polyspace server, the software now automatically imports any comments from results in the destination folder into the downloaded results (except for verifications using the option -add-to-results-repository).

As a result of this change, you can now download intermediate results for a verification running on the Polyspace server, and add or edit comments on those results. When you later download the final results, your comments are preserved.

You can also download and comment on a single unit of a unit-by-unit verification, even if other units are still pending in the server queue. When you download the final results (which overwrites the earlier results), your comments are preserved.

License Manager Support

The License Manager for Polyspace products has been upgraded to FlexNet 11.9.

You may need to upgrade your FlexNet server and daemon.

R2010b

New Features, Bug Fixes, Compatibility Considerations

Polyspace Client for Ada Product

Polyspace Graphical User Interface

Redesigned Polyspace graphical user interface replaces the Launcher and Viewer modules with a single, unified interface called the Polyspace verification environment (PVE).

You use the Polyspace verification environment to create Polyspace projects, launch verifications, and review verification results. The new interface also enables you to provide comments in the source code or in the results.

The Polyspace verification environment consists of two perspectives:

Project Manager Perspective

The Project Manager perspective allows you to create projects, set verification parameters, and launch verifications.

For information on using the Project Manager perspective, see Setting Up a Verification Project in the Polyspace Products for Ada User's Guide.

Run-Time Checks Perspective

The Run-Time Checks perspective allows you to review verification results, comment individual checks, and track review progress.

For information on using the Run-Time Checks perspective, see Reviewing Verification Results in the Polyspace Products for Ada User's Guide.

Data Range Specifications

The Data Range Specifications (DRS) feature allows you to set constraints on data ranges using a text file. With this text file, you can specify data ranges for global variables, stubbed functions and procedures, and function call inputs.

Extended Support for Tasks

You can now verify Ada code that contains the following task-related features :

  • Pointers to explicit tasks

  • Private task types

  • Tasks with discriminants

  • Entry families

  • Explicit tasks declared in a package – you can now verify the package with the -main-generator option

Previously, these features would generate errors during a verification.

Preprocessor Macros for Compilation

You can now specify, with the -D option, the use of preprocessor macros in code compilation. The -U option, which nullifies this -D option, is also available.

New Options to Classify Run-Time Checks

When reviewing results in the Run-Time Checks perspective, the software now provides additional options for classifying checks

After you review the check, you can specify the following:

  • Classification – Select an option to describe the seriousness of the issue.

  • Status – Select an option to describe how you intend to address the issue.

  • Justified – Select the check box to indicate that you have justified this check.

  • Comment – Enter additional information about the check

The software provides pre-defined values for Classification and Status. You can also define your own statuses.

In addition to reviewing checks through the user interface, you can place comments in your code that highlight and categorize checks identified in previous verifications. The software displays the information that you provide within your code comments, and marks the checks as Justified.

Compatibility Considerations

The syntax for code comments has changed to reflect the new options for categorizing checks.

The syntax for run-time checks is now:

-- polyspace<RTE:RTE1 : [Classification] : [Status] > [Comment]

If you placed comments in your code using the previous syntax, the comments will still appear in your results, but the text may be displayed in different columns.

For more information, see Syntax for Run-Time Errors in the Polyspace Products for Ada User's Guide.

Permissiveness on File and Folder Names

Polyspace software now allows space characters in the names of Projects, source files, and folders, as well as in option arguments.

In addition, multiple source files with the same name are now allowed.

    Note:   Non-ASCII characters in file names are not supported.

Default Target Processor

The default setting of the Target processor type (-target-processor) option has changed from SPARC to i386.

Compatibility Considerations

If you launch verifications without specifying a value for this option, the default value has changed. Therefore, your verification results may change when compared to previous versions of the software. Some checks may change color, and the Selectivity rate of your results may change.

Operating System Support

Added support for the Windows 7 operating system.

Solaris™ operating system is no longer supported for new installations.

For more information, see the Polyspace Installation Guide.

Polyspace Server for Ada Product

Polyspace Metrics Web Interface

A web-based tool for software development managers, quality assurance engineers, and software developers, which allows you to do the following in software projects:

  • Evaluate software quality metrics

  • Monitor the variation of code metrics, and run-time checks through the lifecycle of a project

  • View defect numbers, run-time reliability of the software, review progress, and the status of the code with respect to software quality objectives.

In addition, if you have the Polyspace Client™ for Ada product installed on your computer, you can drill down to run-time checks in the Polyspace verification environment. You can review these run-time checks and, if required, classify these checks as defects.

Automatic Verification

Configure verifications to start automatically and periodically, for example, at a specific time every night. At the end of each verification, the software stores results in a results repository and updates the metrics for your software project. You can also configure the software to send you an email at the end of the verification. This email contains links to results, compilation errors, run-time errors, or processing errors.

Operating System Support

Added support for the Windows 7 operating system.

Solaris operating system is no longer supported for new installations.

For more information, see the Polyspace Installation Guide.

R2010a

New Features, Bug Fixes

Polyspace Client for Ada Product

License Activation

Polyspace products now support the MathWorks software activation mechanism.

Activation is a process that verifies licensed use of MathWorks® products. The process validates your product licenses and ensures that they are used correctly. You must complete the activation process before you can use Polyspace software.

    Note:   If you are using Designated Computer (Individual) licenses, you must activate the license for each Polyspace system individually. However, if you are using Concurrent licenses for multiple Polyspace systems, you do not need to activate each Polyspace system. You activate the license once (for the FLEXnet license server), then provide license files for each Polyspace system.

The easiest way to activate the software is to log in to your MathWorks Account during installation. At the end of the installation process, the Polyspace Software Activation dialog box opens.

Follow the prompts in the Polyspace Software Activation dialog box to complete the activation process.

If you do not have a MathWorks account, you can create one during the activation process. To create an account, you must have an Activation Key, which identifies the license you want to install and activate.

If your Polyspace system is not connected to the internet, you can access the MathWorks License Center on a computer with internet access, activate your license, and download a license file for transfer to your Polyspace system. If you do not have access to a computer with an Internet connection, contact Customer Support.

For more information on how to activate your software, see Activating Polyspace Softwarein the Polyspace Installation Guide.

For more information on software activation, including frequently asked questions, refer to the MathWorks Web site: www.mathworks.com/support/activation/polyspace.html

Source Code Comment Support

Polyspace software now allows you to place comments in your code that provide information about known run-time errors. You can use these comments to highlight and categorize previously identified run-time errors. This information can then make the review process quicker and easier.

When you review verification results, the Viewer displays comments on individual checks. You can then skip these commented checks during the review process, or simply use them as additional information during your review.

Eclipse Integration

Polyspace integration with the Eclipse IDE, Version 3.4 and 3.5.

The Polyspace Client for Ada can be integrated with the Eclipse™ Integrated Development Environment through the Polyspace plug-in for Eclipse IDE.

This plug-in provides Polyspace source code verification and bug detection functionality for source code developed within Eclipse IDE. Features include the following:

  • A contextual menu that allows you to launch a verification of one or more files.

  • Views in the Eclipse editor that allow you to set verification parameters and monitor verification progress.

Operating System Support

Added support for the following Linux distributions:

  • OpenSuSE 11.1

  • Debian 5.x

  • Ubuntu 8.04, 8.10, 9.04, and 9.10

For more information, see the Polyspace Installation Guide.

Polyspace Server for Ada Product

License Activation

Polyspace products now support the MathWorks software activation mechanism.

Activation is a process that verifies licensed use of MathWorks products. The process validates your product licenses and ensures that they are used correctly. You must complete the activation process before you can use Polyspace software.

    Note:   If you are using Designated Computer (Individual) licenses, you must activate the license for each Polyspace system individually. However, if you are using Concurrent licenses for multiple Polyspace systems, you do not need to activate each Polyspace system. You activate the license once (for the FLEXnet license server), then provide license files for each Polyspace system.

The easiest way to activate the software is to log in to your MathWorks Account during installation. At the end of the installation process, the Polyspace Software Activation dialog box opens.

Follow the prompts in the Polyspace Software Activation dialog box to complete the activation process.

If you do not have a MathWorks account, you can create one during the activation process. To create an account, you must have an Activation Key, which identifies the license you want to install and activate.

If your Polyspace system is not connected to the internet, you can access the MathWorks License Center on a computer with internet access, activate your license, and download a license file for transfer to your Polyspace system. If you do not have access to a computer with an Internet connection, contact Customer Support.

For more information on how to activate your software, see Activating Polyspace Softwarein the Polyspace Installation Guide.

For more information on software activation, including frequently asked questions, refer to the MathWorks Web site: www.mathworks.com/support/activation/polyspace.html

Queue Manager Interface

The Polyspace Queue Manager Interface (Spooler) is now available on Linux machines, providing a graphical interface for managing verification jobs on the Polyspace server.

Operating System Support

Added support for the following Linux distributions:

  • OpenSuSE 11.1

  • Debian 5.x

  • Ubuntu 8.04, 8.10, 9.04, and 9.10

For more information, see the Polyspace Installation Guide.

R2009b

New Features, Bug Fixes, Compatibility Considerations

Polyspace Client for Ada Product

Report Generator

New Report Generator that presents Polyspace results in PDF, HTML, and other output formats.

The Polyspace Report Generator allows you to generate reports about your verification results, using the following predefined 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.

  • 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.

The Polyspace Report Generator allows you to generate verification reports in the following formats:

  • HTML

  • PDF

  • RTF

  • Microsoft® Word

  • XML

    Note:   Microsoft Word format is not available on UNIX platforms. RTF format is used instead.

Main Generator Enhancements

Enhanced main generator that considers the scope of a procedure and variable, improving error detection at the package level.

This change may affect your results compared with previous releases, and how you interpret the new results. Specific changes include:

  • Uninitialized package body variables are considered uninitialized

  • Uncalled package-scope procedures/functions are considered unreachable

  • Functions/procedures declared at the spec level are called only once

  • Uninitialized spec level variables are considered possibly uninitialized

For more information on the main generator, see Main Generator Overview in the Polyspace Products for Ada User's Guide .

Uninitialized Package Body Variables are Considered Uninitialized

Uninitialized variables that are declared only in the package body are now considered uninitialized, and generate red NIV checks.

Previously, these variables were considered initialized (green NIV) with full-range values. This behavior made interpretation of results easier and allowed verification to continue. However, the software now considers these variables uninitialized (red NIV) and stops verification at this point. This new behavior is more accurate with respect to the actual initialization state of the variables. You must correct the code before verification can continue. Alternatively, you can use the option -continue-with-all-niv.

Uncalled Package-scope Procedures/Functions are Considered Unreachable

Procedures and functions that are declared in the package but not called by code within the package body provided for the verification will now be considered unreachable (gray).

Previously, all procedures and functions in a package were considered for verification and subsequently colored. The argument for this behavior was that these functions and procedures could be called by code inside the package that had not been provided for the verification. Now, the software considers this code unreachable (gray) unless there is a path of execution that leads to it.

Functions/Procedures Declared at the Spec Level are Called Only Once

Functions or procedures declared at the specification level are called only once.

    Note:   This behavior changed in Release 2010a. In R2010a or later, the main generator can call a function several times.

Uninitialized Spec Level Variables are Considered Possibly Uninitialized

Uninitialized variables declared in a package specification will now be considered possibly uninitialized (orange NIV). Previously, these variables were considered initialized (green NIV) with full-range values.

The software now considers uninitialized variables that are declared only in the package body as uninitialized (red NIV). However, for uninitialized variables declared in a package specification, it is possible that packages that use these variables may initialize these variables. The software now recognizes this possibility and generates orange NIV checks for uninitialized variables declared in a package specification.

This behavior is not changed if you use options -init-stubbing-vars-random or -init-stubbing-vars-zero-or-random to initialize uninitialized variables. Specification-level variables will still be considered possibly uninitialized (orange NIV), because the packages that use these variables can alter the variables, even to the extent of uninitializing the variables.

Compatibility Considerations

Changes to the main generator may result in differences in your verification results, when compared with earlier versions of the software. If you verified your code with previous versions of the software (for example, R2009a), be aware of these changes, how they affect your colored results and the way you interpret the results.

Global Data Graphs

New Graphs (similar to concurrent access graphs) available for all global data.

You can display the access sequence for any variable that is read or written in the code. The access graph displays the read and write access for the variable.

Unit-by-unit Verification

New option to create a separate verification job for each source file in the project.

When you run a unit-by-unit verification, each source file is compiled, sent to the Polyspace Server, and verified individually.

The queue manager displays a job for the full verification group, as well as jobs for each unit (using a tree structure).

When verification is complete, you can download and view results for the entire project, or for individual units. When downloading a verification group, all the unit results are downloaded and a summary of the download status for each unit is displayed.

    Note:   Unit by unit verification is available only for server verifications.

Operating System Support

Added support for Windows Server 2008.

For more information, see the Polyspace Installation Guide.

Polyspace Server for Ada Product

Operating System Support

Added support for Windows Server 2008.

For more information, see the Polyspace Installation Guide.

R2009a

New Features, Bug Fixes

Polyspace Client for Ada Product

Character Encoding Options

New character encoding option allows you to view source files created on an operating system that uses different character encoding than your current system.

You specify the character encoding used by the operating system on which the source file was created using the Character encoding tab in the Preferences dialog box of the Polyspace Viewer.

Operating System Support

Added support for Windows Server 2003, Windows Vista™, and Red Hat Enterprise Linux Workstation v.5.

For more information, see the Polyspace Installation Guide.

Polyspace Server for Ada Product

Operating System Support

Added support for Windows Server 2003, Windows Vista, and Red Hat Enterprise Linux Workstation v.5.

For more information, see the Polyspace Installation Guide.

R2008b

New Features, Bug Fixes

Polyspace Client for Ada Product

Operating System Support

Added support for 64–bit Linux.

For more information, see the Polyspace Installation Guide.

Polyspace Server for Ada Product

Operating System Support

Added support for 64–bit Linux.

For more information, see the Polyspace Installation Guide.

R2008a

New Features, Bug Fixes, Compatibility Considerations

Polyspace Client for Ada Product

Removed Cygwin Software Dependency for Windows Platforms

Previous versions of Polyspace products used Cygwin™ emulation to run UNIX® commands on Windows systems.

In version 5.1, the Cygwin software dependency has been removed. Removing Cygwin simplifies the Polyspace product installation process while improving the performance and robustness of the Polyspace Verification process.

Compatibility Considerations

Due to the Cygwin changes, Polyspace Client for Ada Version 5.1 is not compatible with previous versions of Polyspace products on Windows platforms. To avoid compatibility problems on Windows platforms, you must upgrade all your Polyspace client and server products at the same time.

If your Polyspace server is running on a Windows platform, the binary files used for batch commands in previous releases will not work without Cygwin software installed. In version 5.1, the software provides new .exe files for these batch commands. However, these files are now located in a different location.

CommandsPrevious LocationNew Location
StandardPolyspaceInstallDir\verifier\bin\PolyspaceInstallDir\verifier\wbin\
Remote LauncherPolyspace_Common\RemoteLauncher\bin\Polyspace_Common\RemoteLauncher\wbin\
ViewerPolyspace_Common\Viewer\bin\Polyspace_Common\Viewer\wbin\

If you wrote scripts using batch commands in previous releases, you must modify the scripts to use the new commands.

In addition, if you used Cygwin shell scripts for postprocessing or target compilation, those scripts will no longer run on version 5.1. To support scripting, the Polyspace software now includes Perl. You can access Perl in:

PolyspaceInstallDir\verifier\tools\perl\win32\bin\perl.exe

Enhanced Installer

Version 5.1 includes an enhanced and simplified installer for all Polyspace products. The installation process is now faster and easier to complete than in previous releases.

For more information, see the Polyspace Installation Guide.

Viewer Improvements

Enhanced exploring capability in the viewer to provide more focused information.

Unnecessary information has been eliminated from the Procedural Entities (RTE) View and Call Tree View to improve usability.

Enhanced Compilation Checks

Enhanced compilation checks to stop verification only when a pointer to a task is initiated or used, rather than when it is declared.

One-Click Enhancements

Enhanced Polyspace-In-One-Click options, to allow switching between multiple projects using a browse history.

Operating System Support

Added support for the following operating systems:

  • Solaris 2.10

  • Windows XP x64 (32-bit mode)

For more information, see the Polyspace Installation Guide.

Polyspace Server for Ada Product

Removed Cygwin Software Dependency for Windows Platforms

Previous versions of Polyspace products used Cygwin emulation to run UNIX commands on Windows systems.

In version 5.1, the Cygwin software dependency has been removed. Removing Cygwin simplifies the Polyspace product installation process while improving the performance and robustness of the Polyspace Verification process.

Compatibility Considerations

Due to the Cygwin changes, Polyspace Server for Ada Version 5.1 is not compatible with previous versions of Polyspace products on Windows platforms. To avoid compatibility problems on Windows platforms, you must upgrade all your Polyspace client and server products at the same time.

If your Polyspace server is running on a Windows platform, the binary files used for batch commands in previous releases will not work without Cygwin software installed. In version 5.1, the software provides new .exe files for these batch commands. However, these files are now located in a different location.

CommandsPrevious LocationNew Location
StandardPolyspaceInstallDir\verifier\bin\PolyspaceInstallDir\verifier\wbin\
Remote LauncherPolyspace_Common\RemoteLauncher\bin\Polyspace_Common\RemoteLauncher\wbin\
ViewerPolyspace_Common\Viewer\bin\Polyspace_Common\Viewer\wbin\

If you wrote scripts using batch commands in previous releases, you must modify the scripts to use the new commands.

In addition, if you used Cygwin shell scripts for postprocessing or target compilation, those scripts will no longer run on version 5.1. To support scripting, the Polyspace software now includes Perl. You can access Perl in:

PolyspaceInstallDir\verifier\tools\perl\win32\bin\perl.exe

Enhanced Installer

Version 5.1 includes an enhanced and simplified installer for all Polyspace products. The installation process is now faster and easier to complete than in previous releases.

For more information, see the Polyspace Installation Guide.

Operating System Support

Added support for the following operating systems:

  • Solaris 2.10

  • Windows XP x64 (32-bit mode)

For more information, see the Polyspace Installation Guide.

Was this topic helpful?