इस स्कैनफ() का निर्भरता ग्राफ क्यों है - Frama-C द्वारा प्रोग्राम का उपयोग इस तरह दिखता है?

Question

मैं इस प्रोग्राम (main.c) के निर्भरता ग्राफ उत्पन्न करने के लिए Frama-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; 
    } 

आदेश है:

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

परिणाम मेरा प्रश्न है क्यों statments "मीटर = मी * मैं," है, "मीटर = मी% 10000" से मैप नहीं नोड्स। नतीजा सही नहीं लगता है, क्योंकि कोड में तीन लूप हैं।

Answer 1

सी कार्यक्रमों के लिए एक स्लाइसर केवल व्यवहार में काम करता है, अगर उसके निर्धारित लक्ष्य को बनाए रखने परिभाषित फांसी है, और स्लाइसर परिवर्तन अपरिभाषित फांसी करने की अनुमति दी है।

अन्यथा, स्लाइसर रूप में जल्द ही इस तरह के x = *p; के रूप में एक बयान को दूर करने के रूप में यह निर्धारित करने के लिए कि p उस बिंदु पर एक मान्य सूचक है असमर्थ है असमर्थ होगा, भले ही वह जानता है कि यह x की जरूरत नहीं है, सिर्फ इसलिए कि अगर कथन हटा दिया गया है, निष्पादन जहां p उस बिंदु पर शून्य है।

Frama-C जटिल पुस्तकालय कार्यों जैसे scanf() को संभाल नहीं करता है। इस वजह से, यह सोचता है कि स्थानीय चर n प्रारंभ किए बिना उपयोग किया जाता है।

प्रकार frama-c -val main.c आप जैसा एक चेतावनी मिलना चाहिए:

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

शब्द assert मतलब यह है कि Frama सी विकल्प -val निर्धारित करने के लिए कि सभी सज़ाएँ परिभाषित कर रहे हैं असमर्थ है, और "गैर समाप्त फंक्शन" का अर्थ यह है कि जारी रखने के लिए कार्यक्रम के एक परिभाषित निष्पादन को खोजने में असमर्थ है।

एक अनियंत्रित चर का अपरिभाषित उपयोग पीडीजी अधिकांश बयानों को हटा देता है। पीडीजी एल्गोरिदम सोचता है कि यह उन्हें हटा सकता है क्योंकि वे जो सोचते हैं उसके बाद वे एक अनिर्धारित व्यवहार करते हैं, n परिवर्तनीय की पहली पहुंच।

मैं थोड़ा अपने कार्यक्रम संशोधित एक सरल बयान के साथ scanf() कॉल को बदलने के लिए:

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

और मैं PDG नीचे मिला है। जहां तक ​​मैं कह सकता हूं यह पूरा दिखता है। यदि आप dot से बेहतर लेआउट प्रोग्राम जानते हैं लेकिन यह dot प्रारूप स्वीकार करता है, तो यह उनका उपयोग करने का एक अच्छा मौका है।

ध्यान दें कि लगभग while की स्थिति tmp != -1 बन गई। ग्राफ के नोड्स कार्यक्रम के आंतरिक सामान्यीकृत प्रतिनिधित्व के बयान हैं। tmp != -1 की स्थिति tmp = unknown_int(); कथन के लिए नोड के लिए डेटा निर्भरता है।आप frama-c -print main.c के साथ आंतरिक प्रतिनिधित्व प्रदर्शित कर सकते हैं, और यह दिखा देंगे कि outmost पाश हालत में टूट कर दिया गया है

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

यह मदद करता है अन्य बातों के अलावा, टुकड़ा करने की क्रिया केवल एक जटिल बयान के कुछ हिस्सों को हटाने के लिए जो कर सकते हैं पूरे जटिल कथन को रखने के बजाय हटा दिया जाना चाहिए।