Differenze tra Polyspace Bug Finder e Polyspace Code Prover
Polyspace® Bug Finder™ e Polyspace Code Prover™ rilevano gli errori di runtime tramite l'analisi statica. Sebbene i due prodotti abbiano un'interfaccia utente simile e la matematica alla base dell'analisi possa talvolta essere la stessa, perseguono obiettivi differenti.
Bug Finder (o Polyspace as You Code, che esegue un'analisi di un singolo file simile a quella di Bug Finder) analizza rapidamente il codice e rileva molti tipi di difetti. Code Prover controlla ogni operazione nel codice per individuare un insieme di possibili errori di runtime e cerca di dimostrare l'assenza dell'errore per tutti i percorsi di esecuzione.
Nota
Per ogni operazione nel codice, Code Prover considera tutti i percorsi di esecuzione che conducono all'operazione e che non presentano un errore precedente. Se un percorso di esecuzione contiene un errore precedente all'operazione, Code Prover non lo prende in considerazione. Vedere Code Prover Analysis Following Red and Orange Checks (Polyspace Code Prover).
Ad esempio, per ogni divisione nel codice, un'analisi Code Prover cerca di dimostrare che il denominatore non può essere zero. Bug Finder non esegue una verifica così esaustiva. Ad esempio, anche Bug Finder controlla la presenza di errori di divisione per zero, ma potrebbe non individuare tutte le operazioni che possono causare l'errore.
Questa differenza di obiettivi dei due prodotti comporta differenze nella configurazione, nell'analisi e nella revisione dei risultati. Nelle sezioni seguenti vengono evidenziate le principali differenze tra un'analisi con Bug Finder e un'analisi Code Prover (nota anche come verifica). A seconda delle esigenze, è possibile integrare uno o entrambi i tipi di analisi nei punti appropriati del ciclo di vita dello sviluppo software.
Panoramica delle differenze tra Bug Finder e Code Prover
Utilizzare regolarmente sia Bug Finder che Code Prover nel processo di sviluppo. I prodotti offrono un insieme unico di funzionalità e si completano a vicenda. Per le possibili modalità di utilizzo combinato dei prodotti, vedere Workflow utilizzando sia Polyspace Bug Finder che Polyspace Code Prover.
Questa tabella fornisce una panoramica di come i prodotti si completano a vicenda. Per i dettagli, vedere le sezioni seguenti.
| Feature | Bug Finder | Code Prover |
|---|---|---|
| Numero di checker | Oltre 300 checker per i difetti | 30 controlli per errori critici di runtime e 4 controlli sull'utilizzo delle variabili globali |
| Profondità di analisi | Rapido. Ad esempio:
| Esaustivo. Ad esempio:
|
| Criteri di generazione dei report | Difetti probabili | Risultati comprovati |
| Criteri di rilevamento dei bug | Pochi falsi positivi | Zero falsi negativi |
In che modo Bug Finder e Code Prover si completano a vicenda
Analisi più rapida con Bug Finder
La velocità dell'analisi Bug Finder dipende dalla dimensione dell'applicazione. Il tempo di analisi Bug Finder aumenta in modo lineare con la dimensione dell'applicazione. Il tempo di verifica Code Prover aumenta con una velocità superiore a quella lineare.
Un possibile workflow consiste nell'eseguire Code Prover per analizzare i moduli o le librerie in termini di robustezza rispetto a determinati errori ed eseguire Bug Finder nella fase di integrazione. L'analisi Bug Finder su basi di codice di grandi dimensioni può essere completata in un tempo molto più breve e individua inoltre difetti di integrazione come Declaration mismatch e Data race.
Verifica più esaustiva con Code Prover
Code Prover cerca di dimostrare l'assenza di:
Errore Division by Zero in ogni operazione di divisione o di modulo
Errore Out of Bounds Array Index in ogni accesso all'array
Errore Non-initialized Variable in ogni lettura di variabile
Errore Overflow in ogni operazione che può causare un overflow
e così via.
Per ogni operazione:
Se Code Prover può dimostrare l'assenza dell'errore in tutti i percorsi di esecuzione, evidenzia l'operazione in verde.
Se Code Prover può dimostrare la presenza di un errore definito in tutti i percorsi di esecuzione, evidenzia l'operazione in rosso.
Se Code Prover non può dimostrare l'assenza di un errore o la presenza di un errore definito, evidenzia l'operazione in arancione. Questa piccola percentuale di controlli arancioni indica operazioni che è necessario esaminare attentamente, tramite ispezione visiva o test. I controlli arancioni spesso indicano vulnerabilità nascoste. Ad esempio, l'operazione potrebbe essere sicura nel contesto attuale ma non andare a buon fine se riutilizzata in un altro contesto.
È possibile utilizzare le informazioni fornite nell'interfaccia utente di Polyspace per diagnosticare i controlli. Vedere Analisi più rigorosa del flusso di dati e di controllo con Code Prover. È inoltre possibile fornire informazioni contestuali per ridurre ulteriormente il codice non comprovato, ad esempio vincolando esternamente gli intervalli di input.
Bug Finder non mira a fornire un'analisi esaustiva. Cerca di rilevare il maggior numero possibile di bug e ridurre i falsi positivi. Per i componenti software critici, l'esecuzione di uno strumento di individuazione dei bug non è sufficiente perché, nonostante la correzione di tutti i difetti individuati durante l'analisi, possono ancora verificarsi errori durante l'esecuzione del codice (falsi negativi). Dopo aver eseguito Code Prover sul codice e risolto i problemi individuati, è possibile attendersi una qualità del codice molto più elevata. Vedere Zero falsi negativi con Code Prover.
Tipi di difetto più specifici con Bug Finder
Code Prover controlla i tipi di errori di runtime per i quali è possibile dimostrare matematicamente l'assenza dell'errore. Oltre a rilevare gli errori la cui assenza può essere comprovata matematicamente, Bug Finder rileva anche altri difetti.
Ad esempio, l'istruzione if(a=b) è semanticamente corretta secondo lo standard del linguaggio C, ma spesso indica un compito non intenzionale. Bug Finder rileva tali operazioni non intenzionali. Sebbene Code Prover non rilevi tali operazioni non intenzionali, può rilevare se un'operazione non intenzionale causa altri errori di runtime.
Esempi di difetti rilevati da Bug Finder ma non da Code Prover includono difetti di buona pratica, difetti di gestione delle risorse, alcuni difetti di programmazione, difetti di sicurezza e difetti nella progettazione orientata agli oggetti in C++.
Per maggiori informazioni, vedere:
Difetti: Elenco dei difetti che Bug Finder può rilevare.
Run-Time Checks (Polyspace Code Prover): Elenco degli errori di runtime che Code Prover può rilevare.
Processo di impostazione più semplice con Bug Finder
Anche se il codice viene compilato correttamente nella toolchain di compilazione, potrebbe non superare la fase di compilazione di una verifica Code Prover. La compilazione rigorosa in Code Prover è correlata alla sua capacità di dimostrare l'assenza di determinati errori di runtime.
Code Prover segue rigorosamente lo standard ANSI® C99, a meno che non si utilizzino esplicitamente opzioni di analisi che emulano il compiler in uso.
Per consentire deviazioni allo standard ANSI C99, è necessario utilizzare le opzioni Target e compiler. Se si crea un progetto Polyspace dal proprio sistema di build, le opzioni vengono impostate automaticamente.
Code Prover non consente errori di collegamento che i compiler comuni possono invece permettere.
Sebbene il compiler consenta errori di collegamento, come una mancata corrispondenza nella firma della funzione tra unità di compilazione, per evitare comportamenti imprevisti in fase di esecuzione è necessario correggere tali errori.
Per maggiori informazioni, vedere Troubleshoot Compilation and Linking Errors (Polyspace Code Prover).
Bug Finder è meno rigoroso riguardo a determinati errori di compilazione. Gli errori di collegamento, come la mancata corrispondenza nella firma della funzione tra diverse unità di compilazione, possono interrompere una verifica Code Prover ma non un'analisi Bug Finder. Pertanto, è possibile eseguire un'analisi Bug Finder con uno sforzo di configurazione minore. In Bug Finder, gli errori di collegamento vengono spesso segnalati come un difetto al termine dell'analisi.
Esecuzioni ridotte per codice pulito con Bug Finder
Per garantire l'assenza di determinati errori di runtime, Code Prover segue regole rigorose non appena rileva un errore di runtime in un'operazione. Quando si verifica un errore di runtime, lo stato del programma è indefinito e Code Prover non può dimostrare l'assenza di errori nel codice successivo. Quindi:
Se Code Prover dimostra la presenza di un errore definito e visualizza un segno di spunta rosso, non verifica il codice rimanente nello stesso blocco.
Fanno eccezione controlli come Overflow, in cui l'analisi continua con il risultato dell'overflow troncato o ciclico.
Se Code Prover sospetta la presenza di un errore e visualizza un segno di spunta arancione, elimina dalla considerazione il percorso contenente l'errore. Ad esempio, se Code Prover rileva un errore Division by Zero nell'operazione
1/x, nella successiva operazione suxall'interno di quel blocco,xnon può essere zero.Se Code Prover rileva che un blocco di codice non è raggiungibile e visualizza un segno di spunta grigio, non rileva errori in quel blocco.
Per maggiori informazioni, vedere Code Prover Analysis Following Red and Orange Checks (Polyspace Code Prover).
Pertanto, una volta corretti i segni di spunta rossi e grigi e rieseguita la verifica, è possibile individuare altri problemi. Per ottenere un codice completamente pulito, è necessario eseguire la verifica più volte e correggere i problemi a ogni esecuzione. La situazione è simile al test dinamico. Nel test dinamico, una volta corretta un'anomalia in un determinato punto del codice, è possibile scoprirne una nuova nel codice successivo.
Bug Finder non interrompe l'intera analisi in un blocco dopo aver trovato un difetto in quel blocco. Anche con Bug Finder potrebbe essere necessario eseguire l'analisi più volte per ottenere un codice completamente pulito. Tuttavia, il numero di esecuzioni richieste è inferiore rispetto a Code Prover.
Risultati in tempo reale con Bug Finder
Bug Finder mostra alcuni risultati di analisi mentre l'analisi è ancora in corso. Non è necessario attendere la fine dell'analisi per esaminare i risultati.
Code Prover mostra i risultati solo al termine della verifica. Una volta individuato un difetto, Bug Finder è in grado di visualizzarlo. Code Prover deve dimostrare l'assenza di errori su tutti i percorsi di esecuzione. Pertanto, non può visualizzare i risultati durante l'analisi.
Analisi più rigorosa del flusso di dati e di controllo con Code Prover
Per ogni operazione nel codice, Code Prover fornisce:
Tooltip che mostra l'intervallo di valori di ciascuna variabile nell'operazione.
Per un puntatore, i suggerimenti mostrano la variabile a cui punta il puntatore, insieme ai valori delle variabili.
Rappresentazione grafica della sequenza di chiamate di funzione che porta all'operazione.
Utilizzando queste informazioni sull'intervallo e il grafico delle chiamate, è possibile spostarsi facilmente nella gerarchia delle chiamate di funzione e comprendere come una variabile acquisisce i valori che portano a un errore. Ad esempio, per un errore Out of Bounds Array Index, è possibile individuare il punto in cui alla variabile indice vengono assegnati per la prima volta valori che conducono all'errore.
Durante la revisione di un risultato in Bug Finder, sono inoltre disponibili informazioni di supporto per comprendere la causa principale di un difetto. Ad esempio, è disponibile un traccia di esecuzione dal punto in cui Bug Finder ha trovato un difetto fino alla sua causa principale. Tuttavia, in Code Prover le informazioni sono più complete, perché consentono di comprendere tutti i percorsi di esecuzione nel codice.
Analisi del flusso di dati in Code Prover
Analisi del flusso di controllo in Code Prover
Pochi falsi positivi con Bug Finder
Bug Finder mira a ridurre i falsi positivi, ossia i risultati che probabilmente non è necessario correggere. Per impostazione predefinita, vengono visualizzati solo i difetti che potrebbero essere più significativi per l'utente.
Bug Finder assegna inoltre un attributo denominato impatto ai tipi di difetto in base alla criticità dello stesso e al rate di falsi positivi. È possibile scegliere di analizzare il codice solo per i difetti ad impatto elevato. È inoltre possibile abilitare o disabilitare un difetto che non si desidera revisionare.
È inoltre possibile disabilitare alcuni difetti di Code Prover relativi alla mancata inizializzazione.
Zero falsi negativi con Code Prover
Code Prover mira a un'analisi esaustiva. Il software controlla ogni operazione che può causare tipi di errore specifici. Se un'operazione di codice è verde, significa che l'operazione non può causare gli errori di runtime che il software ha controllato. In questo modo, il software mira a zero falsi negativi.
Il risultato di Code Prover è valido solo se il codice viene eseguito nelle stesse condizioni fornite a Code Prover tramite le opzioni di analisi.
Se il software non può dimostrare l'assenza di un errore, evidenzia l'operazione sospetta in rosso o arancione e richiede di revisionare l'operazione.
Supporto delle regole di codifica in Bug Finder
Bug Finder supporta il controllo della conformità a standard di codifica esterni, quali:
AUTOSAR C++14. Vedere Regole AUTOSAR C++14.
MISRA C:2012. Vedere Direttive e regole MISRA C:2012.
MISRA C++:2008. Vedere Regole MISRA C++:2008.
CERT C. Vedere Regole e suggerimenti CERT C.
CERT C++. Vedere Regole CERT C++.
Per l'elenco completo degli standard di codifica supportati, vedere Polyspace Support for Coding Standards.
Vedi anche
Argomenti
- Workflow Using Both Polyspace Bug Finder and Polyspace Code Prover (Polyspace Code Prover)
