goto-cc - Dalam talian di Awan

JADUAL:

NAMA

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

SINOPSIS

cbmc [--harta benda property-id] fail.c ...

cbmc [--show-properties] fail.c ...

cbmc [--semua-sifat] fail.c ...

goto-cc [-Saya masukkan-laluan] [-c] fail.c [-atau fail luar.o]

goto-instrument dalam fail fail luar

Hanya pilihan yang paling berguna disenaraikan di sini; lihat di bawah untuk bakinya.

DESCRIPTION

cbmc menjana kesan yang menunjukkan cara sesuatu dakwaan boleh dilanggar, atau membuktikannya
penegasan tidak boleh dilanggar dalam bilangan lelaran gelung tertentu. CBMC boleh membaca
kod sumber secara langsung, atau perduaan goto yang dihasilkan oleh goto-cc. Program Java diberikan sebagai
fail kelas. Tanpa sebarang pilihan lanjut, cbmc menyemak semua sifat (secara automatik
dijana atau ditentukan pengguna) yang terdapat dalam program. Jika mana-mana sifat boleh
dilanggar, contoh balas dicetak dan analisis dibatalkan. Analisis boleh
terhad kepada harta tertentu dengan pilihan --property. Hasil pengesahan
untuk semua sifat boleh diperolehi melalui pilihan --all-properties.

goto-cc membaca kod sumber, dan menghasilkan goto-binary. Antara muka baris arahannya ialah
direka untuk meniru itu gcc(1). Perhatikan secara khusus bahawa goto-cc membezakan antara
menyusun dan memautkan fasa, sama seperti yang dilakukan oleh gcc. cbmc menjangkakan goto-perduaan yang
pautan telah selesai.

goto-instrument membaca goto-binary, melakukan transformasi program yang diberikan, dan kemudian
menulis program yang terhasil sebagai goto-binary pada cakera.

Aliran biasa ialah (1) menterjemah sumber kepada goto-binary menggunakan goto-cc, kemudian (2)
melakukan instrumentasi dengan goto-instrument, dan akhirnya (3) melaksanakan analisis dengan
cbmc.

PILIHAN

FRONTEND PILIHAN (cbmc and goto-cc)
-Saya jalan
Tetapkan laluan sertakan (C/C++)

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

--praproses
Berhenti selepas prapemprosesan

--tunjuk-simbol-jadual
Tunjukkan jadual simbol

--show-goto-fungsi
Tunjukkan program goto

ARKITEKTUR PILIHAN (cbmc and goto-cc)
cbmc secara lalai menggunakan tetapan seni bina yang sepadan dengan tetapan mesin cbmc is
dilaksanakan pada, iaitu, tetapan di bawah hanya diperlukan semasa mengesahkan perisian iaitu
dimaksudkan untuk dijalankan pada seni bina atau OS yang berbeza. goto-cc menjana goto-perduaan untuk a
seni bina tertentu, iaitu, seni bina tidak boleh diubah selepas goto-binary
dihasilkan.

--16, --32, --64
Tetapkan lebar int

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Tetapkan lebar int, panjang dan penunjuk

--kecil-endian
Benarkan penukaran perkataan-bait kecil-endian

--big-endian
Benarkan penukaran perkataan-bait besar-endian

--unsigned-char
Jadikan "char" tidak ditandatangani secara lalai

--arch Tetapkan seni bina sasaran

--os Tetapkan sistem pengendalian sasaran

--tiada-gerbang
Jangan sediakan seni bina

--tiada perpustakaan
Lumpuhkan perpustakaan C abstrak terbina dalam

--bulat-ke-hampir-hampir, --bulat-ke-tambah-inf, --bulat-ke-tolak-inf, --bulat-ke-sifar
Mod pembundaran titik terapung IEEE untuk digunakan apabila program bermula (lalai ialah bulat
kepada yang terdekat). Program di bawah pengesahan boleh mengatasi tetapan ini, cth, dengan
fesetround(3).

PROGRAM INSTRUMENTASI PILIHAN (cbmc and goto-instrument)
Kedua-dua cbmc and goto-instrument boleh menghasilkan penegasan yang menangkap ralat biasa tertentu,
seperti yang disenaraikan di bawah.

