frama-c.byte - عبر الإنترنت في السحابة

برنامج:

اسم

Frama-c [.byte] - محلل ثابت لبرامج C.

Frama-c-gui [.byte] - الواجهة الرسومية لـ Frama-c

موجز

فراما ج [ الخيارات ] ملفات

الوصف

فراما ج عبارة عن مجموعة من الأدوات المخصصة لتحليل شفرة المصدر المكتوبة بلغة C. It
يجمع العديد من تقنيات التحليل الثابت في إطار تعاوني واحد. هذه
يمكن تمديد إطار العمل عن طريق الإضافات الإضافية الموضوعة في FRAMAC_PLUGIN دولار الدليل.
الامر

فراما ج - التعليمات

سيوفر القائمة الكاملة للمكونات الإضافية المثبتة حاليًا.

فراما سي غوي هي واجهة المستخدم الرسومية لـ فراما ج. يتميز بنفس الخيارات مثل
إصدار سطر الأوامر.

فراما سي بايت و فراما سي غوي بايت هي إصدارات ocaml bytecode لسطر الأوامر و
واجهة المستخدم الرسومية على التوالي.

يتعرف Frama-C افتراضيًا على ملفات .c الملفات كملفات C تحتاج إلى معالجة مسبقة وملفات .i الملفات بتنسيق
تم بالفعل معالجة ملفات C مسبقًا. قد تعمل بعض المكونات الإضافية على توسيع قائمة ملفات
الملفات. يمكن تخصيص المعالجة المسبقة من خلال ملف -cpp- الأمر و -cpp-وسائط إضافية
خيارات.

OPTIONS

بناء الجملة

يمكن أيضًا كتابة الخيارات التي تأخذ معلمة إضافية ضمن النموذج

-خيار=المعلمة

هذا الخيار إلزامي عندما المعلمة يبدأ بشرطة ("-")

معظم الخيارات التي لا تأخذ أي معلمة لها قيمة مقابلة

-لا-اختيار

الخيار الذي له تأثير معاكس.

المساعدة الخيارات

-مساعدة يعطي إشعار استخدام قصير وقائمة المكونات الإضافية المثبتة.

مساعدة-kernel
يطبع قائمة الخيارات التي يتعرف عليها نواة Frama-C

-إفراط n
يعيّن مستوى الإسهاب (الافتراضي هو 1). تعيينه على 0 سينتج تقدمًا أقل
رسائل. يمكن أيضًا تعيين هذا المستوى على لكل المساعد أساس ، مع خيار -المساعد-
مطنب n. يمكن التحكم في مستوى الإسهاب في النواة باستخدام الخيار
-نواة- مطوّل n.

-ديبوغ n
يضبط مستوى التصحيح (الافتراضي هو 0 ، مما يعني عدم وجود رسائل تصحيح). هذا الخيار
له نفس تخصصات كل مكون إضافي (و kernel) مثل -إفراط.

-هادئ يعيّن الإسهاب ومستوى التصحيح إلى 0.

مزيد من الخيارات السيطرة فراما سي نواة

- المطلق - صالح - المدى
تعتبر أن جميع العناوين العددية في النطاق الحد الأدنى - الحد الأقصى صالحة. الحدود
تحليل ثوابت عدد صحيح ocaml. بشكل افتراضي ، جميع العناوين الرقمية هي
تعتبر غير صالحة.

-إضافة المسار p1 [، p2 [...، pn]]
يضيف الدلائل من خلال إلى قائمة الدلائل التي توجد بها المكونات الإضافية
البحث

[-لا] -السماح-الازدواجية
يسمح بتكرار الكتل الصغيرة أثناء تطبيع الاختبارات والحلقات.
وإلا ، فإن التطبيع يستخدم الملصقات والحروف الأساسية. كتل وكتل أكبر مع عدم
لا يتم تكرار تدفق التحكم البسيط. افتراضات إلى نعم.

