शैतान विवरण में है, लेकिन यह आप के लिए काम कर सकते हैं:
पहले, Frama-C मिलता है। यदि आप यूनिक्स का उपयोग कर रहे हैं, तो आपके वितरण में एक पैकेज हो सकता है। पैकेज अंतिम संस्करण नहीं होगा लेकिन यह काफी अच्छा हो सकता है और यदि आप इसे इस तरह इंस्टॉल करते हैं तो यह आपको कुछ समय बचाएगा।
मान लें कि आपका उदाहरण के रूप में नीचे केवल इतना बड़ा है कि यह स्पष्ट नहीं है कि क्या गलत है,:
int add(int x, int y)
{
static int state;
int result = x + y + state; // I tested it once and it worked.
state++;
return result;
}
प्रकार की तरह एक आदेश:
frama-c -lib-entry -main add -deps ugly.c
विकल्प -lib-entry -main add मतलब है "समारोह add को देखो "। विकल्प -deps कार्यात्मक निर्भरताओं की गणना करता है। आप लॉग में इन "कार्यात्मक निर्भरता" मिल जाएगा:
[from] Function add:
state FROM state; (and default:false)
\result FROM x; y; state; (and default:false)
यह वास्तविक आदानों add के परिणामों पर निर्भर है, और वास्तविक आउटपुट इन इनपुट की गणना से पढ़ा स्थैतिक चर सहित सूचीबद्ध करता है और संशोधित। उपयोग किए जाने से पहले ठीक से प्रारंभ किया गया एक स्थैतिक चर सामान्य रूप से इनपुट के रूप में प्रकट नहीं होता है, जब तक कि विश्लेषक यह निर्धारित करने में असमर्थ था कि इसे हमेशा पढ़ने से पहले प्रारंभ किया गया था।
लॉग \result की निर्भरता के रूप में दिखाता है। यदि आपको लौटाया गया परिणाम केवल तर्कों पर निर्भर करता है (जिसका अर्थ है कि एक ही तर्क के साथ दो कॉल एक ही परिणाम उत्पन्न करते हैं), यह संकेत है कि परिवर्तनीय state के साथ यहां कुछ गड़बड़ हो सकती है।
उपर्युक्त पंक्तियों में दिखाया गया एक और संकेत यह है कि फ़ंक्शन state संशोधित करता है।
इससे मदद मिल सकती है या नहीं। विकल्प का अर्थ है कि विश्लेषक यह नहीं मानता कि किसी भी गैर-स्थिर स्थैतिक चर ने विश्लेषण के दौरान कार्य को उस समय अपना मूल्य रखा है, ताकि आपके कोड के लिए यह बहुत ही कम हो सके। इसके आस-पास के तरीके हैं, लेकिन फिर यह आप पर निर्भर करता है कि क्या आप इन तरीकों को सीखने के लिए समय लेना चाहते हैं।
संपादित करें: यहाँ एक अधिक जटिल उदाहरण है:
void initialize_1(int *p)
{
*p = 0;
}
void initialize_2(int *p)
{
*p; // I made a mistake here.
}
int add(int x, int y)
{
static int state1;
static int state2;
initialize_1(&state1);
initialize_2(&state2);
// This is safe because I have initialized state1 and state2:
int result = x + y + state1 + state2;
state1++;
state2++;
return result;
}
इस उदाहरण पर, एक ही आदेश परिणाम का उत्पादन:
[from] Function initialize_1:
state1 FROM p
[from] Function initialize_2:
[from] Function add:
state1 FROM \nothing
state2 FROM state2
\result FROM x; y; state2
क्या आप initialize_2 के लिए देख निर्भरता की एक खाली सूची है, जिसका अर्थ है कि फ़ंक्शन कुछ भी निर्दिष्ट नहीं करता है। मैं सिर्फ एक खाली सूची के बजाय एक स्पष्ट संदेश प्रदर्शित करके इस मामले को स्पष्ट कर दूंगा। यदि आप जानते हैं कि initialize_1, initialize_2 या add का कोई भी कार्य क्या करना है, तो आप विश्लेषण के परिणामों के लिए एक प्राथमिक ज्ञान की तुलना कर सकते हैं और देख सकते हैं कि initialize_2 और add के लिए कुछ गलत है।
दूसरा संपादित करें: और अब मेरा उदाहरण initialize_1 के लिए कुछ अजीब दिखाता है, तो शायद मुझे यह समझा जाना चाहिए। परिवर्तनीय state1p पर इस बात पर निर्भर करता है कि pstate1 पर लिखने के लिए उपयोग किया जाता है, और यदि p अलग था, तो state1 का अंतिम मान अलग-अलग होगा। यहाँ एक आखिरी उदाहरण है:
int t[10];
void initialize_index(int i)
{
t[i] = 1;
}
int main(int argc, char **argv)
{
initialize_index(argv[1][0]-'0');
}
आदेश
frama-c -deps t.c साथ
, निर्भरता initialize_index गणना कर रहे हैं: यदि i है
[from] Function initialize_index:
t[0..9] FROM i (and SELF)
इसका मतलब है कि कोशिकाओं के प्रत्येक i पर निर्भर करता है (यह संशोधित किया जा सकता उस विशेष सेल की अनुक्रमणिका)। प्रत्येक सेल भी अपना मान रख सकता है (यदि i कोई अन्य सेल इंगित करता है): यह नवीनतम संस्करण में (and SELF) उल्लेख के साथ इंगित किया गया है, और पिछले संस्करणों में एक अधिक अस्पष्ट (and default:true) के साथ संकेत दिया गया था।
दिलचस्प सवाल है, लेकिन वालग्रिंड को "स्थानीय" या "घोषित" का कोई ज्ञान नहीं है। मुझे लगता है कि यह कोड विश्लेषण द्वारा किया जाना चाहिए, निष्पादन योग्य विश्लेषण नहीं। – aschepler
हम पीसी लिंट का उपयोग करते हैं, लेकिन यह बहुत सारी चेतावनियों का नरक उत्पन्न करता है ताकि वास्तविक हॉटस्पॉट को कभी-कभी अंधेरे में मछली पकड़ने की तरह मिल सके। –