2012-03-21 10 views

risposta

16

Frama-C è una piattaforma di analisi statica Open Source con a slicer for C programs basata sul calcolo di un grafico di dipendenza del programma.

Si noti che l'affettamento di programmi reali scritti in un linguaggio di programmazione reale come C coinvolge molti casi e concetti speciali che vengono sfogliati nelle pubblicazioni scientifiche. Tuttavia, sono fiducioso che non troverete nulla di più semplice del calcolo del PDG di Frama-C, in primo luogo perché è l'unico Open Source disponibile (che io sappia), e in secondo luogo perché qualsiasi altro calcolo del PDG che gestiva i programmi C avrebbe avuto per risolvere gli stessi problemi e introdurre gli stessi concetti.

Ecco un esempio:

int a, b, d, *p; 

int f (int x) { 
    return a + x; 
} 

int main (int c, char **v) { 
    p = &b; 
    a = 1; 
    *p = 2; 
    d = 3; 
    c = f(b); 
} 

Il comando frama-c -pdg -dot-pdg graph -pdg-print t.c genera file punto graph.main.dot e graph.f.dot contenenti, rispettivamente, il PDG di main() e f().

È possibile utilizzare il programma di dot a pretty-print uno di loro così: dot -Tpdf graph.main.dot > graph.pdf

Il risultato è al di sotto:

PDG of main()

nota il bordo dal nodo c = f(b); al nodo *p = 2;. Un calcolo PDG che sostiene di essere utile per i programmi C deve gestire l'aliasing.

D'altra parte, un'affettatrice utilizza questo PDG tagliare sul criterio “input di istruzione c = f(b);” sarebbe in grado di rimuovere d = 3;, che non può influenzare la chiamata di funzione, anche attraverso l'accesso puntatore *p. L'affettatrice di Frama-C utilizza le dipendenze indicate dal PDG per mantenere solo le istruzioni che sono utili per il criterio di slicing specificato dall'utente. Ad esempio, il comando frama-c -slice-wr c t.c -then-on 'Slicing export' -print produce il programma ridotta sottostante, dove l'assegnazione di d è stato rimosso:

/* Generated by Frama-C */ 
int a; 
int b; 
int *p; 
int f_slice_1(int x) 
{ 
    int __retres; 
    __retres = a + x; 
    return (__retres); 
} 

void main(int c) 
{ 
    p = & b; 
    a = 1; 
    *p = 2; 
    c = f_slice_1(b); 
    return; 
} 
+0

grazie mille per il tuo notevole aiuto. Sto iniziando a imparare come usare Frama-C. Nel riferimento di Frama-C, non riesco a trovare il meanning della linea nel grafico graph.main.dot. Cosa significano i diversi stili di linea? o c'è materiale su questo. – user1283336

+0

@ user1283336 Esistono 3 tipi di frecce: rispettivamente dipendenze di dati, controllo e indirizzi. Il programma 'int a, b, * p; void main (int x, int y, int z) { p = & a; * p = x; if (y) b = z; } 'contiene tutti i 3 tipi di dipendenze. Usando le stesse linee di comando del primo esempio, non dovresti avere difficoltà a riconoscere quale è quale. Non esiste una descrizione disponibile dall'utente delle parti interne dell'affettatrice, mi dispiace, solo una descrizione esterna di come usarlo. –

+1

Penso che debba essere '-pdg-dot' piuttosto che' -dot-pdg' giusto? Almeno per me ha funzionato solo nel modo precedente – Paddre

4

Se si desidera visualizzare le dipendenze dei metodi che si chiamano a vicenda e utilizzano gcc, l'opzione -fdump-rtl-expand di gcc potrebbe essere di vostro interesse.

Per ogni file sorgente compilato utilizzando l'opzione -fdump-rtl-expandgcc verrà emesso un file *.expand.

Questi file alimentati allo strumento egypt producono grafici (s) che mostrano le dipendenze del metodo.

+0

Un PDG è un grafico cui nodi sono istruzioni. Vedi ad esempio http://www.grammatech.com/research/papers/slicing/slicingWhitepaper.html –

Problemi correlati