गोटो-सीसी - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

सीबीएमसी - सी/सी++ और जावा प्रोग्राम के लिए बाउंडेड मॉडल चेकर

SYNOPSIS

सीबीएमसी [--संपत्ति संपत्ति-आईडी] फ़ाइल.सी ...

सीबीएमसी [--प्रदर्शन-गुण] फ़ाइल.सी ...

सीबीएमसी [--सभी-गुण] फ़ाइल.सी ...

गोटो-सीसी [-मैं शामिल-पथ] [-सी] फ़ाइल.सी [-ओर आउटफ़ाइल.ओ]

गोटो-यंत्र फाइल में आउटफाइल

केवल सबसे उपयोगी विकल्प यहां सूचीबद्ध हैं; शेष के लिए नीचे देखें।

वर्णन

सीबीएमसी ऐसे निशान उत्पन्न करता है जो दर्शाता है कि किसी दावे का उल्लंघन कैसे किया जा सकता है, या यह साबित करता है
लूप पुनरावृत्तियों की दी गई संख्या के भीतर दावे का उल्लंघन नहीं किया जा सकता है। सीबीएमसी पढ़ सकते हैं
स्रोत-कोड सीधे, या गोटो-सीसी द्वारा उत्पन्न गोटो-बाइनरी। जावा प्रोग्राम इस प्रकार दिए गए हैं
क्लास फ़ाइलें. बिना किसी अन्य विकल्प के, सीबीएमसी सभी संपत्तियों की जांच (स्वचालित रूप से) करती है
उत्पन्न या उपयोगकर्ता द्वारा निर्दिष्ट) प्रोग्राम में पाया गया। यदि कोई गुण हो सकता है
उल्लंघन होने पर, एक प्रति-उदाहरण मुद्रित किया जाता है और विश्लेषण निरस्त कर दिया जाता है। विश्लेषण हो सकता है
--संपत्ति विकल्प के साथ किसी विशेष संपत्ति तक सीमित। सत्यापन परिणाम
सभी संपत्तियों को --all-properties विकल्प के माध्यम से प्राप्त किया जा सकता है।

गोटो-सीसी स्रोत कोड पढ़ता है, और एक गोटो-बाइनरी उत्पन्न करता है। इसका कमांड-लाइन इंटरफ़ेस है
की नकल करने के लिए डिज़ाइन किया गया है जीसीसी(1). उस पर विशेष ध्यान दें गोटो-सीसी के बीच अंतर करता है
जीसीसी की तरह ही चरणों को संकलित और लिंक करना। सीबीएमसी जिसके लिए एक गोटो-बाइनरी की अपेक्षा है
लिंकिंग का काम पूरा हो गया है.

गोटो-यंत्र एक गोटो-बाइनरी पढ़ता है, दिए गए प्रोग्राम परिवर्तन करता है, और फिर
परिणामी प्रोग्राम को डिस्क पर गोटो-बाइनरी के रूप में लिखता है।

सामान्य प्रवाह है (1) गोटो-सीसी का उपयोग करके स्रोत को गोटो-बाइनरी में अनुवाद करना, फिर (2)
गोटो-इंस्ट्रूमेंट के साथ इंस्ट्रुमेंटेशन करें और अंत में (3) विश्लेषण करें
सीबीएमसी.

विकल्प

दृश्यपटल विकल्प (सीबीएमसी और गोटो-सीसी)
-मैं पथ
सेट में पथ शामिल है (C/C++)

-डी मैक्रो
प्रीप्रोसेसर मैक्रो को परिभाषित करें (C/C++)

--प्रीप्रोसेस
प्रीप्रोसेसिंग के बाद रुकें

--शो-प्रतीक-तालिका
प्रतीक तालिका दिखाएँ

--शो-गोटो-फ़ंक्शन
गोटो प्रोग्राम दिखाएँ

