Polyspace Client for Ada

Dimostrazione dell’assenza di errori di run-time nel codice sorgente

Polyspace Client™ for Ada dimostra l’assenza di overflow, divisioni per zero, fuori limite, accesso ad array fuori limite e alcuni altri errori di runtime in codice sorgente Ada83 e Ada95. Produce risultati senza la necessità di esecuzione del programma, code instrumentation o casi di test. Polyspace Client for Ada utilizza tecniche di interpretazione astratta basate su metodi formali per verificare il codice. I risultati dell’analisi vengono mostrati all’interno del codice sorgente. Ciascuna istruzione di codice è contrassegnata da un colore che indica se l’istruzione è priva di errori di esecuzione, dimostrata come fallimentare, non eseguibile o non dimostrata. Polyspace Client for Ada mostra le informazioni di intervallo per le variabili e i valori restituiti delle funzioni ed è in grado di dimostrare quali variabili superano i limiti di intervallo specificati.

È possibile utilizzare Polyspace Client for Ada sul desktop per eseguire e rivedere le analisi del codice prima della compilazione e del test.

Polyspace Client for Ada utilizza diversi colori per identificare le istruzioni Ada che sono state verificate staticamente.

Dimostrazione dell’assenza di errori critici di runtime

Verifica la correttezza di runtime delle operazioni in codice Ada83 o Ada95. Individua le istruzioni che non subiranno mai un errore di runtime, indipendentemente dalle condizioni di runtime. Analizza le vulnerabilità di runtime con il supporto di tracce degli eventi, intervalli di valori delle variabili e alberi delle chiamate relativi ai risultati. Polyspace Client for Ada impiega metodi formali per rilevare errori che sfuggono ad altri strumenti di test. Analizza tutti i percorsi del codice rispetto a tutti i possibili input senza l’esecuzione del codice.

CSEE Transport garantisce l’affidabilità del software per l’alta velocità ferroviaria

Documentazione

Tre finestre aperte. Una con istruzioni con codice a colori, una con parametri e una con elementi grafici.

Analisi interattiva sul desktop

Organizza e configura i tuoi progetti ed esegui l’analisi statica del codice su un sottogruppo di progetti software per verificare la modifica al codice prima di inviarlo all’archivio del codice sorgente. Utilizza Polyspace Client for Ada per generare report e rivedere e classificare i risultati. Individua la causa principale di bug complessi in viste debugger per analizzare gradualmente ciascuna istruzione che porta a un errore di runtime.

Documentazione

Polyspace Client for Ada fornisce l’elenco di tutte le variabili globali del software analizzato.

Miglioramento della progettazione software e comprensione del codice

Analizza il flusso di controllo e di dati attraverso il software e scopri le informazioni di intervallo associate alle variabili e agli operatori.

Il NATO HAWK Management Office accelera l’analisi delle applicazioni mission-critical

Documentazione

Polyspace Client for Ada mostra il codice non eseguibile in grigio all’interno del codice sorgente.

Ottimizzazione delle prestazioni del software

Rimuovi il codice difensivo identificando operazioni sicure come la divisione per zero. Rileva e rimuovi i rami di codice che non possono essere eseguiti attraverso qualsiasi percorso di esecuzione e gli errori nella logica e nella struttura del programma al fine di ridurre il footprint di memoria.

Documentazione

Polyspace Client for Ada è in grado di mostrare un grafico del percorso che porta a potenziali corse di dati.

Analisi dell’utilizzo delle variabili globali

Riduci il tempo dedicato al debug delle operazioni di lettura/scrittura sulle variabili globali, incluse le variabili condivise da attività o thread. Comprendi il flusso di controllo e di dati che porta a una corsa di dati mediante il grafico ad accesso simultaneo. Identifica le variabili globali inutilizzate al fine di ottimizzare il codice.

Documentazione

Test statici di sicurezza delle applicazioni

Dimostra che l’applicazione è priva di vulnerabilità critiche di sicurezza analizzando in modo esaustivo le istruzioni Ada potenzialmente vulnerabili come l’accesso alla memoria, gli overflow del buffer o gli overflow numerici. Supporto di 20 regole di debolezza CWE. Sfrutta i risultati dell’analisi da Polyspace Client for Ada per integrare o sostituire i test fuzz e concentrarti sulle operazioni vulnerabili.

Sicurezza incorporata con l’analisi statica di Polyspace (1:52)

Polyspace Client for Ada calcola la gerarchia completa delle chiamate per le applicazioni Ada.

Miglioramento e integrazione dei test di robustezza e funzionali

Utilizza Polyspace Client for Ada per migliorare i test di robustezza concentrando i test su istruzioni dimostrate come non sicure quali la divisione per zero o gli overflow. Utilizza i risultati di Polyspace Client for Ada per creare e mantenere test di confine e di partizione, sfruttando l’analisi dei flussi di controllo e di dati nonché gli intervalli calcolati dei parametri delle funzioni e delle variabili globali.

EADS garantisce l’affidabilità dei veicoli di lancio

Documentazione

Risorse di prodotto:

Documentazione Esempi Video Requisiti Note di release

Vuoi saperne di più su Polyspace Client for Ada?

Richiedi una versione di prova Richiedi una quotazione

Hai domande?

Contatta l’assistenza tecnica di Polyspace Client for Ada.