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 العديد من تقنيات التحليل في منصة تعاونية واحدة ، تتكون من kernel توفر مجموعة أساسية من الميزات (على سبيل المثال ، AST الطبيعية لبرامج C) بالإضافة إلى مجموعة من المحللين ، تسمى المكونات الإضافية . يمكن أن تعتمد المكونات الإضافية على النتائج المحسوبة بواسطة المكونات الإضافية الأخرى في النظام الأساسي.
بفضل هذا النهج ، يوفر Frama-C أدوات متطورة ، بما في ذلك:
تشترك هذه المكونات الإضافية في لغة مشتركة ويمكنها تبادل المعلومات عبر خصائص ACSL ( لغة مواصفات ACSL (ANSI/ISO C ). يمكن أن تتعاون المكونات الإضافية أيضًا عبر واجهات برمجة التطبيقات الخاصة بهم.
لمزيد من المعلومات التفصيلية حول تثبيت 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 ، إلخ. يمكن أيضًا تشغيل المكونات الإضافية مباشرة من واجهة المستخدم الرسومية.
لسرد جميع المكونات الإضافية ، قم بتشغيل:
frama-c -plugins
يحتوي كل مكون إضافي على أمر تعليمات ( -<plugin>-help أو- -<plugin>-h ) الذي يصف خياراته العديدة.
أخيرًا ، تتوفر قائمة الخيارات التي تحكم سلوك نواة Frama-C نفسها من خلال
frama-c -kernel-help
للحصول على سيناريوهات الاستخدام الأكثر تعقيدًا (الكثير من الملفات والأدلة ، مع العديد من توجيهات المعالجة المسبقة) ، نوصي بتقسيم استخدام Frama-C في جزأين:
يتضمن التحليل عادةً إعطاء وسيطات إضافية للمعالج المسبق C ، لذلك غالبًا ما يكون خيار -cpp-extra-args مفيدًا ، كما في المثال أدناه:
frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav
ثم يتم تحميل النتائج في Frama-C لمزيد من التحليلات أو للتفتيش عبر واجهة المستخدم الرسومية:
frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]
تتوفر روابط إلى أدلة المستخدم والمطورين ، ومحفوظات Frama-C ، وأدلة المكونات الإضافية على
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 مستقرة ، جاهزة للاستنساخ. يمكن أيضًا استخدامه للإبلاغ عن مشكلات وتقديم طلبات السحب.
