cpachecker

Memulai dengan cpachecker

• Instruksi Instalasi
• Pedoman Kontribusi
• Instruksi pengembangan

Lebih banyak dokumentasi dapat ditemukan di doc/ Direktori.

Lisensi dan Hak Cipta

CPachecker dilisensikan di bawah lisensi Apache 2.0 dengan hak cipta oleh Dirk Beyer dan lainnya (lih. Penulis.MD untuk daftar lengkap semua kontributor). Perpustakaan pihak ketiga berada di bawah berbagai lisensi dan hak cipta lainnya, lih. File dalam LICENSES direktori untuk teks lisensi lengkap. Secara khusus, MathSat tersedia hanya untuk tujuan penelitian dan evaluasi (lih LICENSES/LicenseRef-MathSAT-CPAchecker.txt ), jadi pastikan untuk menggunakan solver SMT yang berbeda jika perlu. Perhatikan bahwa meskipun program GPL didistribusikan bersama dengan cPachecker, cPachecker terpisah dari program itu dan dengan demikian tidak berdasarkan ketentuan GPL.

Mempersiapkan Program untuk Verifikasi oleh CPachecker

Semua program perlu diproses dengan pra-prosesor C, yaitu, mereka mungkin tidak mengandung arahan #define dan #include . Anda dapat mengaktifkan pra-pemrosesan di dalam cpachecker dengan menentukan --preprocess pada baris perintah. Beberapa file C dapat diberikan dan akan ditautkan bersama dan diverifikasi sebagai program tunggal (fitur eksperimental).

CPachecker dapat mengurai dan menganalisis sebagian besar (GNU) c. Jika parsing gagal untuk program Anda, silakan kirim laporan ke [email protected].

Memverifikasi program dengan cpachecker

1. Pilih file kode sumber yang ingin Anda periksa. Jika Anda menggunakan program Anda sendiri, ingatlah untuk pra-proses seperti yang disebutkan di atas. Contoh: doc/examples/example.c atau doc/examples/example_bug.c Sumber yang baik untuk program yang lebih banyak adalah repositori SV-BenchMarks yang misalnya digunakan oleh kompetisi internasional tentang verifikasi perangkat lunak.

2. Secara opsional: Jika Anda ingin memilih analisis tertentu seperti analisis predikat, tentukan file konfigurasi. File ini mendefinisikan misalnya CPA mana yang digunakan. File konfigurasi standar dapat ditemukan di direktori config/ . Jika Anda tidak menginginkan analisis tertentu, kami merekomendasikan konfigurasi default cPachecker. Namun, perhatikan bahwa jika Anda menggunakan macOS, Anda perlu menyediakan binari MathSat yang dikompilasi secara khusus untuk konfigurasi default agar berfungsi (atau menggunakan Docker untuk menjalankan versi CPACHECKER Linux). Konfigurasi cPachecker dijelaskan di doc/Configuration.md .

3. Pilih file spesifikasi (Anda mungkin tidak memerlukan ini untuk beberapa konfigurasi). Konfigurasi standar menggunakan config/specification/default.spc sebagai spesifikasi default. Dengan yang ini, CPachecker akan mencari label bernama ERROR (case tidak sensitif) dan pernyataan dalam file kode sumber. Contoh lain untuk spesifikasi dapat ditemukan di config/specification/ di direktori cPachecker.

