Polyspace Client for Ada

 

Polyspace Client for Ada

Prove the absence of run-time errors in source code

Request a free trial
Request a quote

Polyspace Client™ for Ada proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain other run-time errors in Ada83 and Ada95 source code. It produces results without requiring program execution, code instrumentation, or test cases. Polyspace Client for Ada uses abstract interpretation techniques based on formal methods to verify code. Analysis results are shown within the source code. Each code statement is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven. Polyspace Client for Ada displays range information for variables and function return values and can prove which variables exceed specified range limits.

You can use Polyspace Client for Ada on your desktop to run and review code analyses before compilation and test.

Polyspace Client for Ada
Polyspace Client for Ada uses multiple colors to identify Ada statements that have been statically checked.

Prove the Absence of Critical Run-Time Errors

Check Ada83 or Ada95 code operations for run-time correctness. Identify statements that will never experience a run-time error, regardless of the run-time conditions. Analyze run-time vulnerabilities with the support of event traces, variable value ranges, and call trees related to the finding. Polyspace Client for Ada uses formal methods to detect errors that elude other means of testing. Analyze all code paths against all possible inputs without code execution.

CSEE Transport Ensures Reliability of High-Speed Rail Software

Documentation

Three windows open. One with color-coded statements, one with parameters, and one with graphical elements.

Interactive Analysis on Desktop

Organize and configure your projects, and run static code analysis on subset of software projects to qualify code change before submitting code to source code repository. Use Polyspace Client for Ada to generate reports, and review and triage results. Find the root cause of complex bugs with debugger-like views to navigate step-by-step through each statement leading to a run-time error.

Documentation

Polyspace Client for Ada provides the list of all global variables of the analyzed software.

Improve Software Design and Code Understanding

Examine control and data flow through software and see range information associated with variables and operators.

NATO HAWK Management Office Accelerates Analysis of Mission-Critical Applications

Documentation

Polyspace Client for Ada displays unreachable code in gray color within the source code.

Optimize Software for Performance

Remove defensive code by identifying safe and secure operations such as division by zero. Detect code branches that cannot be reached via any execution path and errors in logic and program structure and remove them for smaller memory footprint.

Documentation

Polyspace Client for Ada can display a graph of the path leading to potential data race.

Analyze Global Variable Usage

Reduce time spent on debugging read/write operations on global variables, including variables shared by tasks or threads. Understand control and data flow leading to a data race with the concurrent access graph. Identify unused global variables for code optimization.

Documentation

Protective shield illustration in front of code.

Static Application Security Testing

Prove that the application is free of critical security vulnerabilities by exhaustively stressing potential vulnerable Ada statements such as memory access, buffer overflows, or numerical overflows. Support of 20 CWE weakness rules. Leverage analysis results from Polyspace Client for Ada to complement or replace fuzz testing and focus instead on vulnerable identified operations.

Embedded Security with Polyspace Static Analysis (1:52)
Polyspace Client for Ada computes the complete call hierarchy for Ada applications.

Improve and Complement Robustness and Functional Testing

Use Polyspace Client for Ada to improve robustness testing by focusing tests on statements proven unsafe such as division by zero or overflows. Use results from Polyspace Client for Ada to create and maintain boundary and partition tests, leveraging control and data flow analysis, and computed range of function parameters and global variables.

EADS Ensures Launch Vehicle Dependability

Documentation

Product Resources:

Documentation Examples Videos Requirements Release notes

Polyspace Product Family

Polyspace products make critical code safe and secure by testing and monitoring software quality throughout the development lifecycle.

Polyspace Access

Identify coding defects, review static analysis results, and monitor software quality metrics.

Polyspace Code Prover Server

Continuously and exhaustively verify critical C and C++ code statements into CI pipelines.  

Polyspace Bug Finder

Check coding rules, security standards, and code metrics, and find bugs.

Polyspace Test

Develop, manage, and execute tests for C and C++ code in embedded systems.

Polyspace Bug Finder Server

Identify software defects and enforce coding rules in your CI pipelines.

Polyspace Client for Ada

Exhaustively verify critical Ada statements units using formal methods.

Polyspace Code Prover

Exhaustively verify the most critical C and C++ statements using formal methods.

Polyspace Server for Ada

Continuously and exhaustively verify critical Ada code statements into CI pipelines.

Interested in Polyspace Client for Ada?

Request a trial Request a quote

Have Questions?

Contact the Polyspace Client for Ada technical team.