frama-c-gui - Dalam Talian di Awan

JADUAL:

NAMA

frama-c[.byte] - penganalisis statik untuk program C

frama-c-gui[.byte] - antara muka grafik bagi frama-c

SINOPSIS

frama-c [ pilihan ] fail

DESCRIPTION

frama-c ialah satu set alat khusus untuk analisis kod sumber yang ditulis dalam C. Ia
mengumpulkan beberapa teknik analisis statik dalam satu rangka kerja kolaboratif. ini
rangka kerja boleh dilanjutkan dengan pemalam tambahan yang diletakkan di dalam $FRAMAC_PLUGIN direktori.
Perintah itu

frama-c -membantu

akan memberikan senarai penuh pemalam yang sedang dipasang.

frama-c-gui ialah antara muka pengguna grafik bagi frama-c. Ia mempunyai pilihan yang sama seperti
versi baris arahan.

frama-c.bait and frama-c-gui.bait ialah versi kod bait ocaml bagi baris arahan dan
antara muka pengguna grafik masing-masing.

Secara lalai, Frama-C mengecam .c fail sebagai fail C yang memerlukan pra-pemprosesan dan .i fail sebagai
Fail C telah dipraproses. Sesetengah pemalam mungkin memanjangkan senarai yang diiktiraf
fail. Pra-pemprosesan boleh disesuaikan melalui -cpp-arahan and -cpp-extra-args
pilihan.

PILIHAN

Syntax

Pilihan yang mengambil parameter tambahan juga boleh ditulis di bawah borang

-pilihan=param

Pilihan ini adalah wajib apabila param bermula dengan tanda sempang ('-')

Kebanyakan pilihan yang tidak mengambil parameter mempunyai yang sepadan

-dekat-pilihan

pilihan yang mempunyai kesan sebaliknya.

Bantuan pilihan

-membantu memberikan notis penggunaan singkat dan senarai pemalam yang dipasang.

-kernel-help
mencetak senarai pilihan yang diiktiraf oleh kernel Frama-C

-berkata-kata n
Menetapkan tahap verbositi (lalai ialah 1). Menetapkannya kepada 0 akan menghasilkan kurang kemajuan
mesej. Tahap ini juga boleh ditetapkan pada per Pasangkan asas, dengan pilihan -Pasangkan-
kata kerja n. Tahap verbositas kernel boleh dikawal dengan pilihan
-kernel-verbose n.

-nyahpepijat n
Menetapkan tahap penyahpepijatan (lalai ialah 0, bermakna tiada mesej penyahpepijatan). Pilihan ini
mempunyai pengkhususan setiap pemalam (dan kernel) yang sama seperti -berkata-kata.

-senyap Tetapkan tahap verbositi dan penyahpepijatan kepada 0.

Pilihan mengawal Frama-C kernel

-julat-sah-mutlak
menganggap bahawa semua alamat berangka dalam julat min-maks adalah sah. Sempadan adalah
dihuraikan sebagai pemalar integer ocaml. Secara lalai, semua alamat berangka adalah
dianggap tidak sah.

-laluan-tambah p1[,p2[...,pn]]
menambah direktori melalui ke senarai direktori di mana pemalam berada
dicari

[-tidak]-benarkan-pendua
membenarkan penduaan blok kecil semasa menormalkan ujian dan gelung.
Jika tidak, normalisasi menggunakan label dan gotos. Blok dan blok yang lebih besar dengan bukan
aliran kawalan remeh tidak pernah diduplikasi. Lalai kepada ya.

[-tidak]-tidak
membaca anotasi ACSL. Ini adalah lalai. Anotasi tidak diproses terlebih dahulu oleh
lalai. guna -pp-annot untuk itu.

-big-ints-hex maks
integer lebih besar daripada maks dipaparkan dalam perenambelasan (secara lalai, semua integer adalah
dipaparkan dalam perpuluhan)

-semak melakukan semakan integriti pada AST dalaman (untuk pembangun sahaja).

[-no]-collapse-call-cast
membenarkan hantaran tersirat antara nilai yang dikembalikan oleh fungsi dan nilainya
ditugaskan untuk. Jika tidak, pembolehubah sementara digunakan dan pelakon dibuat secara eksplisit.
Lalai kepada ya.

