نرم افزار Frama-c یک نرم افزار جهت تست و بررسی برنامه های تولید شده در زبان C بوده که بسیاری از فعالیت ها نظیر Call Graph , Inout, Metrics, PDG, Post Dominator, Slicing, User, WP, Sparecode, Dependencies, Occurrence و بسیار ویژگی های دیگر را بررسی کرده و نتایج را به اشکال مختلف به کاربر ارائه می دهد.
نرم افزار Frama-c حتما باید در لینوکس نصب و اجرا شود برای نصب می توانید هر یک از ورژن های Ubuntu و یا Fedora استفاده کنید طریقه نصب در ادامه در Fedora29 انجام شده است و در Ubuntu دستورات نصب ممکن است متفاوت باشد.
۱- برای نصب Frama-C نیاز به مخزن RPM Fusion داریم در صورتی که این مخزن نصب نیست از طریق مراحل زیر اقدام به نصب نمایید.
۱-۱- باید ابتدا به سایت rpm fusion رفته به آدرس rpmfusion.org رفته و بر اساس معماری Fedora خود مخزن را دانلود نمایید.
۲-۱- پس از دانلود در ترمینال سیستم عامل با دستور rpm -ivh مخزن را نصب نمایید.
۲- سپس باید مخزن را آپدیت نمایید از طریق دستور dnf update میتوانید به جدید ترین پکیج ها دسترسی داشته باشید.
۳- سپس باید پکیج های مختلف شامل jcc و glibc و ++G را نصب نماییم برای نصب هر یک کافیست از دستور
dnf install [package name]
مثال :
dnf install jcc
dnf install glibc
dnf install g++
۴- در ادامه پس از نصب تمام پکیج های مورد نیاز بالا باید پکیج xkit را نصب کنید که مشابه دستورات بالا قابل انجام خواهد بود.
۵- سپس به سایت frama-c رفته به آدرس frama-c.com و نسخه frama-c را بر اساس نوع سیستم عامل و معماری آن دانلود نمایید.
۶- سپس باید فایل tar را uncompress کنید ( توضیحات بیشتر برای استفاده از دستور tar )
۷- برای بهبود GUI برنامه Frama-c باید از پکیج Bladez از طریق دستور dnf install bladez نصب کنید.
۸- داخل پوشه extract شده frama-c رفته و ترمینال را باز کرده و با دستور install/. برنامه را نصب کنید.
پس از نصب برنامه با جستجو نام frama-c در لیست برنامه ها باید آیکون آن پیدا شود و با کلیک بر روی آن برنامه با موفقیت باز شود که به شکل زیر خواهد بود.
برای استفاده از امکانات frama-c هم از طریق terminal و هم از طریق ظاهر برنامه قابل انجام هستند اما در حالت ظاهری امکان متوجه شدن برخی از قسمت ها سخت خواهد بود که با استفاده از دستورات راحتر میتوان به آنها دسترسی داشت.
برای شروع عملیات های مورد نظر ابتدا به یک برنامه C نیازمند خواهید بود. برای آموزش از یک برنامه ساده استفاده کنید زیرا برخی از ویژگی های این نرم افزار پیچیدگی بالایی پیدا خواهد کرد.
فایل مورد نیاز باید با پسوند c. باشد و فایل های cpp. را که مربوط به ++C میشود را اجرا نخواهد کرد و اگر دستورات شما در با زبان ++C نوشته شده میتوانید آن را به c. تغییر دهید اما حتما مطمئن شوید که دستورات مشترک با زبان c داشته باشید در غیر این صورت برای باز کردن فایل با خطا مواجه میشوید.
برای باز کردن فایل C بر روی منو file رفته و گزینه source file را انتخاب کرده و سپس فایل مورد نظر را یافته و انتخاب کنید.
پس از اضافه کردن فایل c به نرم افزار باید دستورات به شکل زیر نمایش داده شود. نکته:دستورات زیر مربوط به فایل c می باشد که در این تمرین قرار گرفته است و بر اساس فایل c شما دستورات متفاوت خواهد بود.
دستورات استفاده شده در این مثال در شکل زیر است
گزارش call graph به نوعی یک گزارش ظاهری بوده که از طریق آن میتوانید یک گراف اجرای برنامه را به حالت های مختلف نمایش می دهد. برای تهیه یک call graph کافیست تا به منو analyses رفته و گزینه show entire callgraph را انتخاب کنید سپس باید همانند شکل زیر گرافی برای شما ظاهر شود.
این گزارش جهت به دست آوردن ورودی ها و خروجی از هر یک از function های برنامه شما خواهد بود.
برای تهیه inout برنامه ابتدا به منو Analyses رفته سپس بر روی Analysesکلیک کرده و از منوی سمت چپ inout را کلیک کرده و مقادیر out, input, inout را انتخاب کرده و نتیجه در کنسول به نمایش در خواهد آمد.
به صورت خلاصه از نتایج به دست آمده میتوان گفت در ابتدا بر اساس function های استفاده شده شروع کرده سپس هر یک را به ترتیب اجرا کرده و در قسمت پایانی نتیجه میتوان به inputهای main و outputهای main رسید و inputهای این برنامه میتوان به موارد زیر اشاره کرد:
Operational inputs:
__fc_stdin; __fc_stdout; __fc_heap_status; S___fc_stdin[0];
Operational inputs on termination:
__fc_stdin; __fc_stdout; __fc_heap_status; S___fc_stdin[0];
outputs:
ptr; limit; i; sum; __retres
در Metrics اطلاعاتی نظیر تعداد if, loop, function call,exit point و ... را به دست بیاورید.
برای تهیه Metrics ابتدا باید دستور frama-c [project.c] -metrics را در ترمینال وارد کرده و متریک های استفاده شده در برنامه به دست می آید.
در قسمت [project.c] باید نام فایل به همراه فرمت آن قرار دهید.
[kernel] Parsing project.c (with preprocessing)
[metrics] Defined functions (1)
=====================
main (0 call);
Undefined functions (0)
=======================
'Extern' global variables (0)
=============================
Potential entry points (1)
==========================
main;
Global metrics
==============
Sloc = 31
Decision point = 3
Global variables = 0
If = 3
Loop = 3
Goto = 0
Assignment = 10
Exit point = 1
Function = 1
Function call = 9
Pointer dereferencing = 2
Cyclomatic complexity = 4
گراف PDG یک گراف تولید شده از وابستگی های داده ای و وابستگی اجرایی دستورات نسبت به هم تهیه می کند که با استفاده از این گراف به سادگی میتوانید دستورات را شناسایی کنید.
اطلاعات بیشتر را میتوانید در این آموزش به دست بیاورید
برای تهیه PDG ابتدا باید از طریق ترمینال اطلاعات به دست آمده از PDG را در فایل dot ذخیره کرده سپس آن را به PDF تبدیل نماییم. در ابتدا دستور زیر را اجرا کرده تا PDG را در فایل projectpdg.dot ذخیره نماید تا سپس آن را به PDF تبدیل نماییم.
frama-c -pdg -pdg-dot graph -pdg-print project.c > projectpdg.dot
dot -Tpdf graph.main.dot > projectpdg.pdf
تهیه Post Dominator
در Post Dominator دستوراتی که بر روی دستورات دیگر تاثیر میگذارد را میتوان مشخص کرده و به شکل یک گراف رسیدن به مقصد به نمایش در خواهد آورد. برای اطلاعات بیشتر میتوانید به این آدرس مراجعه کنید
برای تهیه Post dominator باید از طریق ترمینال دستور زیر را نوشته تا ابتدا گزارش را در فایل dot ذخیره کرد تا سپس آن را به PDF تبدیل کرد اما نکته ای که وجود دارد وجود printf و scanf در دستورات است که باید این دستورات را از طریق مقدار دهی داخلی مقدار داد و از return استفاده کرد تا گراف post dominator ایجاد شود.
frama-c project.c -dot-postdom main
dot -Tpdf main.main.dot > postdom.pdf
در Slicing بر اساس تعیین یک متغیر میتوان دستوراتی که بر روی آن متغیر تاثیر مستقیم و یا غیر مستقیم دارند را شناسایی کنیم برای اطلاعات بیشتر میتوانید به این آدرس مراجعه کنید.
برای تهیه slicing باید در ترمینال دستور زیر را اعمال کرد. برای متغیر ptr اسلایس را در نظر گرفته ایم و در نهایت در فایل slice.txt ذخیره می کنیم. در روال برنامه ابتدا PDG را به دست آورده و سپس Slicing را آغاز کرده است.
frama-c -slice-wr ptr project.c > slice.txt
با استفاده از Users میتوانید ورودی و خروجی ها را پیدا کنید.
برای تهیه گزارش User ابتدا به برنامه بازگشته و سپس بر روی Analysis رفته و بر روی منوی user کلیک کرده و مقدار user- را انتخاب کرده و سپس بر روی execute کلیک می کنیم تا در کنسول نتیجه تولید شود.
برای تهیه WP باید از طریق ترمینال دستور زیر را اعمال نماییم.
frama-c -wp project.c
از طریق Sparecode و دستور زیر متغیر های گلوبال اضافی را حذف کردیم.
frama-c -sparecode-rm-unused-globals project.c > sparecode.txt
برای شناسایی Dependency های متغیر ها از طریق دستور زیر مقدار dependency ها در فایلی ذخیره می کنیم.
frama-c -deps project.c -deps-print > deps.txt
با استفاده از این گزارش میتوانیم تعداد استفاده شدن هر متغیر را پیدا کرد برای اجرای این گزارش از دستور زیر استفاده می کنیم.
Frama-c -occurrence project.c > occurrence.txt
امروزه بررسی و رفع ایراد نرم افزار ها یکی از معضلات تیم برنامه نویسی و تست نرم افزار است که اکثرا بدون استفاده از نرم افزار یا ابزار صورت می گیرد. داشتن علم آزمون نرم افزار قطعا میتواند این چنین موانع را از میان بردارد.
قطعا امروزه برنامه نویسی با زبان های جدیدتر صورت می گیرد همچنین Frama-c یکی از چند صد نرم افزار آزمون نرم افزار بوده که با فراگرفتن دانش آزمون نرم افزار میتوانید موارد مشابه را در زبان های دیگر نیز پیاده سازی کرده و از آن در رفع ایرادات نهفته و آشکار برنامه خود استفاده کنید.
این مقاله معرفی کوتاهی از برنامه Frama-c بوده که پرکاربرد ترین گزارشات این برنامه توضیح داده شد.
برای فراگیری بیشتر علم آزمون نرم افزار میتوانید مباحث ذکر شده را مانند slicing, pdg و ... را جستجو کرده و مقالات انتشار یافته را به دست آورده و اطلاعات بیشتر کسب کنید.