[-لا] -لا
يقرأ شرح ACSL. هذا هو الافتراضي. لم تتم معالجة التعليقات التوضيحية مسبقًا بواسطة
إفتراضي. يستخدم -pp- توضيحي لذلك.

-كبير-ints- عرافة ماكس
أعداد صحيحة أكبر من ماكس يتم عرضها بالنظام الست عشري (افتراضيًا ، تكون جميع الأعداد الصحيحة
معروض في النظام العشري)

-التحقق من يقوم بإجراء فحوصات سلامة على AST الداخلية (للمطورين فقط).

[-لا] -طي-النداء-الزهر
يسمح بإلقاء ضمني بين القيمة التي يتم إرجاعها بواسطة دالة و lvalue هو
مخصص ل. خلاف ذلك ، يتم استخدام متغير مؤقت ويتم توضيح المصبوب.
افتراضات إلى نعم.

[-لا] -كونستفولد
تطوي جميع التعبيرات الثابتة نحويًا في الكود قبل التحليلات. الافتراضات
لا.

[-لا] -مواصلة-خطأ في التعليقات التوضيحية
عند تحليل تعليق توضيحي ، فإن السلوك الافتراضي (ملف -لا نسخة من هذا الخيار)
عند حدوث خطأ في التحقق من الكتابة ، يتم رفض الملف المصدر كما هو الحال بالنسبة لـ
فحص الأخطاء المطبعية داخل كود C. مع تشغيل هذا الخيار ، سوف يقوم فاحص الآلة الكاتبة
فقط قم بإخراج تحذير وتجاهل التعليق التوضيحي ولكن سيستمر التحقق من الكتابة
(الأخطاء في كود C لا تزال قاتلة ، رغم ذلك).

-cpp- الأمر كمد
استخدام كمد كأمر لمعالجة ملفات C مسبقًا. افتراضات إلى CPP بيئة
متغير أو إلى

دول مجلس التعاون الخليجي -C -E -I.

إذا لم يتم تعيينه. من أجل الحفاظ على تعليقات ACSL التوضيحية ، يجب أن يحتفظ المعالج المسبق بـ
التعليقات (ال -C خيار دول مجلس التعاون الخليجي). %1 و %2 يمكن استخدامها في كمد للدلالة على
ملف المصدر الأصلي والملف المعالج مسبقًا على التوالي

-cpp-وسائط إضافية وسائط
يعطي حجج إضافية للمعالج المسبق. هذا مفيد فقط عندما
-العملية التوضيحية تم تعيينه. تتم معالجة التعليقات التوضيحية مسبقًا في قسمين منفصلين مسبقًا
مراحل المعالجة. الأول هو تمرير عادي على كود C الذي يحتفظ بالماكرو
تعريفات. يتم استخدام هذه بعد ذلك في المسار الثاني الذي يتم خلاله استخدام التعليقات التوضيحية
مُعالجة مسبقًا. وسائط تستخدم فقط للمرور الأول ، لذلك فإن الحجج التي
لا يجب استخدامه مرتين (مثل توجيهات التضمين الإضافية أو الماكرو
التعريفات) يجب أن تذهب إلى هناك بدلاً من -cpp- الأمر.

[-لا] -Dynlink
عند التشغيل ، قم بتحميل جميع المكونات الإضافية الديناميكية الموجودة في مسار البحث (انظر -طباعة- البرنامج المساعد-
مسار لمزيد من المعلومات حول مسار البحث الافتراضي). خلاف ذلك ، الإضافات فقط
بتوصية من -حمل-وحدات سيتم تحميلها. السلوك الافتراضي قيد التشغيل.

-التعدادات تمثيلي
اختر طريقة تحديد تمثيل الأنواع التي تم تعدادها. فراما ج
-التعدادات مساعدة يعطي قائمة الخيارات المتاحة. الافتراضي هو enums دول مجلس التعاون الخليجي

-أرقام عائمة n
عند إخراج أرقام الفاصلة العائمة ، اعرض n أرقام. الافتراضي هو 12.

-طفو-تدفق إلى الصفر
تدفق عمليات النقطة العائمة إلى الصفر

