Warum sieht der Abhängigkeitsgraph dieses scanf() - Programms von Frama-C so aus?

Question

Ich benutze das Frama-C-Tool, um den Abhängigkeitsgraphen dieses Programms (main.c) zu erzeugen.

#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; 
    } 

Der Befehl lautet:

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

Das Ergebnis ist Meine Frage ist, warum die statments "m = m * i;", "m = m% 10000" Karte nicht zu Knoten. Das Ergebnis scheint nicht richtig zu sein, da der Code drei Schleifen enthält.

Answer 1

Eine Schneidemaschine für C-Programme funktioniert nur in der Praxis, wenn sein erklärtes Ziel zu bewahren definierten Hinrichtungen sind und die Schneidemaschine zu Änderung undefiniert Hinrichtungen erlaubt.

Andernfalls wäre der Slicer nicht in der Lage, eine Erklärung wie x = *p; so schnell zu entfernen, da sie nicht in der Lage ist, festzustellen, dass p ist ein gültiger Zeiger an diesem Punkt, auch wenn er weiß, dass es nicht x braucht, nur weil, wenn Die Anweisung wird entfernt. Ausführungen, bei denen an diesem Punkt NULL ist, werden geändert.

Frama-C verarbeitet keine komplexen Bibliotheksfunktionen wie scanf(). Aus diesem Grund wird davon ausgegangen, dass die lokale Variable n ohne Initialisierung verwendet wird.

Typ frama-c -val main.c Sie sollten eine Warnung wie erhalten:

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

Das Wort assert bedeutet, dass Frama-C Option -val nicht in der Lage ist, festzustellen, dass alle Ausführungen definiert sind, und „NON ABSCHLUSS FUNCTION“ bedeutet, dass es ist nicht in der Lage, eine einzige definierte Ausführung des Programms zu finden, von der aus fortgesetzt werden soll.

Die undefinierte Verwendung einer nicht initialisierten Variablen ist der Grund, warum das PDG die meisten Anweisungen entfernt. Der PDG-Algorithmus denkt, dass er sie entfernen kann, weil sie nach dem, was er für ein undefiniertes Verhalten hält, der erste Zugriff auf die Variable n ist.

I geändert Ihr Programm leicht den scanf() Anruf mit einer einfacheren Erklärung zu ersetzen:

#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; 
} 

und ich habe unter dem PDG. Soweit ich es beurteilen kann, sieht es komplett aus. Wenn Sie bessere Layoutprogramme als dot kennen, aber das Format dot akzeptieren, ist dies eine gute Gelegenheit, sie zu verwenden.

Beachten Sie, dass der Zustand des äussersten whiletmp != -1 wurde. Die Knoten des Graphen sind die Anweisungen einer internen normalisierten Darstellung des Programms. Die Bedingung tmp != -1 hat eine Datenabhängigkeit zum Knoten für die Anweisung tmp = unknown_int();.Sie können mit frama-c -print main.c die interne Darstellung angezeigt werden, und es wird zeigen, dass die äußerste Schleife Zustand eingebrochen wurde:

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

Dies trägt dazu bei, die unter anderem das Schneiden nur die Teile einer komplexen Aussage zu entfernen, kann entfernt werden, anstatt die gesamte komplexe Aussage zu behalten.