PolySpace Client for Ada 5.2

Product Description

• Introduction and Key Features
• Working with PolySpace Client for Ada
• Verifying Program Dynamics
• Typical Run-Time Errors Detected

Introduction

PolySpace™ Client for Ada, together with PolySpace™ Server for Ada, provides a code-based verification tool that proves source code reliability and detects run-time errors in source code without requiring you to execute or modify the code.

PolySpace Client for Ada is the management and visualization tool of PolySpace products for Ada. You use it to submit jobs for execution by PolySpace Server for Ada (available separately) and to review verification results.

PolySpace Client for Ada and PolySpace Server for Ada use abstract interpretation techniques to verify all possible executions of a source program. As a result, they prove which operations are free of run-time errors, including overflows, divisions by zero, out-of-bounds array indexes, or read access to noninitialized data. They also identify where run-time errors will or might occur and which portion of code is unreachable (dead code). PolySpace products for Ada use color-coding to highlight all elements in source code that have no errors, might have errors, definitely have errors, or cannot be reached. With this information, they generate metrics and reports that let you monitor and improve source code reliability.

Key Features

• Uses advanced code-based verification techniques to automatically verify all program executions
• Does not require code execution, code modification, or test cases
• Operates on packages and sets of packages
• Highlights all diagnostics provided by PolySpace™ Server for Ada
• Identifies run-time errors directly in the code

PolySpace Viewer (left), showing color-coding for each file, procedure, and line of Ada code and PolySpace Queue Manager Interface (below, left), listing jobs posted to PolySpace Server for Ada. Click on image to see enlarged view.

Next