-عوامة-عرافة
عرض يطفو على شكل سداسي عشري

-الطبيعية
عرض يطفو مع روتين أوكامل القياسي

- عائم نسبي
عرض الفاصل الزمني العائم كـ [ الأدنى++عرض ]

[-لا] -القوة- rl-arg-Eval
يفرض ترتيب التقييم من اليمين إلى اليسار لوسائط استدعاءات الوظائف. خلاف ذلك
يتم ترك أمر التقييم غير محدد ، كما هو الحال في المعيار C. افتراضات إلى لا.

- مجلة - تعطيل
لا تقم بإخراج مجلة للجلسة الحالية. ارى -مجلة-تمكين.

-مجلة-تمكين
تشغيل افتراضيًا ، لتفريغ دفتر يومية لجميع الإجراءات التي تم تنفيذها أثناء التيار
جلسة Frama-C على شكل نص أكمل يمكن إعادة تشغيله به -حمل-
سيناريو. يمكن تعيين اسم البرنامج النصي بامتداد -اسم المجلة الخيار.

-اسم المجلة الاسم
عيّن اسم ملف المجلة (بدون امتداد م. L. تمديد). افتراضات إلى
Frama_c_journal.

-تهيئة-الحشو-المحليين
يؤدي التهيئة الضمنية للسكان المحليين إلى تعيين بتات الحشو إلى 0. إذا كانت خاطئة ، فإن بتات الحشو
تُترك بدون تهيئة (افتراضيًا إلى نعم).

[-لا] -التعليقات-المحافظة
يحاول الاحتفاظ بالتعليقات عند طباعة كود المصدر بشكل جيد (الافتراضي هو لا).

[-لا] -صيانة-التبديل
متى -تبسيط- cfg تم تعيينه ، يحتفظ ببيانات التبديل. افتراضات إلى لا.

- حفظ - وظائف - غير مستخدمة - محددة
يرى -إزالة-الوظائف-المحددة-غير المستخدمة

[-لا] - دخول
يشير إلى أنه يتم استدعاء نقطة الدخول أثناء تنفيذ البرنامج. هذا يعني في
خاصة أن المتغيرات العالمية لا يمكن افتراض أن لها قيمها الأولية.
الافتراضي هو -لا دخول ليب: نقطة الدخول هي أيضًا نقطة البداية لـ
البرنامج والكرة الأرضية لها قيمتها الأولية.

-حمل ملف
تحميل الحالة (المحفوظة مسبقًا) المضمنة في ملف.

-حمل الوحدة m1 [، m2 [...، mn]]
يقوم بتحميل وحدات ocaml من خلال . يجب أن تكون هذه الوحدات .cmxsملفات
إصدار الكود الأصلي لـ Frama-c و .cmoor.cmaملفات إصدار البايت كود (انظر
قسم Dynlink في دليل Ocaml لمزيد من المعلومات). جميع الوحدات التي هي
الموجودة في مسارات بحث البرنامج المساعد يتم تحميلها تلقائيًا.

-تحميل- النصي s1 [، s2، [...، sn]]
يقوم بتحميل البرامج النصية ocaml من خلال . يجب أن تكون البرامج النصية م. L.الملفات. أنهم
يجب أن يكون مترجمًا بالاعتماد فقط على مكتبة Ocaml القياسية وواجهة برمجة تطبيقات Frama-C. لو
هناك حاجة إلى بعض خطوات التجميع المخصصة ، قم بتجميعها خارج Frama-C واستخدامها
-حمل الوحدة بدلا من ذلك.

-ماشديب آلة
يستخدم آلة مثل التكوين الحالي المعتمد على الجهاز (حجم مختلف
أنواع الأعداد الصحيحة ، والهبات ، ...). قائمة الأجهزة المدعومة حاليًا هي
متوفر من خلال -ماشديب مساعدة اختيار. الافتراضي هو x86_32

