זוהי הפקודה goto-cc שניתן להריץ בספק האירוח החינמי של OnWorks באמצעות אחת מתחנות העבודה המקוונות המרובות שלנו, כגון Ubuntu Online, Fedora Online, אמולטור מקוון של Windows או אמולטור מקוון של MAC OS
תָכְנִית:
שֵׁם
cbmc - בודק מודלים מוגבל עבור תוכניות C/C++ ו-Java
תַקצִיר
cbmc [--תכונה מזהה נכס] file.c ...
cbmc [--הצג-מאפיינים] file.c ...
cbmc [--כל המאפיינים] file.c ...
goto-cc [-אני כולל-נתיב] [-c] file.c [-אוֹ outfile.o]
goto-מכשיר בקובץ אוסף
רק האפשרויות השימושיות ביותר מפורטות כאן; ראה להלן לגבי השאר.
תיאור
cbmc מייצר עקבות המדגימים כיצד ניתן להפר טענה, או מוכיח זאת
לא ניתן להפר את הקביעה בתוך מספר נתון של איטרציות לולאה. CBMC יכול לקרוא
קוד מקור ישירות, או goto-binary שנוצר על ידי goto-cc. תוכניות Java ניתנות כ
קבצי כיתה. ללא אפשרויות נוספות, cbmc בודק את כל המאפיינים (באופן אוטומטי
שנוצר או שצוין על ידי המשתמש) נמצא בתוכנית. אם כל אחד מהנכסים יכול להיות
הופר, מודפסת דוגמה נגדית והניתוח מבוטל. הניתוח יכול להיות
מוגבל לנכס מסוים עם אפשרות --property. תוצאת האימות
עבור כל הנכסים ניתן להשיג באמצעות האפשרות --all-properties.
goto-cc קורא קוד מקור, ומייצר goto-binary. ממשק שורת הפקודה שלו הוא
נועד לחקות את זה של gcc(1). שימו לב במיוחד לכך goto-cc מבדיל בין
קומפילציה וקישור שלבים, בדיוק כפי שעושה gcc. cbmc מצפה לגוטו-בינארי שעבורו
הקישור הושלם.
goto-מכשיר קורא גוטו-בינארי, מבצע טרנספורמציה נתונה של תוכנית, ולאחר מכן
כותב את התוכנית המתקבלת כגוטו-בינארי בדיסק.
הזרימה הרגילה היא (1) לתרגם מקור לגוטו-בינארי באמצעות goto-cc, ואז (2)
לבצע מכשור עם goto-instrument, ולבסוף (3) לבצע את הניתוח עם
cbmc.
אפשרויות
חזיתי אפשרויות (cbmc ו goto-cc)
-אני נתיב
הגדר נתיב כולל (C/C++)
-D מאקרו
הגדר מאקרו קדם-מעבד (C/C++)
-- תהליך מקדים
עצור לאחר עיבוד מקדים
--הצג-סמל-טבלה
הצג טבלת סמלים
--הצג-גוטו-פונקציות
הצג תוכנית goto
ארכיטקטורה אפשרויות (cbmc ו goto-cc)
cbmc כברירת מחדל משתמש בהגדרות ארכיטקטוניות התואמות לאלו של המכשיר cbmc is
מופעל על, כלומר, ההגדרות שלהלן נחוצות רק בעת אימות תוכנה כלומר
נועד לפעול על ארכיטקטורה או מערכת הפעלה אחרת. goto-cc יוצר גוטו-בינארי עבור a
ארכיטקטורה מסוימת, כלומר, לא ניתן לשנות את הארכיטקטורה לאחר שה-goto-binary is
נוצר.
--16, --32, --64
הגדר רוחב של int
--LP64, --ILP64, --LLP64, --ILP32, --LP32
הגדר רוחב של int, ארוך ומצביעים
---little-endian
אפשר המרות מילה-בתים של מילה קטנה
--ביג-אנדיאן
אפשר המרות מילה-בתים של מילה גדולה
--לא חתום-char
הפוך את "char" ללא חתימה כברירת מחדל
--arch הגדר ארכיטקטורת יעד
--os הגדר מערכת הפעלה יעד
--ללא קשת
אל תגדיר ארכיטקטורה
--ללא ספרייה
השבת את ספריית התקציר C המובנית
--עגול לקרוב, --עגול-לפלוס-אינף, --עגול-למינוס-אינף, --עגול-לאפס
מצב עיגול נקודה צפה IEEE לשימוש כאשר התוכנית מתחילה (ברירת המחדל היא עגולה
הקרוב ביותר). התוכנית באימות יכולה לעקוף הגדרה זו, למשל, עם
מסביב(3).
תָכְנִית מִכשׁוּר אפשרויות (cbmc ו goto-מכשיר)
שניהם cbmc ו goto-מכשיר יכול ליצור הצהרות שתופסות שגיאות נפוצות ספציפיות,
כמפורט להלן.
--בדיקת גבולות
אפשר בדיקות גבולות מערך
-- בדיקת חלוקה לאפס
אפשר חלוקה לפי אפס המחאות
---pointer-check
אפשר בדיקות מצביעים
--בדיקת הצפת חתימה
אפשר בדיקות יתר וחסר אריתמטיות עבור אריתמטיקה של מספר שלם בסימן
--בדיקת הצפת ללא חתימה
אפשר בדיקות יתר וחסר אריתמטיות עבור אריתמטיקה של מספר שלם ללא סימן
--נאן-צ'ק
בדוק חישובי נקודה צפה עבור NaN
--ללא הצהרות
התעלם מהצהרות שסופקו על ידי המשתמש
--ללא הנחות
התעלם מהנחות שסופקו על ידי המשתמש
--תווית שגיאה
בדוק שלא ניתן להגיע לתווית הנתונה
תָכְנִית מִכשׁוּר אפשרויות (גוטו-מכשיר בלבד)
goto-מכשיר תומך בטרנספורמציות נוספות ומורכבות יותר של תוכנית.
--nondet-נדיף
מבצע קריאות ממשתנים נדיפים לא דטרמיניסטיים
פונקציית --isr
מכשיר שגרת שירות להפסיק עם השם הפרטי
--mmio Instruments קלט/פלט ממופה זיכרון
--nondet-static
משתנים בעלי אורך חיים סטטי מאותחלים באופן לא דטרמיניסטי
--dump-c
פלט קוד מקור ANSI-C במקום בינארי goto.
BMC אפשרויות (cbmc)
--כל הנכסים
דווח על מצב כל הנכסים
--הצג-מאפיינים
הצג רק מאפיינים
---show-loops
הצג את הלולאות בתוכנית
--קביעות-כריכה
בדוק לאילו קביעות ניתן להגיע
--שם פונקציה
הגדר את שם הפונקציה הראשית
- מזהה נכס
בדוק רק נכס ספציפי עם מזהה נתון
--לתוכנית בלבד
הצג רק ביטוי תוכנית
--עומק מס'
הגבל את עומק החיפוש
- להירגע מס'
שחרר לולאות מס' פעמים
--לא רוחב L:B,...
שחרר לולאה L עם הגבול של B (השתמש ב--show-loops כדי לקבל את מזהי הלולאה)
--show-vcc
הצג את תנאי האימות
--נוסחה-פרוסה
הסר מטלות שאינן קשורות לנכס
--לא-להתיר-הצהרות
אל תייצר הצהרות מתפתלות
--אין-שמות-יפים
אל תפשט מזהים
גב אפשרויות (cbmc)
--dimacs
צור CNF בפורמט DIMACS לשימוש על ידי פותרי SAT חיצוניים
--לייפות-חמדן
לייפות את הדוגמה הנגדית (היוריסטיקה חמדנית)
--smt1 יעדי פלט בתחביר SMT1 (ניסיוני)
--smt2 יעדי פלט בתחביר SMT2 (ניסיוני)
--בולקטור
השתמש ב-Boolector (ניסיוני)
--מתמטיקה
השתמש ב- MathSAT (ניסיוני)
--cvc השתמש ב-CVC3 (ניסיוני)
-- כן
השתמש ב-Yices (ניסיוני)
--z3 השתמש ב-Z3 (ניסיוני)
--לעדן
השתמש בהליך חידוד (ניסיוני)
--שם קובץ outfile
פלט נוסחה לקובץ נתון
---arrays-uf-never
לעולם אל תהפוך מערכים לפונקציות ללא פירוש
---arrays-uf-always
הפוך תמיד מערכים לפונקציות לא מפורשות
הסביבה
כל הכלים מכבדים את משתנה הסביבה TMPDIR בעת יצירת קבצים זמניים ו
ספריות. יתר על כן, שים לב שהמעבד המקדים בשימוש CBMC ישתמש בסביבה
משתנים לאיתור קבצי כותרת. GOTO-CC שואפת לקבל את כל משתני הסביבה
GCC כן.
זכויות יוצרים
2001-2014, דניאל קרונינג, אדמונד קלארק
השתמש ב-goto-cc באינטרנט באמצעות שירותי onworks.net