[-tidak]-constfold
melipat semua ungkapan malar sintaksis dalam kod sebelum dianalisis. Lalai
kepada tidak.

[-tidak]-terus-jangan-ralat
Apabila menganalisis anotasi, tingkah laku lalai (the -dekat versi pilihan ini)
apabila ralat semakan taip berlaku adalah untuk menolak fail sumber seperti yang berlaku untuk
ralat semakan taip dalam kod C. Dengan pilihan ini dihidupkan, penyemak taip akan
hanya mengeluarkan amaran dan buang anotasi tetapi semakan taip akan diteruskan
(ralat dalam kod C masih membawa maut, walaupun).

-cpp-arahan cmd
kegunaan cmd sebagai arahan untuk pra-memproses fail C. Lalai kepada CPP persekitaran
pembolehubah atau kepada

gcc -C -E -I.

jika ia tidak ditetapkan. Untuk mengekalkan anotasi ACSL, prapemproses mesti menyimpan
komen (yang -C pilihan untuk gcc). %1 and %2 boleh digunakan dalam cmd untuk menandakan
fail sumber asal dan fail pra-diproses masing-masing

-cpp-extra-args args
Memberi hujah tambahan kepada pra-pemproses. Ini hanya berguna apabila
-praproses-annot ditetapkan. Anotasi pra-pemprosesan dilakukan dalam dua pra-
peringkat pemprosesan. Yang pertama ialah pas biasa pada kod C yang mengekalkan makro
takrifan. Ini kemudian digunakan dalam pas kedua di mana anotasi berada
pra-diproses. args digunakan hanya untuk pas pertama, supaya hujah itu
tidak boleh digunakan dua kali (seperti tambahan termasuk arahan atau makro
definisi) oleh itu mesti pergi ke sana dan bukannya -cpp-arahan.

[-tidak]-dynlink
Apabila dihidupkan, muatkan semua pemalam dinamik yang terdapat dalam laluan carian (lihat -print-plugin-
jalan untuk maklumat lanjut tentang laluan carian lalai). Jika tidak, hanya pemalam
diminta oleh -beban-modul akan dimuatkan. Tingkah laku lalai dihidupkan.

-enum teguran
Pilih cara perwakilan jenis terbilang ditentukan. frama-c
-enum membantu memberikan senarai pilihan yang tersedia. Lalai ialah gcc-enums

-digit terapung n
Apabila mengeluarkan nombor titik terapung, paparkan n digit. Lalai kepada 12.

-float-flush-ke-sifar
Operasi titik terapung siram kepada sifar

-float-hex
paparan terapung sebagai perenambelasan

-terapung-biasa
paparan terapung dengan rutin Ocaml standard

-apung-saudara
paparkan selang apungan sebagai [ lower_bound++lebar ]

[-no]-force-rl-arg-eval
memaksa perintah penilaian kanan ke kiri untuk hujah panggilan fungsi. Jika tidak
susunan penilaian dibiarkan tidak ditentukan, seperti dalam piawaian C. Lalai kepada no.

-jurnal-lumpuhkan
Jangan keluarkan jurnal sesi semasa. Lihat -jurnal-membolehkan.

-jurnal-membolehkan
Dihidupkan secara lalai, membuang jurnal semua tindakan yang dilakukan semasa semasa
Sesi Frama-C dalam bentuk skrip ocaml yang boleh dimainkan semula -beban-
skrip. Nama skrip boleh ditetapkan dengan -nama-jurnal pilihan.

-nama-jurnal nama
Tetapkan nama fail jurnal (tanpa .ml sambungan). Lalai kepada
frama_c_journal.

-dimulakan-padding-lokal
Inisialisasi tersirat bagi penduduk tempatan menetapkan bit padding kepada 0. Jika palsu, bit padding
dibiarkan tanpa dimulakan (lalai kepada ya).

[-tidak]-simpan-komen
Cuba untuk mengekalkan komen apabila mencetak kod sumber dengan cantik (lalai kepada tidak).

[-tidak]-simpan-suis
Bila -permudahkan-cfg ditetapkan, menyimpan penyata suis. Lalai kepada no.

-kekalkan-fungsi-ditentukan-tidak digunakan
Lihat -buang-tidak digunakan-dinyatakan-fungsi