4. Jalankan bin/cpachecker [ --config <CONFIG_FILE> ] [ --spec <SPEC_FILE> ] <SOURCE_FILE> Argumen baris perintah tambahan dijelaskan dalam doc/Configuration.md . Untuk menggunakan konfigurasi default cpachecker, lulus hanya file sumber: bin/cpachecker doc/examples/example.c . Analisis spesifik (seperti induksi K) dapat dipilih misalnya dengan bin/cpachecker --config/kInduction.properties doc/examples/example.c atau singkatan yang setara dengan bin/cpachecker --kInduction doc/examples/example.c . Java 17 atau lebih baru diperlukan. Jika tidak ada di jalur Anda, Anda perlu menentukannya di java variabel lingkungan. Contoh: export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java untuk 64bit openjdk 17 di ubuntu.

   Harap dicatat bahwa tidak semua konfigurasi analisis tersedia untuk macOS karena kami tidak mengirimkan binari untuk pemecah SMT untuk platform ini. Anda perlu membangun binari yang sesuai sendiri atau menggunakan analisis yang kurang kuat yang bekerja dengan pemecah berbasis Java, misalnya yang satu ini alih-alih konfigurasi default CPachecker: --predicateAnalysis-linear --option solver.solver=SMTInterpol Tentu saja Anda juga dapat menggunakan solusi seperti pelaksana untuk melaksanakan versi cpacheck.

   If you installed CPAchecker using Docker, the above example command line would look like this: docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c This command makes the current directory available in the container, so to verify a program in the current directory just provide its file name instead of the example that is bundled with Cpachecker. File output cPachecker akan ditempatkan di ./output/ .

5. Selain itu untuk output konsol, laporan HTML interaktif dihasilkan dalam output/ , baik bernama Report.html (untuk hasil yang benar) atau Counterexample.*.html (untuk hasil FALSE). Buka file -file ini di browser untuk melihat hasil analisis cPachecker (lih. doc/Report.md )

Ada juga file output tambahan di output/ :

• ARG.dot : Visualisasi pohon jangkauan abstrak (format graphviz)
• cfa*.dot : Visualisasi Automaton Aliran Kontrol (Format GraphViz)
• reached.dot : Visualisasi Automaton Aliran Kontrol dengan status abstrak divisualisasikan di atas (Format GraphViz)
• coverage.info : Informasi Cakupan (Mirip dengan alat pengujian) dalam format Gcov Gunakan baris perintah berikut untuk menghasilkan laporan HTML sebagai output/index.html : genhtml output/coverage.info --output-directory output --legend
• Counterexample.*.txt : jalur melalui program yang mengarah ke kesalahan
• Counterexample.*.assignment.txt : penugasan untuk semua variabel pada jalur kesalahan.
• Counterexample.*.harness.c : harness uji yang dapat mereproduksi jalur kesalahan melalui eksekusi tes. Lihat DOC/TUTORIAL/TEST-HARNESS.MD untuk contoh penggunaan.
• predmap.txt : predikat yang digunakan oleh analisis predikat untuk membuktikan keamanan program
• reached.txt : dump dari semua negara abstrak tercapai
• Statistics.txt : Statistik Waktu (juga dapat dicetak ke konsol dengan --stats )

Perhatikan bahwa tidak semua file ini akan tersedia untuk semua konfigurasi. Juga beberapa file ini hanya diproduksi jika kesalahan ditemukan (atau sebaliknya). CPachecker akan menimpa file di direktori ini!

Memvalidasi program dengan CPA-witness2test

Anda dapat memvalidasi pelanggaran saksi dengan CPA-witness2test, yang merupakan bagian dari cpachecker.

1. Untuk melakukannya, Anda memerlukan saksi pelanggaran, file spesifikasi yang sesuai dengan saksi pelanggaran, dan file kode sumber yang sesuai dengan saksi pelanggaran.

2. Untuk memvalidasi saksi, jalankan perintah berikut:

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

   Argumen baris perintah tambahan dilihat dengan bin/cpa-witness2test -h .

3. Setelah selesai, dan jika saksi pelanggaran berhasil divalidasi, output konsol menunjukkan Verification result: FALSE . Selain output konsol, CPA-witness2test juga membuat output/*.harness.c . File ini dapat dikompilasi terhadap file sumber untuk membuat tes yang dapat dieksekusi yang mencerminkan saksi pelanggaran.

Perhatikan bahwa jika saksi pelanggaran tidak berisi informasi yang cukup untuk membuat tes yang dapat dieksekusi, hasil validasi akan menjadi ERROR dan output konsol akan berisi baris berikut: Could not export a test harness, some test-vector values are missing.