Polyspace Client™ für Ada weist die Abwesenheit von Fehlern durch Überlauf, Division durch Null, Array-Zugriff außerhalb der Grenzen und bestimmte weitere Laufzeitfehler in Ada83- und Ada95-Quellcode nach. Diese Ergebnisse erfordern weder eine Programmausführung noch eine Code-Instrumentierung oder Testfälle. Polyspace Client for Ada nutzt abstrakte Interpretationsmethoden für die Codeverifizierung, die auf formalen Methoden beruhen. Analyseergebnisse werden im Quellcode angezeigt. Jede Anweisung im Code ist farblich markiert, um zu verdeutlichen, ob sie frei von Laufzeitfehlern ist, nachweislich fehlschlagen wird, nicht erreichbar oder unbewiesen ist. Polyspace Client for Ada zeigt Bereichsinformationen für Variablen und Ausgabewerte von Funktionen an und prüft, welche Variablen festgelegte Bereichsgrenzen überschreiten.
Sie können Polyspace Client for Ada auf Ihrem Desktop nutzen, um vor der Kompilierung und den Tests Codeanalysen durchzuführen und zu überprüfen.
Nachweis der Abwesenheit kritischer Laufzeitfehler
Prüfen Sie Ada83- oder Ada95-Codevorgänge auf korrektes Laufzeitverhalten. Identifizieren Sie Anweisungen, die unabhängig von den Laufzeitbedingungen nie Laufzeitfehler aufweisen. Analysieren Sie Schwachstellen in der Laufzeit, unterstützt durch Event-Traces, Wertebereiche für Variablen und Aufrufbäume, die mit den Ergebnissen verknüpft sind. Polyspace Client for Ada verwendet formale Methoden, um Fehler zu finden, die anderen Testmethoden entgehen. Analysieren Sie alle Codepfade hinsichtlich aller potenziellen Eingaben, ohne Code ausführen zu müssen.
Interaktive Analysen auf Desktop-Computern
Organisieren und konfigurieren Sie Ihre Projekte und führen Sie statische Codeanalysen für Teilmengen von Softwareprojekten aus, um Codeänderungen zu qualifizieren, bevor Sie den Quellcode an das Quellcode-Repository übergeben. Nutzen Sie Polyspace Client for Ada für die Erstellung von Berichten sowie zum Überprüfen und Vorsortieren der Ergebnisse. Ermitteln Sie die Ursache komplexer Programmierfehler mithilfe Debugger-ähnlicher Ansichten, um Schritt für Schritt durch jede Anweisung zu navigieren, die zu einem Laufzeitfehler führt.
Besseres Software-Design und besseres Codeverständnis
Überprüfen Sie die Kontroll- und Datenflüsse in der Software und sehen Sie Wertebereichsinformationen, die mit Variablen und Operatoren verbunden sind.
Optimierung der Softwareleistung
Identifizieren Sie sichere Vorgänge und entfernen Sie defensiven Code wie die Division durch Null. Erkennen und entfernen Sie Fehler in Logik und Programmstruktur sowie Codezweige, die von Ausführungspfaden nicht erreicht werden können, um den Speicherbedarf gering zu halten.
Analyse der Verwendung globaler Variablen
Beschleunigen Sie das Debugging von Lese-/Schreibvorgängen mit globalen Variablen, einschließlich Variablen, die von Tasks oder Threads gemeinsam genutzt werden. Der Mehrfachzugriffs-Graph bietet Einblicke in den Kontroll- und Datenfluss, der zu einem Data Race führt. Identifizieren Sie ungenutzte globale Variablen für die Codeoptimierung.
Statische Anwendungssicherheitstests
Weisen Sie nach, dass die Anwendung keine kritischen Sicherheitsschwachstellen aufweist, indem Sie potenziell schwachstellenbehaftete Ada-Anweisungen umfassend auf Faktoren wie Speicherzugriff, Pufferüberlauf oder numerischen Überlauf testen. Unterstützung von 20 CWE-Schwachstellenregeln. Nutzen Sie die Analyseergebnisse des Polyspace Client for Ada als Fuzzing-Ergänzung oder -Ersatz und konzentrieren Sie sich stattdessen auf Vorgänge, die als anfällig identifiziert wurden.
Optimierung und Ergänzung von Robustheits- und funktionalen Tests
Verwenden Sie Polyspace Client for Ada für Robustheitstests, indem Sie sich bei Tests auf Anweisungen wie Division durch Null oder Überläufe konzentrieren, die als unsicher eingestuft wurden. Nutzen Sie die Ergebnisse von Polyspace Client for Ada zur Erstellung und Pflege von Grenzwert- und Partitionstests, für die Kontroll- und Datenflussanalyse und den berechneten Bereich von Funktionsparametern und globalen Variablen.
Produktressourcen:
Polyspace-Produktfamilie
Polyspace-Produkte machen kritischen Code sicher und geschützt, indem die Softwarequalität während des gesamten Entwicklungslebenszyklus getestet und überwacht wird.
Polyspace Access
Erkennen Sie Codierfehler, überprüfen Sie die Ergebnisse statischer Analysen und überwachen Sie Softwarequalitätsmetriken.
Polyspace Copilot
Ein für Polyspace optimierter KI-Assistent.
Polyspace Test
Entwicklung, Verwaltung und Durchführung von Tests für C und C++ Code in Embedded Systems.
Polyspace as You Code
Erkennen Sie Software-Schwachstellen und Verstöße gegen Codierungsstandards über Ihre IDE.
Polyspace Test Server
Führen Sie Tests und Analysen der strukturellen Abdeckung von C/C++ Code auf Automatisierungsservern aus.
Polyspace Code Prover Server
Verifizieren Sie laufend und umfassend kritische Anweisungen in C und C++ Code in CI-Pipelines.
Polyspace Bug Finder
Überprüfen Sie Programmierregeln, Sicherheitsstandards und Codemetriken und finden Sie Bugs.
Polyspace Client for Ada
Erstellen Sie mithilfe formaler Methoden umfassende Verifikationen für Ada-Anweisungseinheiten.
Polyspace Bug Finder Server
Ermitteln Sie Softwarefehler und setzen Sie Programmierregeln in Ihren CI-Pipelines durch.
Polyspace Server for Ada
Erstellen Sie laufende und umfassende Verifikationen für kritische Ada-Codeanweisungen in CI-Pipelines.
Polyspace Code Prover
Erstellen Sie mithilfe formaler Methoden umfassende Verifikationen für besonders kritische C und C++ Anweisungen.
Polyspace Client for Ada – Häufig gestellte Fragen
Der Polyspace Client for Ada weist das Fehlen kritischer Laufzeitfehler wie Overflows, Division durch Null und Arrayzugriffe außerhalb der Grenzen in Ada83- und Ada95-Code nach. Es bietet außerdem Architekturansichten wie Aufrufgraphen und die Nutzung globaler Daten, um die Softwarestruktur aus dem Code besser zu verstehen.
Er verwendet auf formalen Methoden basierende statische Analyse, um alle Ausführungspfade und Eingaben in Ada83- und Ada95-Quellcode zu untersuchen, ohne diesen auszuführen.
Er trägt zur Verbesserung der Softwaresicherheit bei, indem er das Fehlen kritischer Schwachstellen wie Pufferüberläufe, ungültige Speicherzugriffe und numerische Overflows über alle Ausführungspfade und Eingaben hinweg nachweist, ohne den Code auszuführen.
Polyspace Client for Ada wird interaktiv über eine Desktop-Oberfläche verwendet und ist auf die Analyse einzelner Dateien beschränkt, während Polyspace Server for Ada für automatisierte Integrationsanalysen in CI‑Workflows optimiert ist.
Ergebnisse werden direkt im Quellcode angezeigt, mithilfe farblich codierter Anmerkungen, die darstellen, ob Operationen als frei von Laufzeitfehlern nachgewiesen, als fehlerhaft nachgewiesen, als unerreichbar oder als nicht nachgewiesen eingestuft wurden. Zusätzlich werden Informationen zu Wertebereichen für Variablen und Funktionsrückgabewerte bereitgestellt, um die Ursachenanalyse zu unterstützen.