[-no]-lib-masuk
Menunjukkan bahawa titik masuk dipanggil semasa pelaksanaan program. Ini bermakna dalam
khususnya bahawa pembolehubah global tidak boleh diandaikan mempunyai nilai awalnya.
Lalai adalah -tiada-masuk-lib: titik masuk juga merupakan titik permulaan
program dan global mempunyai nilai awalnya.

-load fail
muatkan keadaan (sebelum ini disimpan) yang terkandung dalam fail.

-beban-modul m1[,m2[...,mn]]
memuatkan modul ocaml melalui . Modul-modul ini mestilah .cmxsfail untuk
versi kod asli Frama-c dan .cmoor.cmafail untuk versi bytecode (lihat
bahagian Dynlink manual Ocaml untuk maklumat lanjut). Semua modul yang
hadir dalam laluan carian pemalam dimuatkan secara automatik.

-muat-skrip s1[,s2,[...,sn]]
memuatkan skrip ocaml melalui . Skrip mestilah .mlfail. mereka
mesti boleh dikompilasi hanya bergantung pada perpustakaan standard Ocaml dan API Frama-C. Jika
beberapa langkah penyusunan tersuai diperlukan, susunkannya di luar Frama-C dan gunakan
-beban-modul sebaliknya.

-machdep mesin
menggunakan mesin sebagai konfigurasi yang bergantung kepada mesin semasa (saiz pelbagai
jenis integer, endiandness, ...). Senarai mesin yang disokong pada masa ini ialah
boleh didapati melalui -machdep membantu pilihan. Lalai ialah x86_32

-utama f
Set f sebagai titik masuk analisis. Lalai kepada 'utama'. Secara lalai, ia adalah
dianggap sebagai titik permulaan program yang dianalisis. guna -masuk-lib if f
sepatutnya dipanggil di tengah-tengah pelaksanaan.

-mengelirukan
mencetak versi kod yang dikelirukan (di mana pengecam asal diganti
dengan yang tidak bermakna) dan keluar. Jadual surat menyurat antara asal dan baharu
simbol disimpan pada permulaan keputusan.

-okod fail
mengubah hala kod yang dicetak cantik ke fail bukannya keluaran standard.

[-no]-nama-asal
Semasa fasa normalisasi, beberapa pembolehubah mungkin dinamakan semula apabila berbeza
pembolehubah dengan nama yang sama boleh wujud bersama (cth pembolehubah global dan pembolehubah formal
parameter). Apabila pilihan ini dihidupkan, mesej dicetak setiap kali ini berlaku.
Lalai kepada no.

[-no]-warn-signed-downcast
menjana penggera apabila downcast yang ditandatangani mungkin melebihi julat destinasi (lalai kepada
tidak).

[-no]-warn-signed-overflow
jana penggera untuk operasi yang ditandatangani yang melimpah (lalai kepada ya).

[-no]-warn-unsigned-downcast
menjana penggera apabila downcast yang tidak ditandatangani mungkin melebihi julat destinasi (lalai
kepada tidak).

[-no]-warn-unsigned-overflow
menjana penggera untuk operasi tidak ditandatangani yang melimpah (lalai kepada tidak).

[-tidak]-pp-annot
anotasi pra-proses. Ini hanya boleh dilakukan pada masa ini apabila menggunakan gcc (atau GNU
cpp) pra-pemproses. Lalainya ialah bukan pra-proses anotasi.

[-tidak]-cetak
pretty-mencetak kod sumber seperti yang dinormalkan oleh CIL (lalai kepada tidak).

-print-libpath
mengeluarkan direktori tempat pustaka kernel Frama-C dipasang

-jalan-cetak
alias daripada -cetak-kongsi-laluan

-print-plugin-path
mengeluarkan direktori tempat Frama-C mencari pemalamnya (boleh digantikan oleh
FRAMAC_PLUGIN pemboleh ubah dan -laluan-tambah pilihan)

-cetak-kongsi-laluan
mengeluarkan direktori tempat Frama-C menyimpan datanya (boleh digantikan oleh
FRAMAC_SHARE pembolehubah)

-buang-tidak digunakan-dinyatakan-fungsi
menyimpan prototaip fungsi yang mempunyai spesifikasi ACSL tetapi tidak digunakan dalam
kod. Ini adalah lalai. Fungsi yang mempunyai atribut FRAMAC_BUILTIN sentiasa
disimpan.

