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.
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.
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.
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.
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.
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.
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.
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.
Risorse di prodotto:
Famiglia di prodotti Polyspace
I prodotti Polyspace rendono il codice critico sicuro testando e monitorando la qualità del software lungo l’intero ciclo di sviluppo.
Polyspace Access
Identificazione dei difetti di codifica, revisione dei risultati delle analisi statiche e monitoraggio delle metriche di qualità del software.
Polyspace Copilot
Assistente di IA ottimizzato per Polyspace.
Polyspace Test
Sviluppo, gestione ed esecuzione di test per il codice C e C++ in sistemi embedded.
Polyspace as You Code
Individua violazioni degli standard di codifica e vulnerabilità del software direttamente dal tuo IDE.
Polyspace Test Server
Esegui test e analizza la copertura strutturale del codice C/C++ su server di automazione.
Polyspace Code Prover Server
Verifica in modo continuo ed esaustivo le istruzioni fondamentali del codice C e C++ nelle pipeline di CI.
Polyspace Bug Finder
Identificazione dei bug del software utilizzando l'analisi statica.
Polyspace Client for Ada
Verifica in modo esaustivo le unità fondamentali delle istruzioni Ada utilizzando metodi formali.
Polyspace Bug Finder Server
Identificazione di difetti software tramite analisi statiche in esecuzione su computer server.
Polyspace Server for Ada
Verifica in modo continuo ed esaustivo le istruzioni fondamentali del codice C e C++ nelle pipeline di CI.
Polyspace Code Prover
Verifica in modo esaustivo le istruzioni fondamentali di C e C++ utilizzando metodi formali.
FAQ su Polyspace Client for Ada
Polyspace Client for Ada dimostra l'assenza di errori critici di run-time, come overflow, divisione per zero e accessi a array fuori dai limiti, nel codice Ada83 e Ada95. Fornisce inoltre viste architetturali, come grafi delle chiamate e informazioni sull'utilizzo dei dati globali, per aiutare a comprendere la struttura del software a partire dal codice.
Utilizza l'analisi statica basata su metodi formali per esplorare tutti i percorsi di esecuzione e gli input nel codice Ada83 e Ada95 senza eseguirlo.
Aiuta a migliorare la sicurezza del software dimostrando l'assenza di vulnerabilità critiche, come overflow del buffer, accessi alla memoria non validi e overflow numerici, su tutti i percorsi di esecuzione e per tutti gli input, senza eseguire il codice.
Polyspace Client for Ada viene utilizzato in modo interattivo tramite un'interfaccia desktop ed è limitato all'analisi di singoli file, mentre Polyspace Server for Ada è ottimizzato per l'analisi di integrazione automatizzata nei workflow di integrazione continua (CI).
Visualizza i risultati direttamente nel codice sorgente mediante annotazioni codificate per colore che indicano se le operazioni sono dimostrate prive di errori di run-time, dimostrate come errate, irraggiungibili o non dimostrate. Fornisce inoltre informazioni sugli intervalli di valori delle variabili e sui valori di ritorno delle funzioni per supportare l'analisi delle cause radice.
