goto-cc - Online di Cloud

PROGRAM:

NAMA

cbmc - Pemeriksa Model Terikat untuk program C/C++ dan Java

RINGKASAN

cbmc [--Properti ID-properti] file.c ...

cbmc [--show-properti] file.c ...

cbmc [--semua-properti] file.c ...

goto-cc [-SAYA termasuk-jalur] [-C] file.c [-atau file keluar.o]

goto-instrumen masuk file keluar

Hanya opsi yang paling berguna yang tercantum di sini; lihat di bawah untuk sisanya.

DESKRIPSI

cbmc menghasilkan jejak yang menunjukkan bagaimana pernyataan dapat dilanggar, atau membuktikan bahwa
pernyataan tidak dapat dilanggar dalam sejumlah iterasi loop tertentu. CBMC bisa membaca
source-code secara langsung, atau goto-binary yang dihasilkan oleh goto-cc. Program Java diberikan sebagai
file kelas. Tanpa opsi lebih lanjut, cbmc memeriksa semua properti (secara otomatis
dihasilkan atau ditentukan pengguna) yang ditemukan dalam program. Jika salah satu properti dapat menjadi
dilanggar, contoh tandingan dicetak dan analisis dibatalkan. Analisisnya bisa berupa
terbatas pada properti tertentu dengan opsi --properti. Hasil verifikasi
untuk semua properti dapat diperoleh melalui opsi --all-properties.

goto-cc membaca kode sumber, dan menghasilkan goto-biner. Antarmuka baris perintahnya adalah
dirancang untuk meniru itu dari gcc(1). Perhatikan secara khusus bahwa goto-cc membedakan antara
fase kompilasi dan penautan, seperti halnya gcc. cbmc mengharapkan goto-binary yang
penyambungan telah selesai.

goto-instrumen membaca biner-goto, melakukan transformasi program yang diberikan, dan kemudian
menulis program yang dihasilkan sebagai goto-biner pada disk.

Alur yang biasa adalah (1) menerjemahkan sumber menjadi biner-goto menggunakan goto-cc, lalu (2)
melakukan instrumentasi dengan goto-instrument, dan akhirnya (3) melakukan analisis dengan
cbmc.

PILIHAN

Frontend PILIHAN (cbmc dan goto-cc)
-Aku jalan
Tetapkan sertakan jalur (C/C++)

-D makro
Tentukan makro praprosesor (C/C++)

--praproses
Berhenti setelah pra-pemrosesan

--tampilkan-simbol-tabel
Tampilkan tabel simbol

--show-goto-fungsi
Tampilkan program goto

ARSITEKTUR PILIHAN (cbmc dan goto-cc)
cbmc secara default menggunakan pengaturan arsitektur yang cocok dengan mesin cbmc is
dijalankan pada, yaitu, pengaturan di bawah ini hanya diperlukan saat memverifikasi perangkat lunak yang
dimaksudkan untuk berjalan pada arsitektur atau OS yang berbeda. goto-cc menghasilkan goto-biner untuk a
arsitektur tertentu, yaitu, arsitektur tidak dapat diubah setelah goto-binary adalah
dihasilkan.

---16, --32, --64
Setel lebar int

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Atur lebar int, panjang dan pointer

--little-endian
Izinkan konversi bita kata little-endian

--big-endian
Izinkan konversi byte kata big-endian

--unsigned-char
Buat "char" tidak ditandatangani secara default

--arch Tetapkan arsitektur target

--os Tetapkan sistem operasi target

--tidak ada lengkungan
Jangan mengatur arsitektur

--tidak ada perpustakaan
Nonaktifkan pustaka C abstrak bawaan

--round-to-terdekat, --round-to-plus-inf, --round-to-minus-inf, --round-to-zero
Mode pembulatan titik mengambang IEEE untuk digunakan saat program dimulai (standarnya bulat
ke terdekat). Program yang sedang diverifikasi dapat mengesampingkan pengaturan ini, misalnya dengan
putaran feset(3).

PROGRAM PERALATAN PILIHAN (cbmc dan goto-instrumen)
Kedua cbmc dan goto-instrumen dapat menghasilkan pernyataan yang menangkap kesalahan umum tertentu,
seperti tercantum di bawah ini.