-الأساسية f
باكجات f كنقطة دخول للتحليل. افتراضيات على "main". افتراضيا ، هو
تعتبر نقطة انطلاق البرنامج قيد التحليل. يستخدم -دخول الكتاب المقدس if f
من المفترض أن يتم استدعاؤه في منتصف عملية الإعدام.

- مبهم
يطبع نسخة مبهمة من الكود (حيث يتم استبدال المعرفات الأصلية
من قبل واحد لا معنى له) والمخارج. جدول المطابقة بين الاصل والجديد
يتم الاحتفاظ بالرموز في بداية النتيجة.

- كود ملف
يعيد توجيه التعليمات البرمجية المطبوعة إلى ملف بدلاً من الإخراج القياسي.

[-لا] -اسم -orig
أثناء مرحلة التطبيع ، قد تتم إعادة تسمية بعض المتغيرات عندما تكون مختلفة
متغير يحمل نفس الاسم يمكن أن يتعايش (على سبيل المثال ، متغير عالمي ومتغير رسمي
معامل). عند تشغيل هذا الخيار ، تتم طباعة رسالة في كل مرة يحدث ذلك.
افتراضات إلى لا.

[-لا] -حذر-وقع-محبط
إنشاء إنذارات عندما تتجاوز التنبيهات الموقعة نطاق الوجهة (الافتراضي إلى
ليس).

[-لا] - تحذير - تجاوز - موقع
إنشاء إنذارات للعمليات الموقعة التي تجاوزت (افتراضيًا إلى نعم).

[-لا] - تحذير - بدون توقيع - معطل
إنشاء إنذارات عندما يتجاوز البث غير الموقعة النطاق الوجهة (الافتراضي
لا).

[-لا] - تحذير - تجاوز السعة غير الموقعة
إنشاء إنذارات للعمليات غير الموقعة التي تجاوزت (افتراضيًا إلى لا).

[-لا] -pp-annot
التعليقات التوضيحية قبل المعالجة. هذا ممكن في الوقت الحالي فقط عند استخدام gcc (أو GNU
CPP) ما قبل المعالج. الإعداد الافتراضي هو عدم المعالجة المسبقة للتعليقات التوضيحية.

[-لا] -طباعة
جميلة تطبع الكود المصدري كما تم تطبيعه بواسطة CIL (الافتراضي إلى لا).

-طباعة- libpath
إخراج الدليل حيث تم تثبيت مكتبة نواة Frama-C

-طباعة المسار
الاسم المستعار لـ -طباعة-مسار-المشاركة

-طباعة-مسار البرنامج المساعد
يخرج الدليل الذي يبحث فيه Frama-C عن مكوناته الإضافية (يمكن تجاوزه بواسطة ملف
FRAMAC_PLUGIN متغير و -إضافة المسار خيار)

-طباعة-مسار-المشاركة
يخرج الدليل حيث يقوم Frama-C بتخزين بياناته (يمكن تجاوزه بواسطة ملف
FRAMAC_SHARE متغير)

-إزالة-الوظائف-المحددة-غير المستخدمة
يحتفظ بالنماذج الأولية للوظائف التي لها مواصفات ACSL ولكنها غير مستخدمة في
الشفرة. هذا هو الافتراضي. الوظائف التي لها السمة FRAMAC_BUILTIN انهم دائما
أبقى.

- صفائف آمنة
بالنسبة للصفائف أو المصفوفات متعددة الأبعاد التي هي حقول داخل البنيات ، يفترض ذلك
يجب أن تكون جميع عمليات الوصول مقيدة (يتم تعيينها افتراضيًا). الخيار المعاكس -غير آمن-
المصفوفات

-حفظ ملف
يحفظ حالة Frama-C في ملف بعد إجراء التحليلات.

[-لا] -تبسيط- cfg
يزيل الكسر والمتابعة والتبديل البيان قبل التحليلات. افتراضات إلى لا.

-من ثم يسمح للشخص بتكوين التحليلات: سيحدث التشغيل الأول لـ Frama-C مع الخيارات
قبل -من ثم وسيتم إجراء تشغيل ثان مع الخيارات بعد ذلك -من ثم على
المشروع الحالي من التشغيل الأول.

