Dlaczego wykres zależności tego scanf() - używania programu przez Frama-C wygląda tak?

Question

Używam narzędzia Frama-C do generowania wykresu zależności tego programu (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; 
    } 

Polecenie brzmi:

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

Rezultatem jest Moje pytanie brzmi, dlaczego statments "m = m * i;", "m = m% 10000" nie mapować węzły. Wynik nie wydaje się właściwy, ponieważ w kodzie znajdują się trzy pętle.

Answer 1

krajalnicy dla programów C działa tylko w praktyce, jeśli jego celem jest zdefiniowana do zachować określone egzekucje i krajalnica wolno zmian nieokreślonych egzekucji.

Inaczej, krajalnica byłby w stanie usunąć oświadczenie takie jak x = *p; tak szybko, jak to jest w stanie określić, że p to ważny wskaźnik w tym punkcie, nawet jeśli wie, że nie musi x, tylko dlatego, że jeśli instrukcja zostanie usunięta, zmienione zostają wykonania, w których p ma wartość NULL.

Frama-C nie obsługuje złożonych funkcji bibliotecznych, takich jak scanf(). Z tego powodu uważa, że ​​lokalna zmienna n jest używana bez inicjalizacji.

Rodzaj frama-c -val main.c Powinieneś dostać ostrzeżenie jak:

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

Słowo assert oznacza, że ​​opcja Frama-C za -val nie jest w stanie ustalić, że wszystkie egzekucje są zdefiniowane i „NON kończące FUNCTION” oznacza, że nie może znaleźć pojedynczego określonego programu, z którego można kontynuować.

Nieokreślone użycie niezainicjowanej zmiennej jest powodem, dla którego PDG usuwa większość instrukcji. Algorytm PDG myśli, że może je usunąć, ponieważ przychodzą po tym, co uważa się za niezdefiniowane zachowanie, pierwszy dostęp do zmiennej n.

zmodyfikowałem nieco swój program, aby zastąpić połączenia scanf() z prostszej stwierdzeniem:

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

i mam PDG poniżej. Wygląda na kompletny, o ile wiem. Jeśli znasz lepsze programy układowe niż dot, ale akceptują format dot, jest to dobra okazja, aby z nich korzystać.

Należy zauważyć, że warunek napotykanym while stał tmp != -1. Węzły wykresu są wyrażeniami wewnętrznej znormalizowanej reprezentacji programu. Warunek tmp != -1 ma zależność danych od węzła dla instrukcji tmp = unknown_int();.Można wyświetlić reprezentację wewnętrzną z frama-c -print main.c, i pokaże, że niezmiernie warunek pętli zostały podzielone na:

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

pomaga to, między innymi, krojenie, aby usunąć jedynie części złożonego oświadczenia, które mogą być usunięte zamiast konieczności przechowywania całego złożonego oświadczenia.