این دستور goto-cc است که می تواند در ارائه دهنده هاست رایگان OnWorks با استفاده از یکی از چندین ایستگاه کاری آنلاین رایگان ما مانند Ubuntu Online، Fedora Online، شبیه ساز آنلاین ویندوز یا شبیه ساز آنلاین MAC OS اجرا شود.
برنامه:
نام
cbmc - جستجوگر مدل محدود برای برنامه های C/C++ و جاوا
خلاصه
cbmc [--ویژگی شناسه ملک] file.c ...
cbmc [--نمایش خواص] file.c ...
cbmc [--تمام خواص] file.c ...
goto-cc [-من شامل مسیر] [-c] file.c [-یا outfile.o]
goto-instrument پرونده مجموعه
فقط مفیدترین گزینه ها در اینجا فهرست شده اند. برای بقیه موارد زیر را ببینید.
شرح
cbmc ردیابی هایی ایجاد می کند که نشان می دهد چگونه یک ادعا می تواند نقض شود، یا آن را ثابت می کند
این ادعا را نمی توان در تعداد معینی از تکرارهای حلقه نقض کرد. CBMC می تواند بخواند
کد منبع مستقیم یا یک goto-binary تولید شده توسط goto-cc. برنامه های جاوا به عنوان ارائه شده است
فایل های کلاس بدون هیچ گزینه دیگری، cbmc تمام ویژگی ها را بررسی می کند (به طور خودکار
تولید شده یا مشخص شده توسط کاربر) در برنامه یافت می شود. اگر هر یک از خواص می تواند باشد
نقض می شود، یک مثال متقابل چاپ می شود و تجزیه و تحلیل لغو می شود. تحلیل می تواند باشد
محدود به یک ویژگی خاص با گزینه --property. نتیجه تایید
برای همه خواص را می توان با استفاده از گزینه --all-properties به دست آورد.
goto-cc کد منبع را می خواند و یک goto-binary ایجاد می کند. رابط خط فرمان آن است
طراحی شده برای تقلید از gcc(1). به ویژه توجه داشته باشید که goto-cc بین
کامپایل و پیوند دادن فازها، درست مانند gcc. cbmc انتظار یک goto-binary برای آن دارد
پیوند کامل شده است.
goto-instrument یک goto-binary را می خواند، یک تبدیل برنامه داده شده را انجام می دهد و سپس
برنامه حاصل را به صورت goto-binary روی دیسک می نویسد.
جریان معمول این است که (1) منبع را با استفاده از goto-cc به یک goto-binary ترجمه کنید، سپس (2)
ابزار دقیق را با goto-instrument انجام دهید و در نهایت (3) تجزیه و تحلیل را با
cbmc.
OPTIONS
ظاهر OPTIONS (cbmc و goto-cc)
-من مسیر
مجموعه مسیر شامل (C/C++)
-D ماکرو
تعریف ماکرو پیش پردازنده (C/C++)
--پیش پردازش
پس از پیش پردازش متوقف شود
--نمایش-نماد-جدول
نمایش جدول نمادها
--show-goto-functions
نمایش برنامه goto
معماری OPTIONS (cbmc و goto-cc)
cbmc به طور پیش فرض از تنظیمات معماری مطابق با تنظیمات دستگاه استفاده می کند cbmc is
اجرا شده در، به عنوان مثال، تنظیمات زیر فقط در هنگام تأیید نرم افزار مورد نیاز است
به معنای اجرا بر روی یک معماری یا سیستم عامل متفاوت است. goto-cc یک goto-binary برای a ایجاد می کند
معماری خاص، به عنوان مثال، معماری را نمی توان بعد از رفتن به دودویی تغییر داد
تولید شده
--16، --32، --64
تنظیم عرض int
--LP64، --ILP64، --LLP64، --ILP32، --LP32
عرض int، long و اشاره گر را تنظیم کنید
--کوچک اندیان
به تبدیل کلمه بایتی اندک اندکی اجازه دهید
--بزرگ اندیان
به تبدیل کلمه بایتی با حجم بزرگ اجازه دهید
---unsigned-char
به طور پیش فرض "char" را بدون علامت بگذارید
--arch معماری هدف را تنظیم کنید
--os سیستم عامل هدف را تنظیم کنید
-- بدون قوس
یک معماری راه اندازی نکنید
--بدون کتابخانه
کتابخانه انتزاعی C داخلی را غیرفعال کنید
-- دور به نزدیکترین، -- دور به مثبت-inf، -- دور به منهای-inf، -- دور به صفر
حالت گرد کردن ممیز شناور IEEE برای استفاده در هنگام شروع برنامه (پیش فرض گرد است
به نزدیکترین). برنامه تحت تأیید می تواند این تنظیم را لغو کند، به عنوان مثال، با
فسترون(3).
برنامه سنجش OPTIONS (cbmc و ابزار goto)
هر دو cbmc و goto-instrument می تواند ادعاهایی ایجاد کند که خطاهای رایج خاص را دریافت کند،
همانطور که در زیر ذکر شد.
--حدود-بررسی
بررسی محدوده آرایه را فعال کنید
--div-by-zero-check
تقسیم بر صفر چک ها را فعال کنید
-- اشاره گر-بررسی
بررسی های اشاره گر را فعال کنید
---امضا-سرریز-بررسی
بررسی های حسابی بیش از حد و زیر جریان را برای محاسبات عدد صحیح امضا شده فعال کنید
--بدون علامت-سرریز-بررسی
بررسی های حسابی بیش از حد و زیر جریان را برای محاسبات اعداد صحیح بدون علامت فعال کنید
-- نان چک
محاسبات ممیز شناور را برای NaN بررسی کنید
-- بدون ادعا
اظهارات ارائه شده توسط کاربر را نادیده بگیرید
--بدون فرضیات
مفروضات ارائه شده توسط کاربر را نادیده بگیرید
-- برچسب خطا
بررسی کنید که برچسب داده شده غیرقابل دسترسی باشد
برنامه سنجش OPTIONS (برو-ساز تنها)
goto-instrument از تغییرات برنامه های پیچیده تر و بیشتر پشتیبانی می کند.
-- غیر دات فرار
خواندن از متغیرهای فرار را غیر قطعی می کند
تابع --isr
یک روال سرویس وقفه را با نام داده شده ابزار می کند
--mmio Instruments با حافظه نگاشت ورودی/خروجی
- غیردید-استاتیک
متغیرهای با طول عمر ثابت به صورت غیر قطعی مقداردهی اولیه می شوند
-- dump-c
خروجی کد منبع ANSI-C به جای یک Goto باینری.
BMC OPTIONS (cbmc)
--تمام خواص
گزارش وضعیت تمام املاک
--نمایش خواص
فقط خصوصیات را نشان دهید
---حلقه ها
حلقه های موجود در برنامه را نشان دهید
--پوشش اظهارات
بررسی کنید که کدام ادعاها قابل دسترسی هستند
- نام تابع
نام تابع اصلی را تنظیم کنید
-- شناسه ملک
فقط دارایی خاص را با شناسه داده شده بررسی کنید
--فقط برنامه
فقط بیان برنامه را نشان دهید
-- عمق شماره
عمق جستجو را محدود کنید
-- unwind nr
باز کردن حلقه ها تعداد دفعات
-- باز کردن چرخش L:B،...
حلقه L را با کران B باز کنید (از --show-loops برای بدست آوردن شناسه های حلقه استفاده کنید)
--show-vcc
شرایط تأیید را نشان دهید
--فرمول برش
تکالیف غیر مرتبط با اموال را حذف کنید
--بدون بازگشایی-اظهار
ادعاهای ناپایدار ایجاد نکنید
--بدون نام های زیبا
شناسه ها را ساده نکنید
پس زمینه OPTIONS (cbmc)
--dimacs
CNF را در قالب DIMACS برای استفاده توسط حل کننده های SAT خارجی تولید کنید
--زیبا کردن-حریص
مثال متقابل را زیبا کنید (اکتشافی حریصانه)
--smt1 اهداف فرعی خروجی در نحو SMT1 (تجربی)
--smt2 اهداف فرعی خروجی در نحو SMT2 (تجربی)
--بولکتور
استفاده از Boolector (تجربی)
-- mathsat
استفاده از MathSAT (تجربی)
--cvc استفاده از CVC3 (تجربی)
-- ییس
استفاده از Yices (تجربی)
--z3 استفاده از Z3 (تجربی)
--پالودن
استفاده از روش پالایش (تجربی)
--نام فایل outfile
فرمول خروجی به فایل داده شده
--آرایه ها-اف-هرگز
هرگز آرایه ها را به توابع تفسیر نشده تبدیل نکنید
--آرایه ها-اف-همیشه
همیشه آرایه ها را به توابع تفسیر نشده تبدیل کنید
محیط زیست
همه ابزارها متغیر محیطی TMPDIR را هنگام تولید فایل های موقت و
دایرکتوری ها علاوه بر این توجه داشته باشید که پیش پردازنده مورد استفاده توسط CBMC از محیط استفاده می کند
متغیرهایی برای مکان یابی فایل های هدر هدف GOTO-CC پذیرش تمام متغیرهای محیطی است
GCC انجام می دهد.
کپی رایت
2001-2014، دانیل کرونینگ، ادموند کلارک
با استفاده از خدمات onworks.net از goto-cc به صورت آنلاین استفاده کنید