--semak-batas
Dayakan semakan sempadan tatasusunan

--div-dengan-sifar-semak
Dayakan pembahagian dengan semakan sifar

--semak-penunjuk
Dayakan semakan penunjuk

--signed-overflow-check
Dayakan semakan lebihan dan aliran bawah aritmetik untuk aritmetik integer yang ditandatangani

--unsigned-overflow-check
Dayakan semakan lebihan dan aliran bawah aritmetik untuk aritmetik integer yang tidak ditandatangani

--nan-semak
Semak pengiraan titik terapung untuk NaN

--tiada-penegasan
Abaikan dakwaan yang disediakan pengguna

--tiada-andaian
Abaikan andaian yang diberikan oleh pengguna

--label-label ralat
Semak sama ada label yang diberikan tidak dapat dicapai

PROGRAM INSTRUMENTASI PILIHAN (goto-instrument sahaja)
goto-instrument menyokong lebih lanjut, lebih kompleks, transformasi program.

--nondet-volatile
Menjadikan bacaan daripada pembolehubah yang tidak menentu tidak pasti

--fungsi isr
Alatkan rutin perkhidmatan gangguan dengan nama yang diberikan

--mmio Instrumen dipetakan memori I/O

--nondet-statik
Pembolehubah dengan jangka hayat statik dimulakan secara bukan deterministik

--buang-c
Keluarkan kod sumber ANSI-C dan bukannya binari goto.

BMC PILIHAN (cbmc)
--semua-harta
Laporkan status semua hartanah

--show-properties
Hanya tunjukkan sifat

--show-gelung
Tunjukkan gelung dalam program

--cover-penegasan
Semak pernyataan yang boleh dicapai

--nama fungsi
Tetapkan nama fungsi utama

--id hartanah
Hanya semak harta tertentu dengan pengecam yang diberikan

--program-sahaja
Hanya tunjukkan ekspresi program

--kedalaman nr
Hadkan kedalaman carian

--rehatkan no
Longgarkan gelung nr kali

--lepas kerehatan L:B,...
Lepaskan gelung L dengan sekatan B (gunakan --show-loops untuk mendapatkan ID gelung)

--tunjukkan-vcc
Tunjukkan syarat pengesahan

--slice-formula
Alih keluar tugasan yang tidak berkaitan dengan harta benda

--tidak-melepaskan-penegasan
Jangan menjana dakwaan yang melelahkan

--tiada-nama-cantik
Jangan mudahkan pengecam

KEMBALI PILIHAN (cbmc)
--dimacs
Hasilkan CNF dalam format DIMACS untuk digunakan oleh penyelesai SAT luaran

--cantikkan-tamak
Cantikkan contoh balas (heuristik tamak)

--smt1 Output submatlamat dalam sintaks SMT1 (percubaan)

--smt2 Output submatlamat dalam sintaks SMT2 (percubaan)

--boolector
Gunakan Boolector (percubaan)

--mathsat
Gunakan MathSAT (percubaan)

--cvc Gunakan CVC3 (percubaan)

--yices
Gunakan Yices (percubaan)

--z3 Gunakan Z3 (percubaan)

--halusi
Gunakan prosedur penghalusan (percubaan)

--nama fail fail
Formula keluaran ke fail yang diberikan

--susunan-uf-tidak pernah
Jangan sekali-kali menukar tatasusunan kepada fungsi yang tidak ditafsirkan

--susunan-uf-selalu
Sentiasa tukar tatasusunan kepada fungsi yang tidak ditafsirkan

PERSEKITARAN

Semua alatan menghormati pembolehubah persekitaran TMPDIR apabila menjana fail sementara dan
direktori. Tambahan pula ambil perhatian bahawa prapemproses yang digunakan oleh CBMC akan menggunakan persekitaran
pembolehubah untuk mencari fail pengepala. GOTO-CC bertujuan untuk menerima semua pembolehubah persekitaran yang
GCC melakukannya.

HAKCIPTA

2001-2014, Daniel Kroening, Edmund Clarke

Gunakan goto-cc dalam talian menggunakan perkhidmatan onworks.net