এটি হল goto-cc কমান্ড যা আমাদের একাধিক বিনামূল্যের অনলাইন ওয়ার্কস্টেশন যেমন উবুন্টু অনলাইন, ফেডোরা অনলাইন, উইন্ডোজ অনলাইন এমুলেটর বা MAC OS অনলাইন এমুলেটর ব্যবহার করে OnWorks ফ্রি হোস্টিং প্রদানকারীতে চালানো যেতে পারে।
কার্যক্রম:
NAME এর
cbmc - C/C++ এবং জাভা প্রোগ্রামের জন্য বাউন্ডেড মডেল চেকার
সাইনোপিসিস
cbmc [---সম্পত্তি সম্পত্তি-আইডি] file.c ...
cbmc [-শো-সম্পত্তি] file.c ...
cbmc [---সমস্ত-সম্পত্তি] file.c ...
goto-cc [-আমি অন্তর্ভুক্ত-পথ] [-গ] file.c [-ও outfile.o]
goto-যন্ত্র ইনফাইল আউটফাইল
শুধুমাত্র সবচেয়ে দরকারী বিকল্প এখানে তালিকাভুক্ত করা হয়; বাকি জন্য নীচে দেখুন.
বর্ণনাঃ
cbmc এমন চিহ্ন তৈরি করে যা প্রদর্শন করে যে কীভাবে একটি দাবি লঙ্ঘন করা যেতে পারে, বা প্রমাণ করে
একটি নির্দিষ্ট সংখ্যক লুপ পুনরাবৃত্তির মধ্যে দাবী লঙ্ঘন করা যাবে না। CBMC পড়তে পারেন
সোর্স-কোড সরাসরি, বা goto-cc দ্বারা উত্পন্ন একটি গোটো-বাইনারি। জাভা প্রোগ্রাম হিসাবে দেওয়া হয়
ক্লাস ফাইল। আর কোন বিকল্প ছাড়াই, cbmc সমস্ত বৈশিষ্ট্য পরীক্ষা করে (স্বয়ংক্রিয়ভাবে
উৎপন্ন বা ব্যবহারকারী-নির্দিষ্ট) প্রোগ্রামে পাওয়া যায়। যদি কোন সম্পত্তি হতে পারে
লঙ্ঘন করা হয়, একটি পাল্টা উদাহরণ মুদ্রিত হয় এবং বিশ্লেষণ বাতিল করা হয়। বিশ্লেষণ হতে পারে
--property বিকল্পের সাথে একটি নির্দিষ্ট সম্পত্তিতে সীমাবদ্ধ। যাচাইকরণের ফলাফল
সমস্ত বৈশিষ্ট্যের জন্য --all-properties বিকল্পের মাধ্যমে প্রাপ্ত করা যেতে পারে।
goto-cc সোর্স কোড পড়ে এবং একটি গোটো-বাইনারী তৈরি করে। এর কমান্ড-লাইন ইন্টারফেস
এর নকল করার জন্য ডিজাইন করা হয়েছে জিসিসি(1)। বিশেষ করে নোট করুন যে goto-cc মধ্যে পার্থক্য করে
কম্পাইলিং এবং লিংকিং ফেজ, ঠিক যেমন gcc করে। cbmc যার জন্য একটি গোটো-বাইনারী আশা করে
লিঙ্কিং সম্পন্ন হয়েছে।
goto-যন্ত্র একটি গোটো-বাইনারী পড়ে, একটি প্রদত্ত প্রোগ্রাম রূপান্তর সম্পাদন করে এবং তারপরে
ডিস্কে গোটো-বাইনারী হিসাবে ফলাফল প্রোগ্রাম লেখে।
স্বাভাবিক প্রবাহ হল (1) গোটো-সিসি ব্যবহার করে উৎসকে একটি গোটো-বাইনারিতে অনুবাদ করা, তারপর (2)
গোটো-ইন্সট্রুমেন্টের সাহায্যে ইন্সট্রুমেন্টেশন সঞ্চালন করুন এবং অবশেষে (3) এর সাথে বিশ্লেষণ করুন
cbmc
বিকল্প
ফ্রন্টএন্ড বিকল্প (cbmc এবং goto-cc)
-আমি পথ
অন্তর্ভুক্ত পথ সেট করুন (C/C++)
-ডি ম্যাক্রো
প্রিপ্রসেসর ম্যাক্রো (C/C++) সংজ্ঞায়িত করুন
--প্রিপ্রসেস
প্রিপ্রসেসিং পরে থামুন
--প্রতীক-সারণী দেখান
প্রতীক টেবিল দেখান
--শো-গোটো-ফাংশন
গোটো প্রোগ্রাম দেখান
শিল্পকলা বিকল্প (cbmc এবং goto-cc)
cbmc ডিফল্টরূপে স্থাপত্য সেটিংস ব্যবহার করে যা মেশিনের সাথে মেলে cbmc is
সফ্টওয়্যার যাচাই করার সময় নিচের সেটিংস শুধুমাত্র প্রয়োজন হয়
একটি ভিন্ন আর্কিটেকচার বা OS এ চালানোর জন্য বোঝানো হয়েছে। goto-cc a এর জন্য একটি গোটো-বাইনারী তৈরি করে
নির্দিষ্ট আর্কিটেকচার, অর্থাৎ, গোটো-বাইনারির পরে আর্কিটেকচার পরিবর্তন করা যাবে না
উত্পন্ন
--16, --32, --64
int এর প্রস্থ সেট করুন
--LP64, --ILP64, --LLP64, --ILP32, --LP32
int, দীর্ঘ এবং পয়েন্টার প্রস্থ সেট করুন
--সামান্য endian
লিটল-এন্ডিয়ান ওয়ার্ড-বাইট রূপান্তরের অনুমতি দিন
--বড় endian
বড়-এন্ডিয়ান ওয়ার্ড-বাইট রূপান্তরের অনুমতি দিন
-- স্বাক্ষরবিহীন চর
ডিফল্টরূপে "char" আনসাইনড করুন
--arch সেট টার্গেট আর্কিটেকচার
--os টার্গেট অপারেটিং সিস্টেম সেট করুন
--নো-খিলান
একটি আর্কিটেকচার সেট আপ করবেন না
--কোন-লাইব্রেরি
বিল্ট-ইন অ্যাবস্ট্রাক্ট সি লাইব্রেরি অক্ষম করুন
--বৃত্তাকার থেকে নিকটতম, --রাউন্ড-থেকে-প্লাস-ইনফ, --রাউন্ড-থেকে-বিয়োগ-ইনফ, --রাউন্ড-থেকে-শূন্য
প্রোগ্রাম শুরু হলে IEEE ফ্লোটিং পয়েন্ট রাউন্ডিং মোড ব্যবহার করতে হবে (ডিফল্ট রাউন্ড
নিকটতম)। যাচাইকরণের অধীনে থাকা প্রোগ্রামটি এই সেটিংটিকে ওভাররাইড করতে পারে, যেমন, এর সাথে
উত্সব(3).
প্রোগ্রাম ইন্সট্রুমেন্টেশন বিকল্প (cbmc এবং গোটো-যন্ত্র)
উভয় cbmc এবং goto-যন্ত্র নির্দিষ্ট সাধারণ ত্রুটি ধরার দাবী তৈরি করতে পারে,
নিচে তালিকাভুক্ত হিসাবে।
--সীমা-চেক
অ্যারে বাউন্ড চেক সক্ষম করুন
--div-বাই-জিরো-চেক
শূন্য চেক দ্বারা বিভাজন সক্ষম করুন
--পয়েন্টার-চেক
পয়েন্টার চেক সক্রিয় করুন
--স্বাক্ষরিত-ওভারফ্লো-চেক
স্বাক্ষরিত পূর্ণসংখ্যা পাটিগণিতের জন্য গাণিতিক ওভার- এবং আন্ডারফ্লো চেক সক্ষম করুন
--স্বাক্ষরবিহীন-ওভারফ্লো-চেক
স্বাক্ষরবিহীন পূর্ণসংখ্যা পাটিগণিতের জন্য গাণিতিক ওভার- এবং আন্ডারফ্লো চেক সক্ষম করুন
--নান-চেক
NaN-এর জন্য ফ্লোটিং-পয়েন্ট কম্পিউটেশন পরীক্ষা করুন
--কোনো-জক্তি
ব্যবহারকারীর দেওয়া বক্তব্য উপেক্ষা করুন
--না-অনুমান
ব্যবহারকারী-প্রদত্ত অনুমান উপেক্ষা করুন
--ত্রুটি-লেবেল লেবেল
প্রদত্ত লেবেলটি নাগালযোগ্য কিনা তা পরীক্ষা করুন
প্রোগ্রাম ইন্সট্রুমেন্টেশন বিকল্প (গোটো-যন্ত্র কেবল)
goto-যন্ত্র আরও, আরও জটিল, প্রোগ্রাম রূপান্তর সমর্থন করে।
--nondet-অস্থির
অস্থির ভেরিয়েবল থেকে রিড তৈরি করে অ-নির্ধারক
--isr ফাংশন
প্রদত্ত নামের সাথে একটি বিঘ্নিত পরিষেবার রুটিন যন্ত্র
--mmio Instruments মেমরি-ম্যাপ করা I/O
--ননডেট-স্ট্যাটিক
স্ট্যাটিক লাইফটাইম সহ ভেরিয়েবলগুলি অ-নির্ধারিতভাবে শুরু করা হয়
--ডাম্প-গ
গোটো বাইনারির পরিবর্তে ANSI-C সোর্স কোড আউটপুট করুন।
বিএমসি বিকল্প (cbmc)
--সমস্ত-সম্পত্তি
সমস্ত সম্পত্তির অবস্থা রিপোর্ট করুন
--শো-সম্পত্তি
শুধুমাত্র বৈশিষ্ট্য দেখান
-- শো-লুপস
প্রোগ্রামে লুপ দেখান
--কভার-জক্তি
কোন দাবী পৌঁছানো যায় তা পরীক্ষা করুন
--ফাংশনের নাম
প্রধান ফাংশন নাম সেট করুন
--প্রপার্টি আইডি
শুধুমাত্র প্রদত্ত শনাক্তকারীর সাথে নির্দিষ্ট সম্পত্তি চেক করুন
--শুধুমাত্র প্রোগ্রাম
শুধুমাত্র প্রোগ্রাম এক্সপ্রেশন দেখান
-- গভীরতা nr
অনুসন্ধানের গভীরতা সীমিত করুন
--আনওয়াইন্ড nr
লুপ nr বার unwind
--আনউইন্ডসেট এল:বি,...
B এর সীমানা সহ লুপ L আনউইন্ড করুন (লুপ আইডি পেতে --show-loops ব্যবহার করুন)
--শো-ভিসিসি
যাচাইকরণ শর্তাবলী দেখান
-- স্লাইস-সূত্র
সম্পত্তির সাথে সম্পর্কহীন অ্যাসাইনমেন্টগুলি সরান
--নো-আনওয়াইন্ডিং-অ্যাসটারসনস
অপ্রীতিকর দাবী উত্পন্ন করবেন না
--না-সুন্দর-নাম
শনাক্তকারীকে সরলীকরণ করবেন না
পিছনে বিকল্প (cbmc)
--ডিম্যাক্স
বহিরাগত SAT সমাধানকারীদের দ্বারা ব্যবহারের জন্য DIMACS বিন্যাসে CNF তৈরি করুন
--সুন্দর-লোভী
পাল্টা উদাহরণ সুন্দর করুন (লোভী হিউরিস্টিক)
--smt1 SMT1 সিনট্যাক্সে আউটপুট সাবগোলস (পরীক্ষামূলক)
--smt2 SMT2 সিনট্যাক্সে আউটপুট সাবগোলস (পরীক্ষামূলক)
--বুলেক্টর
বুলেক্টর ব্যবহার করুন (পরীক্ষামূলক)
-- mathsat
MathSAT ব্যবহার করুন (পরীক্ষামূলক)
--cvc CVC3 ব্যবহার করুন (পরীক্ষামূলক)
-- হ্যাঁ
Yice ব্যবহার করুন (পরীক্ষামূলক)
--z3 Z3 ব্যবহার করুন (পরীক্ষামূলক)
-- পরিমার্জন
পরিমার্জন পদ্ধতি ব্যবহার করুন (পরীক্ষামূলক)
--আউটফাইল ফাইলের নাম
প্রদত্ত ফাইলে আউটপুট সূত্র
--অ্যারে-উফ-কখনও না
অ্যারেগুলিকে কখনও ব্যাখ্যাহীন ফাংশনে পরিণত করবেন না
--অ্যারে-উফ-সর্বদা
সর্বদা অ্যারেগুলিকে ব্যাখ্যাহীন ফাংশনে পরিণত করুন
পরিবেশ
অস্থায়ী ফাইল তৈরি করার সময় সমস্ত সরঞ্জাম TMPDIR পরিবেশ পরিবর্তনশীলকে সম্মান করে
ডিরেক্টরি আরও নোট করুন যে CBMC দ্বারা ব্যবহৃত প্রিপ্রসেসর পরিবেশ ব্যবহার করবে
হেডার ফাইল সনাক্ত করতে ভেরিয়েবল। GOTO-CC এর লক্ষ্য হল সমস্ত পরিবেশের ভেরিয়েবল গ্রহণ করা
জিসিসি করে।
কপিরাইট
2001-2014, ড্যানিয়েল ক্রোনিং, এডমন্ড ক্লার্ক
onworks.net পরিষেবা ব্যবহার করে goto-cc অনলাইন ব্যবহার করুন