वास्तु विकल्प (सीबीएमसी और गोटो-सीसी)
सीबीएमसी डिफ़ॉल्ट रूप से मशीन से मेल खाने वाली आर्किटेक्चरल सेटिंग्स का उपयोग करता है सीबीएमसी is
पर क्रियान्वित किया जाता है, अर्थात, नीचे दी गई सेटिंग्स की आवश्यकता केवल सॉफ़्टवेयर को सत्यापित करते समय होती है
इसका मतलब एक अलग आर्किटेक्चर या ओएस पर चलना है। गोटो-सीसी के लिए एक गोटो-बाइनरी उत्पन्न करता है
विशेष आर्किटेक्चर, यानी, गोटो-बाइनरी के बाद आर्किटेक्चर को बदला नहीं जा सकता है
उत्पन्न।

--16, --32, --64
इंट की चौड़ाई निर्धारित करें

--एलपी64, --आईएलपी64, --एलएलपी64, --आईएलपी32, --एलपी32
इंट, लॉन्ग और पॉइंटर्स की चौड़ाई निर्धारित करें

--छोटा एंडियन
छोटे-छोटे शब्द-बाइट रूपांतरणों की अनुमति दें

--बड़े एंडियन
बड़े-एंडियन शब्द-बाइट रूपांतरण की अनुमति दें

--अचिन्हित वर्ण
डिफ़ॉल्ट रूप से "char" को अहस्ताक्षरित बनाएं

--आर्च लक्ष्य आर्किटेक्चर सेट करें

--ओएस लक्ष्य ऑपरेटिंग सिस्टम सेट करें

--नो-मेहराब
कोई आर्किटेक्चर स्थापित न करें

--कोई पुस्तकालय नहीं
अंतर्निहित अमूर्त सी लाइब्रेरी को अक्षम करें

--राउंड-टू-निकटतम, --राउंड-टू-प्लस-इनफ़, --राउंड-टू-माइनस-इनफ़, --राउंड-टू-ज़ीरो
प्रोग्राम शुरू होने पर आईईईई फ़्लोटिंग पॉइंट राउंडिंग मोड का उपयोग करें (डिफ़ॉल्ट राउंड है
निकटतम)। सत्यापन के तहत प्रोग्राम इस सेटिंग को ओवरराइड कर सकता है, उदाहरण के लिए, के साथ
fesetround(3).

PROGRAM इंस्ट्रुमेंटेशन विकल्प (सीबीएमसी और गोटो-यंत्र)
दोनों सीबीएमसी और गोटो-यंत्र ऐसे दावे उत्पन्न कर सकते हैं जो विशिष्ट सामान्य त्रुटियों को पकड़ते हैं,
जैसा कि नीचे सूचीबद्ध है।

--बाउंड-चेक
सरणी सीमा जांच सक्षम करें

--डिव-बाय-जीरो-चेक
शून्य जांच द्वारा विभाजन सक्षम करें

--पॉइंटर-चेक
सूचक जाँच सक्षम करें

--हस्ताक्षरित-अतिप्रवाह-जाँच
हस्ताक्षरित पूर्णांक अंकगणित के लिए अंकगणित ओवर- और अंडरफ्लो जांच सक्षम करें

--अहस्ताक्षरित-अतिप्रवाह-जाँच
अहस्ताक्षरित पूर्णांक अंकगणित के लिए अंकगणित ओवर- और अंडरफ्लो जांच सक्षम करें

--नान-चेक
NaN के लिए फ़्लोटिंग-पॉइंट गणनाओं की जाँच करें

--नहीं-अभिकथन
उपयोगकर्ता द्वारा प्रदत्त दावों पर ध्यान न दें

-- कोई धारणा नहीं
उपयोगकर्ता द्वारा प्रदत्त धारणाओं पर ध्यान न दें

--त्रुटि-लेबल लेबल
जांचें कि दिया गया लेबल पहुंच योग्य नहीं है

PROGRAM इंस्ट्रुमेंटेशन विकल्प (गोटो-यंत्र केवल)
गोटो-यंत्र आगे, अधिक जटिल, प्रोग्राम परिवर्तनों का समर्थन करता है।

--नॉन्डेट-वाष्पशील
अस्थिर चरों से पढ़ने को गैर-नियतात्मक बनाता है

