Sto cercando uno strumento in grado di scoprire staticamente le invarianti nei programmi in C. Ho controllato Daikon ma scopre gli invarianti solo in modo dinamico.Esiste uno strumento di individuazione invariabile statico per i programmi C?
Esiste uno strumento a disposizione per quello che sto cercando? Grazie!
Se si intende "invariante" nel senso più ampio, poiché la pagina collegata a Daikon è in uso, il lavoro di molti strumenti di analisi statici può essere descritto come "scoperta di invarianti", solo forse non gli invarianti espressivi che si stavano cercando per.
L'analisi del valore di Frama-C accumula i suoi risultati, i valori possibili di tutte le variabili, per ogni affermazione. Alla fine dell'analisi, può quindi presentare informazioni non relazionali sulla variazione del dominio di ciascuna variabile nel programma, ad ogni affermazione. In this screenshot, un invariante è che S è sempre 0, 1, 3 o 6 appena prima dell'istruzione selezionata, per tutte le esecuzioni di questo programma deterministico.
I due parametri nascosti nella tua domanda sono la forma degli invarianti che ti interessano, e la forma dei programmi per cui vuoi trovare questi invarianti. Ad esempio, lo SLAM, menzionato nella risposta di Ira, è stato progettato per funzionare sul codice del driver del dispositivo e per inferire invarianti che contengono solo le informazioni necessarie per verificare l'uso corretto delle API di sistema. Un altro strumento, Astrée, è famoso per fare un ottimo lavoro nel dedurre solo gli invarianti giusti per dimostrare la sicurezza runtime del software di controllo del volo.
I due gradi di libertà creano uno spazio di design molto ampio. Non troverai nulla che funzioni per tutti i tipi di programmi C e non fornirai tutti gli invarianti a cui potresti essere interessato, ma se raffini la tua domanda per domini applicativi e tipi di invarianti specifici, avrai maggiori possibilità di trovare risposte pertinenti.
Vedere The SLAM project: debugging system software via static analysis. Dichiara di dedurre staticamente le invarianti, proprio per quello che hai chiesto, il linguaggio C. L'autore, Tom Ball, è ampiamente noto per il lavoro stellare nell'analisi del programma.
Ciao, grazie per la risposta. Sono interessato alle invarianti con una struttura semplice come intervalli (caselle). Penso che l'analisi del valore di Frama-C sia migliore in quanto fornisce anche valori specifici e non solo intervalli. –
@VijayaraghavanMurali Bene, ci sono tutti i tipi di compromessi su quali informazioni conservare e quali informazioni buttare via, e per esempio, l'analisi del valore di Frama-C mantiene serie di valori solo fino a 8 elementi, quindi passa ad intervalli con informazioni di congruenza. Questo è per i numeri interi. Per 'float' e' double', usa solo l'intervallo, per riflettere il fatto che questi non sono spesso usati per rappresentare valori discreti con significato individuale. E per gli indirizzi ... i dettagli sono in http://frama-c.com/download/frama-c-value-analysis.pdf –