Frama C snapshot

Frama-C adalah platform yang didedikasikan untuk analisis kode sumber yang ditulis dalam C.

Catatan: Repositori Frama-C resmi sekarang ada di Gitlab kami!

Frama-C telah memindahkan repositori resminya ke instance Gitlab yang diselenggarakan sendiri.

Rilis resmi (mulai dari Frama-C 21) tidak akan lagi diperbarui di sini.

Snapshot malam juga tersedia di gitlab kami! Anda sekarang bisa mendapatkan akses ke versi pengembangan terbaru di: https://git.frama-c.com/pub/frama-c/-/tree/master

Pelacak edisi frama-c resmi sekarang di gitlab kami: https://git.frama-c.com/pub/frama-c/-/issues

Anda dapat mengirimkan masalah dan menarik permintaan menggunakan login GitHub Anda (pilih "Masuk dengan GitHub" saat diminta).

Sampai jumpa di sana!

Platform kolaboratif

Frama-C mengumpulkan beberapa teknik analisis dalam platform kolaboratif tunggal, yang terdiri dari kernel yang menyediakan serangkaian fitur inti (misalnya, AST yang dinormalisasi untuk program C) ditambah serangkaian analisis, yang disebut plug-in . Plug-in dapat dibangun berdasarkan hasil yang dihitung oleh plug-in lain di platform.

Berkat pendekatan ini, Frama-C menyediakan alat canggih, termasuk:

• seorang penganalisa berdasarkan interpretasi abstrak, yang bertujuan memverifikasi tidak adanya kesalahan run-time ( EVA );
• kerangka kerja bukti program berdasarkan kalkulus prasyarat terlemah ( WP );
• Program Slicer ( mengiris );
• alat untuk verifikasi properti temporal (LTL) ( Aoraï );
• Alat Verifikasi Runtime ( E-ACSL );
• Beberapa alat untuk eksplorasi basis kode dan analisis ketergantungan ( dari , dampak , metrik , kejadian , ruang lingkup , dll.).

Plug-in ini berbagi bahasa umum dan dapat bertukar informasi melalui properti ACSL ( ANSI/ISO C Spesifikasi Bahasa ). Plug-in juga dapat berkolaborasi melalui API mereka.

Instalasi

Untuk informasi lebih rinci tentang menginstal OPAM/Frama-C, lihat Install.md.

Frama-C tersedia melalui OPAM, OCAML Package Manager. Ini adalah metode instalasi yang disukai. Pastikan untuk menginstal OPAM V2.0 atau lebih tinggi. Kemudian urutan perintah berikut harus menginstal Frama-C dan GUI-nya:

 opam init
opam install depext
opam depext frama-c
opam install frama-c

Frama-C dikembangkan terutama di Linux, sering diuji dalam macOS (melalui homebrew), dan sesekali diuji pada windows (melalui subsistem Windows untuk Linux).

Penggunaan

Frama-C dapat dijalankan dari baris perintah, atau melalui antarmuka grafisnya.

Penggunaan sederhana

Penggunaan yang disarankan untuk file sederhana adalah salah satu baris berikut:

 frama-c file.c -<plugin> [options]
frama-c-gui file.c

Di mana -<plugin> adalah salah satu dari beberapa plug -in frama -C, misalnya -eva , atau -wp , atau -metrics , dll. Plug -in juga dapat dijalankan langsung dari GUI.

Untuk mendaftar semua plug-in, jalankan:

 frama-c -plugins

Setiap plug-in memiliki perintah bantuan ( -<plugin>-help atau- -<plugin>-h ) yang menjelaskan beberapa opsi.

Akhirnya, daftar opsi yang mengatur perilaku kernel Frama-C itu sendiri tersedia melalui

 frama-c -kernel-help

Skenario kompleks

Untuk skenario penggunaan yang lebih kompleks (banyak file dan direktori, dengan beberapa arahan preprocessing), kami sarankan pemisahan penggunaan Frama-C dalam dua bagian:

1. Parsing file input dan menyimpan hasilnya ke file;
2. Memuat hasil parsing dan kemudian menjalankan analisis atau GUI.

Parsing biasanya melibatkan memberikan argumen tambahan kepada preprocessor C, sehingga opsi -cpp-extra-args sering berguna, seperti pada contoh di bawah ini:

 frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav

Hasilnya kemudian dimuat ke dalam Frama-C untuk analisis lebih lanjut atau untuk diperiksa melalui GUI:

 frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]

Referensi lebih lanjut

• Tautan ke manual pengguna dan pengembang, arsip Frama-C, dan manual plug-in tersedia di
  http://frama-c.com/download.html

• StackoverFlow memiliki beberapa pertanyaan dengan tag frama-c , yang dipantau oleh beberapa anggota komunitas Frama-C.

• Mailing Frama-C-Discuss digunakan untuk pengumuman dan diskusi umum.

• Sistem pelacakan bug resmi dapat digunakan untuk laporan bug.

• Wiki Frama-C memiliki beberapa informasi yang berguna, meskipun tidak sepenuhnya mutakhir.

• Blog Frama-C memiliki beberapa posting tentang perkembangan baru Frama-C, serta diskusi umum tentang bahasa C, perilaku yang tidak terdefinisi, perhitungan titik mengambang, dll.

• Repositori Snapshot GitHub berisi arsip .tar.gz rilis Frama-C yang stabil, siap dikloning. Ini juga dapat digunakan untuk pelaporan masalah dan mengirimkan permintaan tarik.