Version 7.0 (R2009a) Polyspace for C/C++ Products :: Polyspace Release Notes (Polyspace®)

Version 7.0 (R2009a) Polyspace for C/C++ Products

This table summarizes what's new in V7.0 (R2009a):

New Features and Changes	Version Compatibility Considerations	Fixed Bugs and Known Problems
Yes Details below	Yes—Details labeled as Compatibility Considerations, below. See also Summary.	Includes fixes: Polyspace Client for C/C++ Bug Reports Polyspace Server for C/C++ Bug Reports

New features and changes introduced in this version are organized by product:

Polyspace Client for C/C++ Product

JSF++ Support

Enhanced JSF C++ checker supports all checkable Joint Strike Fighter Air Vehicle C++ coding standards (JSF++:2005).

Polyspace software can now check all possible C++ programming rules defined by Lockheed Martin^® for the JSF program. These coding standards are designed to improve the robustness of C++ code, and improve maintainability.

For more information, see Checking Coding Rules, in the Polyspace Products for C++ User's Guide.

Back to Source Link

New "back-to-source" link in the Polyspace launcher associates compile errors, MISRA-C violations, and JSF++ violations reported in the logs directly to the source file.

For more information, see Viewing Coding Rules Checker Resultsin the Polyspace Products for C/C++ User's Guide or Examining Rule Violations, in the Polyspace Products for C++ User's Guide.

Eclipse Integration

New Polyspace integration with the Eclipse IDE, Version 3.3.

The Polyspace Client for C/C++ product can be integrated with the Eclipse Integrated Development Environment through the Polyspace C/C++ 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.

For more information, see Using Polyspace Software in the Eclipse IDE in the Polyspace Products for C/C++ User's Guideor
Using Polyspace Software in the Eclipse IDEin the Polyspace Products for C++ User's Guide.

Performance Improvements for Multi-Core Systems

Enhanced performance on multi-core architecture platforms, improving the speed of Polyspace code verification.

The time required to perform an average code verification has been reduced. On multi-core systems, you can now select the number of processes that can run simultaneously, further improving performance.

For more information, see Number of processes for multiple CPU core systems (-max-processes) in the Polyspace Products for C/C++ Referenceor Polyspace Products for C++ Reference.

Architecture Improvements

Several changes have been made to the Polyspace architecture to improve overall performance, as well as the precision of verification results.

During each verification phase (pass), the software now only analyzes those procedures that need to be analyzed. This means that starting with PASS1, if the verification cannot be more precise than that already completed in a previous pass, the procedure is not analyzed again. This improves the overall performance of the verification. It also means that some passes will finish more quickly than others, and some passes could be completely empty. This is normal behavior.

In addition, these architecture improvements result in the following changes:

The –quick precision option is now obsolete, and has been removed. –quick mode has been replaced with verification PASS0. PASS0 takes somewhat longer to run, but the results are more complete. The limitations of –quick mode, (no NTL or NTC checks, no float checks, no variable dictionary) no longer apply. Unlike –quick mode, PASS0 also provides full navigation in the Viewer.
The –voa option is now obsolete, and has been removed. Value On Assignment checks are now provided by default. In general, this means that Polyspace results now contain many more VOA checks. For C applications, all possible VOA are given.

The UOVFL (Float Underflows and Overflows) check no longer exists. Float underflows and overflows are now reported as two separate checks. This is similar to the way integers are handled.

Note Since the single UOVFL check has been replaced by two checks, the total number of checks reported by Polyspace on a given file may be different in this release than with previous versions of the software.

Messages have been improved for float arithmetic checks, making them similar to the messages for integers. For example, NIV checks on float variables now contain the type size (32 or 64).
For IPT (Inspection Point) checks, there is now one check for each variable. Previously there was a single IPT check (on the keyword) for multiple variables.
The log file has several additions, including the names of each PASS, the verification phases, and additional messages.

Compatibility Considerations. The verification results provided by Polyspace software may be different in R2009a than with previous releases of the software. Verification results are more precise, and the total number of checks reported on a given source file may be different. In general, the software now reports more checks, due to increased VOA checks, changes to the IPT check, and the single float UOVFL check being replaced by two checks (UNFL and OVFL).

In addition, due to the float UOVFL check being split into two checks, the selectivity (number of proven checks red+green+gray / number of total checks) of a verification may change significantly for applications using many float variables. For example, an application that had 10 orange UOVFL checks with a previous release, could now have up to 20 orange UNFL and OVFL checks on the same float variables. Although this appears to be a decrease in precision, the verification itself is not less precise.

Mathematical Functions Included in Stubs

Mathematical functions are now included in the standard stubs. This means:

An IRV (Initialized Return Value) check appears on the math function call.
The POW check no longer appears in the Viewer.
Math functions appear in the call graph.
The modeling of mathematical functions is visible through the stub body, instead of being handled internally.
By default, math functions are launched with the option -context-sensitivity , allowing them to distinguish their calling sites.

In addition, you can provide your own math functions instead of using the standard stub provided by Polyspace software. This allows the software to verify the body of the math function, instead of using a stub for the math function.

For example, in C90, the mathematical function fabs() has the prototype:

double fabs(double) ;

However, on a 16-bit target, the function may have the prototype:

float fabs(float);

In this case, you would want to verify your own fabs() function.

To provide your own math function:

Create source code for the function. For example:

float  fabs (float var)
{
  if (var >= 0.0f)
    return var;
  return -var;
}

Provide the function to your verification using the —D compiler flag. For example:
```
polyspace-c -D  __polyspace_no_fabs
```

Note There is a compiler flag for each standard ANSI C90 mathematical function. A complete list of flags is located in the file: %POLYSPACE_C%\Verifier\cinclude\__polyspace__stdstubs.c.

Compatibility Considerations. Since the POW check no longer appears in the Viewer, verification results may be different in R2009a than with previous releases of the software.

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.

For more information, see Setting Character Encoding Preferencesin the Polyspace Products for C/C++ User's Guideor Polyspace Products for C++ User's Guide.

Automatic Orange Tester

The Automatic Orange Tester (for C), dynamically stresses unproven code (orange checks) to help you identify run-time errors.

For more information, see Automatically Testing Orange Code in the Polyspace Products for C/C++ User's Guide.

Compatibility Considerations. If you open verification results created with an older version of the product in the Automatic Orange Tester, you may get a compilation error. The version of the product used to create the instrumented source code must be the same as the one used for analysis in the Automatic Orange Tester.

To avoid this problem, re-launch the code verification with the current version of the 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.

Polyspace Server for C/C++ Product