Perché il grafico di dipendenza di questo scanf() - usando il programma di Frama-C assomiglia a questo?

Question

Uso lo strumento Frama-C per generare il grafico di dipendenza di questo programma (main.c).

#include<stdio.h> 
    int main() 
    { 
     int n,i,m,j; 
     while(scanf("%d",&n)!=EOF) 
     { 
      m=n; 
      for(i=n-1;i>=1;i--) 
      { 
       m=m*i; 
       while(m%10==0) 
       { 
        m=m/10; 
       } 
       m=m%10000; 
      } 
      m=m%10; 
      printf("%5d -> %d\n",n,m); 
     } 
     return 0; 
    } 

Il comando è:

frama-c -pdg -dot-pdg main main.c 
    dot -Tpdf main.main.dot -o main.pdf 

Il risultato è mia domanda è perché le statments "m = m * i;", "m = m% 10000" non si mappano i nodi. Il risultato non sembra giusto, perché ci sono tre loop nel codice.

Answer 1

un'affettatrice per i programmi C funziona solo in pratica se il suo obiettivo è definito a esecuzioni preservare definiti, e l'affettatrice è permesso di cambiamento esecuzioni indefiniti.

In caso contrario, l'affettatrice non sarebbe in grado di rimuovere una dichiarazione come x = *p; non appena è in grado di determinare che p è un puntatore valido a quel punto, anche se si sa che non ha bisogno di x, proprio perché se la dichiarazione è stata rimossa, le esecuzioni in cui p è NULL in quel punto sono state modificate.

Frama-C non gestisce funzioni di libreria complesse come scanf(). Per questo motivo, la variabile locale n viene utilizzata senza essere inizializzata.

Tipo frama-c -val main.c Si dovrebbe ottenere un avvertimento del tipo:

main.c:10:[kernel] warning: accessing uninitialized left-value: 
       assert \initialized(&n); 
... 
[value] Values for function main: 
     NON TERMINATING FUNCTION 

La parola assert significa che l'opzione di Frama-C -val è in grado di stabilire che tutte le esecuzioni vengono definiti, e "CHIUSURA FUNZIONE NON" significa che non è in grado di trovare una singola esecuzione definita del programma da cui continuare.

L'uso indefinito di una variabile non inizializzata è la ragione per cui il PDG rimuove la maggior parte delle istruzioni. L'algoritmo PDG pensa di poterli rimuovere perché vengono dopo quello che pensa sia un comportamento non definito, il primo accesso alla variabile n.

ho modificato un po 'il vostro programma per sostituire la chiamata scanf() con una dichiarazione semplice:

#define EOF (-1) 
int unknown_int(); 

int scan_unknown_int(int *p) 
{ 
    *p = unknown_int(); 
    return unknown_int(); 
} 

int main() 
{ 
    int n,i,m,j; 
    while(scan_unknown_int(&n) != EOF) 
    { 
     m=n; 
     for(i=n-1;i>=1;i--) 
     { 
     m=m*i; 
     while(m%10==0) 
     { 
      m=m/10; 
     } 
     m=m%10000; 
     } 
     m=m%10; 
     printf("%5d -> %d\n",n,m); 
    } 
    return 0; 
} 

e ho ottenuto il PDG di seguito. Sembra completo per quanto posso dire. Se conosci programmi di impaginazione migliori di dot ma che accettano il formato dot, questa è una buona possibilità di usarli.

Nota che la condizione del outmost while divenne tmp != -1. I nodi del grafico sono le dichiarazioni di una rappresentazione normalizzata interna del programma. La condizione tmp != -1 ha una dipendenza dai dati per il nodo per l'istruzione tmp = unknown_int();.È possibile visualizzare la rappresentazione interna con frama-c -print main.c, e mostrerà che la condizione del ciclo più esterno è stato suddiviso in:

while (1) { 
    int tmp; 
    tmp = scan_unknown_int(& n); 
    if (! (tmp != -1)) { break; } 

Ciò contribuisce, tra l'altro, le operazioni di affettamento per rimuovere solo le parti di una dichiarazione complessa che può essere rimosso invece di dover mantenere l'intera dichiarazione complessa.