Polyspace Code Prover

Laufzeitfehler erkennen

Polyspace Code Prover verwendet abstrakte Interpretation mit statischer Codeanalyse, um Laufzeitfehler wie Überläufe, Division durch Null, Zeiger, die außerhalb des gültigen Bereichs liegen, nachzuweisen, zu identifizieren und zu diagnostizieren. Mit dieser Technik werden alle Laufzeitbedingungen vollständig und umfassend verifiziert. Für jede Codeoperation erfolgt die automatische Ausgabe der Diagnose „bewiesen“, „fehlgeschlagen“, „unerreichbar“, „unbewiesen“. In den von Polyspace Code Prover gelieferten Verifikationsergebnissen ist jede C- oder C++-Operation farbkodiert, um den entsprechenden Status anzugeben:

Grün: bewiesen „frei“ von Laufzeitfehlern
Rot: bewiesen „fehlerhaft“ bei jedem Ausführen der Operation
Grau: bewiesen „unerreichbar“ (möglicherweise ein funktionales Problem)
Orange: „unbewiesene“ Operation ist möglicherweise unter bestimmten Bedingungen fehlerhaft

Color-coded run-time error attributes identified by Polyspace Code Prover.

Von Polyspace Code Prover identifizierte Attribute für Laufzeitfehler.

Folgende Fehler werden erkannt:

  • Überlauf, Unterlauf, Division durch Null und andere arithmetische Fehler
  • unzulässiger Array-Zugriff und unerlaubt dereferenzierte Zeiger
  • immer wahr/falsch-Anweisung
  • nicht-initialisierte Klassenmember (C++)
  • Lesezugriff auf nicht initialisierte Daten
  • Zugriff, um diesen Zeiger (C++) für ungültig zu erklären
  • toter Code
  • dynamische Fehler in Bezug auf Objektprogrammierung, Vererbung und Ausnahmebehandlung (C++)
Weiter: Bereichsinformationen anzeigen

Probieren Sie Polyspace Code Prover

Testsoftware anfordern

Kein Spaß an Code Reviews? Automatische Verifikation!

Webinar anzeigen