cpachecker

البدء مع cpachecker

• تعليمات التثبيت
• إرشادات المساهمة
• تعليمات التنمية

يمكن العثور على المزيد من الوثائق في doc/ Directory.

الترخيص وحقوق الطبع والنشر

تم ترخيص Cpachecker بموجب ترخيص Apache 2.0 مع حقوق الطبع والنشر من قبل Dirk Beyer وغيرها (راجع المؤلفون. MD للحصول على قائمة كاملة بجميع المساهمين). مكتبات الطرف الثالث تخضع مختلف التراخيص وحقوق الطبع والنشر ، راجع الملفات في LICENSES الدليل لنصوص الترخيص الكاملة. على وجه الخصوص ، تتوفر MathSat لأغراض البحث والتقييم فقط (راجع LICENSES/LicenseRef-MathSAT-CPAchecker.txt ) ، لذلك تأكد من استخدام SMT Solver مختلف إذا لزم الأمر. لاحظ أنه على الرغم من توزيع برنامج GPL مع cpachecker ، فإن cpachecker منفصل عن هذا البرنامج وبالتالي ليس بموجب شروط GPL.

إعداد برامج للتحقق من CPACHECKER

تحتاج جميع البرامج إلى معالجتها مسبقًا مع المعالجة المسبقة C ، أي قد لا تحتوي على توجيهات #define و #include . يمكنك تمكين المعالجة المسبقة داخل cpachecker من خلال تحديد --preprocess على سطر الأوامر. يمكن إعطاء ملفات C متعددة وسيتم ربطها معًا والتحقق منها كبرنامج واحد (ميزة تجريبية).

Cpachecker قادر على تحليل وتحليل مجموعة فرعية كبيرة من (GNU) ج. إذا فشل التحليل في برنامجك ، فيرجى إرسال تقرير إلى [email protected].

التحقق من برنامج مع cpachecker

1. اختر ملف رمز المصدر الذي تريد فحصه. إذا كنت تستخدم البرنامج الخاص بك ، تذكر أن تعرضه مسبقًا كما هو مذكور أعلاه. مثال: doc/examples/example.c doc/examples/example_bug.c

2. اختياريا: إذا كنت ترغب في اختيار تحليلات معينة مثل التحليل الأصلي ، فحدد ملف تكوين. يحدد هذا الملف على سبيل المثال أي CPAs المستخدمة. يمكن العثور على ملفات التكوين القياسية في config/ . إذا كنت لا تريد تحليلًا محددًا ، فإننا نوصي بالتكوين الافتراضي لـ Cpachecker. ومع ذلك ، لاحظ أنه إذا كنت على جهاز MacOS ، فأنت بحاجة إلى تقديم ثنائيات MathSat التي يتم تنسيقها على وجه التحديد حتى يعمل التكوين الافتراضي (أو استخدام Docker من أجل تشغيل إصدار Linux من Cpachecker). يتم شرح تكوين cpachecker في doc/Configuration.md .

3. اختر ملف مواصفات (قد لا تحتاج إلى هذا لبعض التكوينات). تستخدم التكوينات القياسية config/specification/default.spc كمواصفات افتراضية. مع هذا واحد ، سيبحث Cpachecker عن ملصقات تسمى ERROR (حالة غير حساسة) والتأكيدات في ملف الكود المصدري. يمكن العثور على أمثلة أخرى للمواصفات في config/specification/ في دليل cpachecker.

