PolySpace Server for Ada 5.2

Product Description

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

Introduction

PolySpace™ Server for Ada, together with PolySpace™ Client 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 Server for Ada is the computation engine of PolySpace™ products for Ada. You can use it to run jobs posted by PolySpace™ Client for Ada (available separately) and to manage multiple servers.

PolySpace Server for Ada and PolySpace Client 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
• Produces verification results
• Generates HTML reports

Remote Launcher Manager, showing configuration options for PolySpace Server for Ada. Options include setting user permissions and selecting available products. Click on image to see enlarged view.

Next