--bounds-periksa
Aktifkan pemeriksaan batas array

--div-by-zero-check
Aktifkan pembagian dengan nol cek

--penunjuk-cek
Aktifkan pemeriksaan penunjuk

--ditandatangani-overflow-cek
Aktifkan pemeriksaan over- dan underflow aritmatika untuk aritmatika bilangan bulat yang ditandatangani

--unsigned-overflow-cek
Aktifkan pemeriksaan over- dan underflow aritmatika untuk aritmatika bilangan bulat yang tidak ditandatangani

--nan-cek
Periksa perhitungan floating-point untuk NaN

--tidak ada pernyataan
Abaikan pernyataan yang diberikan pengguna

--tanpa asumsi
Abaikan asumsi yang diberikan pengguna

--label label-kesalahan
Periksa apakah label yang diberikan tidak dapat dijangkau

PROGRAM PERALATAN PILIHAN (goto-instrumen saja)
goto-instrumen mendukung lebih lanjut, lebih kompleks, transformasi program.

--nondet-volatil
Membuat pembacaan dari variabel volatil non-deterministik

--fungsi isr
Instrumen rutin layanan interupsi dengan nama yang diberikan

--mmio Instrumen I/O yang dipetakan dengan memori

--nondet-statis
Variabel dengan masa hidup statis diinisialisasi secara non-deterministik

--buang-c
Keluarkan kode sumber ANSI-C alih-alih biner goto.

BMC PILIHAN (cbmc)
--semua-properti
Laporkan status semua properti

--show-properti
Hanya tampilkan properti

--show-loop
Tampilkan loop dalam program

--penutup-pernyataan
Periksa pernyataan mana yang dapat dijangkau

--nama fungsi
Tetapkan nama fungsi utama

--id properti
Hanya periksa properti tertentu dengan pengenal yang diberikan

--hanya program
Hanya tampilkan ekspresi program

--kedalaman nr
Batasi kedalaman pencarian

--bersantai nr
Bersantai loop nr kali

--lepas angin L:B,...
Lepaskan loop L dengan batas B (gunakan --show-loop untuk mendapatkan ID loop)

--tunjukkan-vcc
Tunjukkan kondisi verifikasi

--rumus irisan
Hapus tugas yang tidak terkait dengan properti

--no-unwinding-pernyataan
Jangan menghasilkan pernyataan yang tidak menarik

--tanpa-nama-cantik
Jangan sederhanakan pengidentifikasi

BELAKANG PILIHAN (cbmc)
--dimac
Hasilkan CNF dalam format DIMACS untuk digunakan oleh pemecah SAT eksternal

--mempercantik-serakah
Mempercantik contoh tandingan (heuristik serakah)

--smt1 Output subtujuan dalam sintaks SMT1 (eksperimental)

--smt2 Output subtujuan dalam sintaks SMT2 (eksperimental)

--boolektor
Gunakan Boolector (eksperimental)

--matsat
Gunakan MathSAT (eksperimental)

--cvc Gunakan CVC3 (eksperimental)

--ya
Gunakan Yices (eksperimental)

--z3 Gunakan Z3 (eksperimental)

--menyaring
Gunakan prosedur penyempurnaan (eksperimental)

--outfile nama file
Rumus keluaran ke file yang diberikan

--array-uf-tidak pernah
Jangan pernah mengubah array menjadi fungsi yang tidak diinterpretasikan

--arrays-uf-selalu
Selalu ubah array menjadi fungsi yang tidak ditafsirkan

LINGKUNGAN

Semua alat menghormati variabel lingkungan TMPDIR saat membuat file sementara dan
direktori. Selanjutnya perhatikan bahwa preprocessor yang digunakan oleh CBMC akan menggunakan environment
variabel untuk mencari file header. GOTO-CC bertujuan untuk menerima semua variabel lingkungan yang
GCC melakukannya.

HAK CIPTA

2001-2014, Daniel Kroening, Edmund Clarke

Gunakan goto-cc online menggunakan layanan onworks.net