4. تنفيذ bin/cpachecker [ --config <CONFIG_FILE> ] [ --spec <SPEC_FILE> ] <SOURCE_FILE> تم وصف وسيطات خط الأوامر الإضافية في doc/Configuration.md . لاستخدام التكوين الافتراضي لـ cpachecker ، تمرير الملف المصدر فقط: bin/cpachecker doc/examples/example.c . يمكن اختيار تحليل محدد (مثل حث K) على سبيل المثال مع bin/cpachecker --config/kInduction.properties doc/examples/example.c أو مكافئ الاختصار bin/cpachecker --kInduction doc/examples/example.c . جافا 17 أو في وقت لاحق ضروري. إذا لم يكن في طريقك ، فأنت بحاجة إلى تحديده في البيئة المتغير Java. مثال: export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java لـ 64bit openjdk 17 على Ubuntu.

   يرجى ملاحظة أنه لا تتوفر جميع تكوينات التحليل لـ MacOS لأننا لا نشحن الثنائيات لحل SMT لهذا النظام الأساسي. تحتاج إما إلى بناء الثنائيات المناسبة بنفسك أو استخدام تحليلات أقل قوة تعمل مع حلال القائمة على Java ، على سبيل المثال هذا واحد بدلاً من التكوين الافتراضي لـ CPACHECKER: --predicateAnalysis-linear --option solver.solver=SMTInterpol بالطبع يمكنك أيضًا استخدام حلول مثل DOCKER لتنفيذ إصدار Linux من CPACHECKER.

   إذا قمت بتثبيت cpachecker باستخدام Docker ، فإن سطر الأوامر مثال أعلاه سيبدو هكذا: docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c cpachecker. سيتم وضع ملفات الإخراج من cpachecker في ./output/ .

5. بالإضافة إلى إخراج وحدة التحكم ، يتم إنشاء تقرير HTML التفاعلي في output/ ، إما باسم Report.html (للنتيجة صواب) أو Counterexample.*.html (للنتيجة خطأ). افتح هذه الملفات في متصفح لعرض نتيجة تحليل cpachecker (راجع doc/Report.md )

هناك أيضًا ملفات إخراج إضافية في output/ :

• ARG.dot : تصور شجرة الوصول التجريدية (تنسيق GraphViz)
• cfa*.dot : تصور تدفق التحكم Automaton (تنسيق GraphViz)
• reached.dot .
• coverage.info : معلومات التغطية (على غرار معلومات أدوات الاختبار) بتنسيق Gcov ، استخدم سطر الأوامر التالي لإنشاء تقرير HTML output/index.html : genhtml output/coverage.info --output-directory output --legend
• Counterexample.*.txt : مسار من خلال البرنامج الذي يؤدي إلى خطأ
• Counterexample.*.assignment.txt
• Counterexample.*.harness.c انظر DOC/TUBLESS/TEST-HARNESS.MD للحصول على مثال.
• predmap.txt : المتوقعات المستخدمة من قبل التحليل المسند لإثبات سلامة البرنامج
• reached.txt
• Statistics.txt : إحصائيات الوقت (يمكن أيضًا طباعتها إلى وحدة التحكم مع --stats )

لاحظ أنه لن تكون كل هذه الملفات متاحة لجميع التكوينات. كما يتم إنتاج بعض هذه الملفات فقط إذا تم العثور على خطأ (أو العكس). سوف cpachecker الكتابة فوق الملفات في هذا الدليل!

التحقق من صحة برنامج مع CPA-Witness2test

يمكنك التحقق من صحة الشهود مع CPA-Witness2test ، وهو جزء من CPachecker.

1. للقيام بذلك ، تحتاج إلى شاهد انتهاك ، ملف مواصفات يناسب شاهد الانتهاك ، وملف قانون المصدر الذي يناسب شاهد الانتهاك.

2. للتحقق من صحة الشاهد ، قم بتنفيذ الأمر التالي:

    bin/cpa-witness2test --witness <WITNESS_FILE> --spec <SPEC_FILE> <SOURCE_FILE>`
   

   يتم عرض وسيطات سطر القيادة الإضافية مع bin/cpa-witness2test -h .

3. عند الانتهاء ، وإذا تم التحقق من صحة شاهد الانتهاك بنجاح ، فإن إخراج وحدة التحكم يظهر Verification result: FALSE . بالإضافة إلى إخراج وحدة التحكم ، يقوم CPA-Witness2test أيضًا بإنشاء ملف output/*.harness.c . يمكن تجميع هذا الملف مقابل الملف المصدر لإنشاء اختبار قابل للتنفيذ يعكس شاهد الانتهاك.

لاحظ أنه إذا لم يكن شاهد الانتهاك لا يحتوي على معلومات كافية لإنشاء اختبار قابل للتنفيذ ، فستكون نتيجة التحقق ERROR وستتضمن إخراج وحدة التحكم السطر التالي: Could not export a test harness, some test-vector values are missing.