--आईएसआर फ़ंक्शन
दिए गए नाम के साथ एक व्यवधान सेवा रूटीन उपकरण

--mmio इंस्ट्रूमेंट्स मेमोरी-मैप्ड I/O

--नॉन्डेट-स्टैटिक
स्थैतिक जीवनकाल वाले चर को गैर-नियतात्मक रूप से प्रारंभ किया जाता है

--डंप-सी
गोटो बाइनरी के बजाय एएनएसआई-सी स्रोत कोड आउटपुट करें।

बीएमसी विकल्प (सीबीएमसी)
--सभी-गुण
सभी संपत्तियों की स्थिति रिपोर्ट करें

--शो-गुण
केवल गुण दिखाएं

--शो-लूप
प्रोग्राम में लूप दिखाएं

--कवर-दावे
जांचें कि कौन से दावे पहुंच योग्य हैं

--फ़ंक्शन नाम
मुख्य फ़ंक्शन नाम सेट करें

--संपत्ति आईडी
केवल दिए गए पहचानकर्ता के साथ विशिष्ट संपत्ति की जाँच करें

--केवल-कार्यक्रम
केवल प्रोग्राम अभिव्यक्ति दिखाएँ

--गहराई एन.आर
खोज की गहराई सीमित करें

--अनविंड एनआर
लूप को एनआर बार खोलें

--अनविंडसेट एल:बी,...
बी की सीमा के साथ लूप एल को खोलें (लूप आईडी प्राप्त करने के लिए --शो-लूप का उपयोग करें)

--दिखाएँ-vcc
सत्यापन शर्तें दिखाएं

--स्लाइस-सूत्र
संपत्ति से असंबंधित असाइनमेंट हटाएं

--कोई-अनचाहा-दावा नहीं
अनचाहे दावे न उत्पन्न करें

--कोई-सुंदर-नाम नहीं
पहचानकर्ताओं को सरल न बनाएं

बैकएंड विकल्प (सीबीएमसी)
--dimacs
बाहरी SAT सॉल्वरों द्वारा उपयोग के लिए DIMACS प्रारूप में CNF उत्पन्न करें

--सुंदरीकरण-लोलुप
प्रतिउदाहरण को सुशोभित करें (लालची अनुमानी)

--smt1 SMT1 सिंटैक्स में आउटपुट उपलक्ष्य (प्रयोगात्मक)

--smt2 SMT2 सिंटैक्स में आउटपुट उपलक्ष्य (प्रयोगात्मक)

--बूलेक्टर
बूलेक्टर का प्रयोग करें (प्रायोगिक)

--मैथसैट
मैथसैट का प्रयोग करें (प्रायोगिक)

--cvc CVC3 का उपयोग करें (प्रयोगात्मक)

--हाँ
Yices का प्रयोग करें (प्रायोगिक)

--z3 Z3 का उपयोग करें (प्रायोगिक)

--परिष्कृत
शोधन प्रक्रिया का उपयोग करें (प्रायोगिक)

--आउटफ़ाइल फ़ाइल नाम
दी गई फ़ाइल में आउटपुट सूत्र

--सरणी-यूएफ-कभी नहीं
सरणियों को कभी भी अव्याख्यायित फ़ंक्शंस में न बदलें

--सरणी-यूएफ-हमेशा
सरणियों को हमेशा अनिर्वचनीय फ़ंक्शंस में बदलें

वातावरण

अस्थायी फ़ाइलें बनाते समय सभी उपकरण TMPDIR पर्यावरण चर का सम्मान करते हैं
निर्देशिकाएँ इसके अलावा ध्यान दें कि सीबीएमसी द्वारा उपयोग किया जाने वाला प्रीप्रोसेसर पर्यावरण का उपयोग करेगा
हेडर फ़ाइलों का पता लगाने के लिए वेरिएबल। GOTO-CC का लक्ष्य सभी पर्यावरण चर को स्वीकार करना है
जीसीसी करता है.

कॉपीराइट

2001-2014, डैनियल क्रोनिंग, एडमंड क्लार्क

onworks.net सेवाओं का उपयोग करके ऑनलाइन गोटो-सीसी का उपयोग करें