-susun-selamat
Untuk tatasusunan berbilang dimensi atau tatasusunan yang merupakan medan di dalam structs , andaikan itu
semua akses mesti dalam terikat (ditetapkan secara lalai). Pilihan yang bertentangan ialah -tidak selamat-
tatasusunan

-jimat fail
Menyimpan keadaan Frama-C ke dalam fail selepas analisis dilakukan.

[-tidak]-permudahkan-cfg
mengalih keluar penyataan break, continue dan switch sebelum analisis. Lalai kepada no.

-kemudian membolehkan seseorang mengarang analisis: larian pertama Frama-C akan berlaku dengan pilihan
sebelum -kemudian dan larian kedua akan dilakukan dengan pilihan selepas -kemudian pada
projek semasa dari larian pertama.

-kemudian prj
Sama seperti -kemudian kecuali larian kedua dilakukan dalam projek prj Jika tidak begitu
projek wujud, Frama-C keluar dengan ralat.

-masa fail
menambahkan masa dan tarikh pengguna dalam yang diberikan fail apabila Frama-C keluar.

-semak taip
memaksa penyemakan taip fail sumber. Pilihan ini hanya relevan jika tidak lebih lanjut
analisis diminta (kerana penyemakan taip akan berlaku secara tersirat sebelum analisis
dilancarkan).

-ulevel n
buka gelung secara sintaksis n kali sebelum analisis. Ini boleh menjadi agak mahal
dan beberapa pemalam (cth analisis nilai) menyediakan cara yang lebih cekap untuk melaksanakan
benda yang sama. Lihat manual masing-masing untuk maklumat lanjut. Ini juga boleh
diaktifkan secara per-gelung melalui gelung pragma batal arahan. A
nilai negatif untuk n akan menghalang pragma tersebut.

[-no]-unicode
mengeluarkan formula ACSL dengan aksara utf8. Ini adalah lalai. Apabila diberi
-tiada-unikod pilihan, Frama-C akan menggunakan versi ASCII sebaliknya. Lihat manual ACSL
untuk surat menyurat.

-susunan-tidak selamat
lihat -susun-selamat

[-no]-unspecified-access
semak bahawa akses baca/tulis berlaku dalam susunan yang tidak ditentukan (mengikut C
tanggapan standard titik jujukan) dilakukan pada lokasi yang berasingan. Dengan
-tiada-akses yang tidak ditentukan, menganggap bahawa ia sentiasa berlaku (ini adalah lalai).

-turun
mengeluarkan rentetan versi Frama-C

-amaran-perpuluhan-apung
memberi amaran apabila pemalar titik terapung tidak boleh diwakili dengan tepat (cth 0.1).
boleh menjadi salah satu tiada, sekali, Atau semua

[-tidak]-amaran-tidak-diisytiharkan-pemanggil
memberi amaran apabila fungsi dipanggil sebelum ia diisytiharkan (ditetapkan secara lalai).
Frama-C

Plugin khusus pilihan

Bagi setiap Pasangkan, arahan

frama-c -Pasangkan-membantu

akan memberikan senarai pilihan yang khusus untuk pemalam.

EXIT STATUS

0 Perlaksanaan yang berjaya

1 Input pengguna tidak sah

2 Gangguan pengguna (bunuh atau setara)

3 Ciri yang tidak dilaksanakan

4 5 6 Masalah dalaman

125 Ralat tidak diketahui

Status keluar lebih daripada 2 boleh dianggap sebagai pepijat (atau permintaan ciri untuk kes itu
status keluar 3) dan mungkin dilaporkan pada BTS Frama-C (lihat di bawah).

PERSEKITARAN PELBAGAI

Adalah mungkin untuk mengawal tempat di mana Frama-C mencari failnya melalui
pembolehubah berikut.

FRAMAC_LIB
Direktori tempat antara muka tersusun kernel dipasang

FRAMAC_PLUGIN
Direktori tempat Frama-C boleh mencari pemalam standard. Jika anda ingin mempunyai pemalam
di beberapa tempat, gunakan -laluan-tambah sebaliknya.

FRAMAC_SHARE
Direktori tempat data Frama-C dipasang.

Gunakan frama-c-gui dalam talian menggunakan perkhidmatan onworks.net