هذا هو الأمر goto-cc الذي يمكن تشغيله في مزود الاستضافة المجانية OnWorks باستخدام إحدى محطات العمل المجانية المتعددة على الإنترنت مثل Ubuntu Online أو Fedora Online أو محاكي Windows عبر الإنترنت أو محاكي MAC OS عبر الإنترنت
برنامج:
اسم
cbmc - مدقق نموذج مقيد لبرامج C / C ++ و Java
موجز
com.cbmc [--ملكية معرف الملكية] ملف
com.cbmc [- إظهار الخصائص] ملف
com.cbmc [- جميع الخصائص] ملف
الانتقال إلى نسخة [-أنا تضمين المسار] [-ج] ملف [-أو outfile.o]
غوتو-صك شرير ملف
يتم سرد الخيارات الأكثر فائدة فقط هنا ؛ انظر أدناه للباقي.
الوصف
com.cbmc يولد آثارًا توضح كيف يمكن انتهاك تأكيد ما ، أو يثبت ذلك
لا يمكن انتهاك التأكيد ضمن عدد معين من تكرار الحلقة. يمكن قراءة CBMC
شفرة المصدر مباشرة ، أو الانتقال الثنائي الذي تم إنشاؤه بواسطة goto-cc. يتم إعطاء برامج Java كـ
ملفات الصف. بدون أي خيارات أخرى ، يتحقق cbmc من جميع الخصائص (تلقائيًا
تم إنشاؤه أو تحديده بواسطة المستخدم) الموجود في البرنامج. إذا كان أي من الخصائص يمكن أن يكون
تم انتهاكه ، تتم طباعة نموذج مضاد وإلغاء التحليل. يمكن أن يكون التحليل
يقتصر على خاصية معينة باستخدام الخيار --property. نتيجة التحقق
يمكن الحصول على جميع الخصائص عن طريق خيار - all-properties.
الانتقال إلى نسخة يقرأ التعليمات البرمجية المصدر ، وينشئ ملفًا ثنائيًا. واجهة سطر الأوامر الخاصة به هي
مصممة لتقليد ذلك من دول مجلس التعاون الخليجي(1). لاحظ على وجه الخصوص أن الانتقال إلى نسخة يميز بين
مراحل التجميع والربط ، تمامًا كما تفعل دول مجلس التعاون الخليجي. com.cbmc يتوقع ثنائياً من أجله
اكتمل الربط.
غوتو-صك يقرأ geto-binary ، ويقوم بتحويل برنامج معين ، ثم
يكتب البرنامج الناتج كـ goto-binary على القرص.
التدفق المعتاد هو (1) ترجمة المصدر إلى ثنائي الانتقال باستخدام goto-cc ، ثم (2)
أداء الأجهزة باستخدام أداة goto ، وأخيراً (3) إجراء التحليل باستخدام
com.cbmc.
OPTIONS
الواجهة OPTIONS (كبمك و الانتقال إلى نسخة)
-أنا المسار
مجموعة تشمل المسار (C / C ++)
-د الماكرو
تحديد ماكرو المعالج المسبق (C / C ++)
--العملية
توقف بعد المعالجة المسبقة
- عرض رمز الجدول
إظهار جدول الرموز
- إظهار الوظائف
عرض برنامج goto
المعماري OPTIONS (كبمك و الانتقال إلى نسخة)
com.cbmc يستخدم افتراضيًا إعدادات معمارية تتطابق مع إعدادات الجهاز com.cbmc is
المنفذة ، على سبيل المثال ، الإعدادات أدناه مطلوبة فقط عند التحقق من البرنامج
يُقصد به أن يعمل على بنية أو نظام تشغيل مختلف. الانتقال إلى نسخة يولد الانتقال الثنائي لـ a
معمارية معينة ، أي لا يمكن تغيير البنية بعد أن يكون goto-binary
ولدت.
--16 ، --32 ، --64
تعيين عرض int
--LP64 ، --ILP64 ، --LLP64 ، --ILP32 ، --LP32
تعيين عرض مؤشرات int و long و
- ليتل إنديان
السماح بتحويلات كلمات بايت صغيرة
--endian كبيرة
السماح بتحويلات الكلمات ذات الحجم الكبير
- حرف غير موقّع
اجعل "char" بدون توقيع افتراضيًا
--أرش تعيين العمارة المستهدفة
--os تعيين نظام التشغيل الهدف
--لا قوس
لا تقم بإعداد بنية
--لا مكتبة
تعطيل مكتبة C التجريدية المضمنة
- تقريبًا إلى أقرب ، - تقريبًا إلى زائد - inf ، - تقريبًا إلى ناقص - inf ، - تقريبًا إلى الصفر
وضع تقريب الفاصلة العائمة IEEE لاستخدامه عند بدء البرنامج (الافتراضي مستدير
إلى أقرب). يمكن للبرنامج قيد التحقق تجاوز هذا الإعداد ، على سبيل المثال ، مع
com.fesetround(3).
PROGRAM INSTRUMENTATION OPTIONS (كبمك و غوتو-صك)
يبلغ قطر كلاً من com.cbmc و غوتو-صك يمكن أن تولد تأكيدات تكتشف أخطاء شائعة محددة ،
كما هو موضح أدناه.
- فحص الحدود
تفعيل عمليات التحقق من حدود الصفيف
- تحقق من تقسيم على صفر
تمكين القسمة على صفر الشيكات
- فحص المؤشر
تمكين تدقيق المؤشر
- تحقق من تجاوز السعة
قم بتمكين عمليات التحقق الحسابية من تجاوز وتحت التدفق لحساب الأعداد الصحيحة الموقعة
- فحص تجاوز السعة غير الموقعة
قم بتمكين عمليات التحقق الحسابية من تجاوز وتحت التدفق لحساب عدد صحيح بدون إشارة
--نان الاختيار
تحقق من حسابات الفاصلة العائمة لـ NaN
--لا تأكيدات
تجاهل التأكيدات المقدمة من المستخدم
- لا افتراضات
تجاهل الافتراضات المقدمة من المستخدم
- تسمية خطأ
تحقق من أن الملصق المحدد لا يمكن الوصول إليه
PROGRAM INSTRUMENTATION OPTIONS (غوتو-صك فقط)
غوتو-صك يدعم عمليات تحويل البرامج الأكثر تعقيدًا.
- نونديت متقلبة
يجعل القراءة من المتغيرات المتقلبة غير حتمية
- وظيفة مصر
أدوات روتين خدمة المقاطعة بالاسم المحدد
- أجهزة mmio المعينة الذاكرة I / O
- نونديت ثابت
تتم تهيئة المتغيرات ذات العمر الثابت بشكل غير حتمي
- تفريغ ج
إخراج الكود المصدري ANSI-C بدلاً من الانتقال الثنائي.
BMC OPTIONS (كبمك)
--جميع الخصائص
تقرير حالة جميع الخصائص
- إظهار الخصائص
إظهار الخصائص فقط
- حلقات العرض
اعرض الحلقات في البرنامج
- تأكيدات الغلاف
تحقق من التأكيدات التي يمكن الوصول إليها
--اسم وظيفة
تعيين اسم الوظيفة الرئيسية
- معرف الملكية
تحقق فقط من خاصية معينة باستخدام المعرف المحدد
- برنامج فقط
إظهار تعبير البرنامج فقط
--العمق nr
تحديد عمق البحث
- الاسترخاء nr
استرخاء الحلقات عدد مرات
- وضعية الغروب L: B ، ...
قم بفك الحلقة L بحدود B (استخدم حلقات العرض للحصول على معرفات الحلقة)
--عرض- vcc
اعرض شروط التحقق
- صيغة شريحة
قم بإزالة التخصيصات التي لا علاقة لها بالملكية
- تأكيدات عدم التراجع
لا تولد تأكيدات حل
--لا أسماء جميلة
لا تبسط المعرفات
الخلفية OPTIONS (كبمك)
- ديماكس
قم بإنشاء CNF بتنسيق DIMACS للاستخدام بواسطة محاليل SAT الخارجية
- تجميل - الجشع
تجميل المضاد (الاستدلال الجشع)
- أهداف فرعية للإخراج SMT1 في بناء جملة SMT1 (تجريبي)
- أهداف فرعية للإخراج SMT2 في بناء جملة SMT2 (تجريبي)
- منطوق
استخدام بوليكتور (تجريبي)
--mathsat
استخدام MathSAT (تجريبي)
--cvc استخدم CVC3 (تجريبي)
- نعم
استخدم Yices (تجريبي)
--z3 استخدم Z3 (تجريبي)
--صقل
استخدام إجراء الصقل (تجريبي)
--اسم الملف الخارجي
صيغة الإخراج لملف معين
- arrays-uf-never
لا تقم أبدًا بتحويل المصفوفات إلى وظائف غير مفسرة
- المصفوفات - دائما
قم دائمًا بتحويل المصفوفات إلى وظائف غير مفسرة
البيئة
تحترم جميع الأدوات متغير البيئة TMPDIR عند إنشاء ملفات مؤقتة وملفات
الدلائل. علاوة على ذلك ، لاحظ أن المعالج الذي يستخدمه CBMC سيستخدم البيئة
متغيرات لتحديد موقع ملفات الرأس. يهدف GOTO-CC إلى قبول جميع متغيرات البيئة
دول مجلس التعاون الخليجي يفعل.
حقوق الطبع والنشر
2001-2014 ، دانيال كرونينغ ، إدموند كلارك
استخدم goto-cc عبر الإنترنت باستخدام خدمات onworks.net
