Frama C snapshot
1.0.0
Frama-C เป็นแพลตฟอร์มที่อุทิศให้กับการวิเคราะห์ซอร์สโค้ดที่เขียนใน C.
Frama-C ได้ย้ายที่เก็บอย่างเป็นทางการไปยังอินสแตนซ์ Gitlab ที่โฮสต์ตนเองของเรา
การเปิดตัวอย่างเป็นทางการ (เริ่มต้นจาก FRAMA-C 21) จะไม่ได้รับการปรับปรุงที่นี่อีกต่อไป
สแน็ปช็อตทุกคืนยังมีอยู่ใน Gitlab ของเรา! ตอนนี้คุณสามารถเข้าถึงเวอร์ชันการพัฒนาล่าสุดได้ที่: https://git.frama-c.com/pub/frama-c/-/tree/master
ตัวติดตามปัญหา Frama-C อย่างเป็นทางการอยู่ที่ Gitlab ของเรา: https://git.frama-c.com/pub/frama-c//issues
คุณสามารถส่งปัญหาและดึงคำขอโดยใช้การเข้าสู่ระบบ GitHub ของคุณ (เลือก "ลงชื่อเข้าใช้ด้วย GitHub" เมื่อได้รับแจ้ง)
แล้วเจอกัน!
Frama-C รวบรวมเทคนิคการวิเคราะห์หลายอย่างในแพลตฟอร์มการทำงานร่วมกันเดียวซึ่งประกอบด้วย เคอร์เนล ที่ให้คุณสมบัติหลักของคุณสมบัติ (เช่น AST ปกติสำหรับโปรแกรม C) รวมถึงชุดของเครื่องวิเคราะห์ที่เรียกว่า ปลั๊กอิน ปลั๊กอินสามารถสร้างตามผลลัพธ์ที่คำนวณโดยปลั๊กอินอื่น ๆ ในแพลตฟอร์ม
ด้วยวิธีการนี้ FRAMA-C มีเครื่องมือที่ซับซ้อนรวมถึง:
ปลั๊กอินเหล่านี้แบ่งปันภาษาร่วมกันและสามารถแลกเปลี่ยนข้อมูลผ่านคุณสมบัติ ACSL ( ภาษาข้อกำหนด ANSI/ISO C ) ปลั๊กอินยังสามารถทำงานร่วมกันผ่าน API ของพวกเขา
สำหรับข้อมูลรายละเอียดเพิ่มเติมเกี่ยวกับการติดตั้ง OPAM/FRAMA-C ดูที่ Install.md
FRAMA-C มีให้บริการผ่าน OPAM ผู้จัดการแพ็คเกจ OCAML นี่คือวิธีการติดตั้งที่ต้องการ ตรวจสอบให้แน่ใจว่าได้ติดตั้ง OPAM v2.0 หรือสูงกว่า จากนั้นลำดับของคำสั่งต่อไปนี้ควรติดตั้ง FRAMA-C และ GUI ของมัน:
opam init
opam install depext
opam depext frama-c
opam install frama-c
Frama-C ได้รับการพัฒนาเป็นหลักใน Linux ซึ่งมักจะทดสอบใน MacOS (ผ่าน Homebrew) และทดสอบเป็นครั้งคราวบน Windows (ผ่านระบบย่อย Windows สำหรับ Linux)
FRAMA-C สามารถเรียกใช้จากบรรทัดคำสั่งหรือผ่านอินเตอร์เฟสกราฟิก
การใช้งานที่แนะนำสำหรับไฟล์ง่าย ๆ เป็นหนึ่งในบรรทัดต่อไปนี้:
frama-c file.c -<plugin> [options]
frama-c-gui file.c
โดยที่ -<plugin> เป็นหนึ่งในหลาย ๆ ปลั๊กอิน frama -c เช่น -eva หรือ -wp หรือ -metrics ฯลฯ ปลั๊กอินสามารถเรียกใช้โดยตรงจาก GUI
หากต้องการแสดงรายการปลั๊กอินทั้งหมด Run:
frama-c -plugins
ปลั๊กอินแต่ละตัวมีคำสั่งวิธีใช้ ( -<plugin>-help หรือ -<plugin>-h ) ที่อธิบายตัวเลือกต่าง ๆ
ในที่สุดรายการตัวเลือกที่ควบคุมพฤติกรรมของเคอร์เนลของ Frama-C นั้นมีให้บริการผ่าน
frama-c -kernel-help
สำหรับสถานการณ์การใช้งานที่ซับซ้อนมากขึ้น (ไฟล์และไดเรกทอรีจำนวนมากพร้อมคำสั่งการประมวลผลล่วงหน้าหลายคำ) เราขอแนะนำให้แยกการใช้งานของ Frama-C เป็นสองส่วน:
การแยกวิเคราะห์มักจะเกี่ยวข้องกับการให้ข้อโต้แย้งเพิ่มเติมกับตัวประมวลผล c preprocessor ดังนั้นตัวเลือก -cpp-extra-args มักจะมีประโยชน์เช่นในตัวอย่างด้านล่าง:
frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav
ผลลัพธ์จะถูกโหลดลงใน FRAMA-C สำหรับการวิเคราะห์เพิ่มเติมหรือตรวจสอบผ่าน GUI:
frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]
ลิงค์ไปยังคู่มือผู้ใช้และนักพัฒนา
http://frama-c.com/download.html
Stackoverflow มีคำถามหลายข้อเกี่ยวกับแท็ก frama-c ซึ่งได้รับการตรวจสอบโดยสมาชิกหลายคนของชุมชน Frama-C
รายชื่อส่งจดหมาย FRAMA-C-Discuss ใช้สำหรับการประกาศและการอภิปรายทั่วไป
ระบบติดตามข้อผิดพลาดอย่างเป็นทางการสามารถใช้สำหรับรายงานข้อผิดพลาด
Frama-C Wiki มีข้อมูลที่เป็นประโยชน์บางอย่างแม้ว่าจะไม่ทันสมัยทั้งหมด
บล็อก FRAMA-C มีหลายโพสต์เกี่ยวกับการพัฒนาใหม่ของ FRAMA-C รวมถึงการอภิปรายทั่วไปเกี่ยวกับภาษา C พฤติกรรมที่ไม่ได้กำหนดการคำนวณจุดลอยตัว ฯลฯ
ที่เก็บสแน็ปช็อตของ GitHub มีไฟล์เก็บถาวร. tar.gz ของการเผยแพร่ Frama-C ที่มั่นคงพร้อมที่จะโคลน นอกจากนี้ยังสามารถใช้สำหรับการรายงานปัญหาและส่งคำขอดึง