-ثم على PRJ
على غرار -من ثم فيما عدا أنه يتم تنفيذ التشغيل الثاني في المشروع PRJ إذا لم يكن هناك مثل هذا
المشروع موجود ، يخرج Frama-C مع وجود خطأ.

-زمن ملف
لإلحاق وقت المستخدم والتاريخ في المعطى ملف عندما يخرج Frama-C.

- نوع
يفرض فحص نوع الملفات المصدر. هذا الخيار مناسب فقط إذا لم يكن هناك المزيد
التحليل مطلوب (حيث سيحدث التحقق من الطباعة بشكل ضمني قبل التحليل
إطلاق).

-وليفل n
حلقات فتح نحويًا n مرات قبل التحليل. هذا يمكن أن يكون مكلفا جدا
وبعض المكونات الإضافية (مثل تحليل القيمة) توفر طرقًا أكثر فاعلية للأداء
نفس الشيء. انظر كتيبات كل منهم لمزيد من المعلومات. هذا يمكن أيضا
يتم تنشيطه على أساس كل حلقة عبر حلقة براجما انبسط التوجيه. أ
قيمة سالبة لـ n سوف تمنع مثل هذه البراغمات.

[-لا] -يونيكود
إخراج صيغ ACSL بأحرف utf8. هذا هو الافتراضي. عندما تعطى ال
-لا-يونيكود الخيار ، سيستخدم Frama-C إصدار ASCII بدلاً من ذلك. انظر دليل ACSL
للمراسلات.

- المصفوفات غير الآمنة
انظر تعريف - صفائف آمنة

[-لا] - وصول غير محدد
يتحقق من أن عمليات الوصول للقراءة / الكتابة تحدث بترتيب غير محدد (وفقًا لـ C
المفهوم القياسي لنقطة التسلسل) يتم تنفيذه في مواقع منفصلة. مع
-لا- وصول غير محدد، يفترض أن هذا هو الحال دائمًا (هذا هو الوضع الافتراضي).

-الإصدار
لإخراج سلسلة إصدار Frama-C

- تحذير - عشري - تعويم
يحذر عندما لا يمكن تمثيل ثابت الفاصلة العائمة بالضبط (مثل 0.1).
يمكن أن تكون واحدة من لا شيء, مرةالطرق أو من جميع

[-لا] -حذر-استدعى-غير معلن
يحذر عند استدعاء وظيفة قبل التصريح عنها (يتم تعيينها افتراضيًا).
فراما سي

الإضافات محدد الخيارات

لكل المساعد، الامر

فراما ج -المساعد-مساعدة

سيعطي قائمة بالخيارات الخاصة بالمكوِّن الإضافي.

EXIT الوضع

0 التنفيذ الناجح

1 إدخال مستخدم غير صالح

2 مقاطعة المستخدم (القتل أو ما يعادله)

3 ميزة غير مطبقة

4 5 6 خطأ داخلي

125 خطأ غير معروف

يمكن اعتبار حالة الخروج الأكبر من 2 بمثابة خطأ (أو طلب ميزة للحالة
من حالة الخروج 3) ويمكن الإبلاغ عنها على Frama-C's BTS (انظر أدناه).

البيئة المتغيرات

من الممكن التحكم في الأماكن التي يبحث فيها Frama-C عن ملفاته من خلال ملف
المتغيرات التالية.

FRAMAC_LIB
الدليل حيث يتم تثبيت واجهات kernel المترجمة

FRAMAC_PLUGIN
الدليل حيث يمكن لـ Frama-C العثور على المكونات الإضافية القياسية. إذا كنت ترغب في الحصول على ملحقات
في عدة أماكن ، استخدم -إضافة المسار بدلا من ذلك.

FRAMAC_SHARE
الدليل حيث تم تثبيت بيانات Frama-C.

استخدم frama-c.byte عبر الإنترنت باستخدام خدمات onworks.net