اين ابزار یک نرم افزار جهت تست و بررسی برنامه های تولید شده در زبان C است . مواردي كه در اين مقاله مورد بحث و بررسي قرار خواهند گرفت عبارتند از :
آموزش نصب Frama-C در Ubuntu :
اين ابزار روي تمام نسخه هاي ubuntu نصب مي شود. يكي از راههاي نصب اين ابزار به صورت زير است :
1- ترمينال را باز كنيد.
2- ابتدا دستور sudo apt-get update –y را وارد نماييد.
3- سپس دستور sudo apt-get install -y frama-c را وارد كنيد تا فراماسي نصب شود.
آموزش باز كردن ابزار Frama-C در Ubuntu :
1- ابتدا ترمينال را باز كنيد .
2- دستور frama-c-gui را وارد نماييد. ابزار فراماسي باز مي شود. (هر بار كه مي خواهيد اين ابزار را باز كنيد از اين دستور استفاده نماييد).
آموزش باز كردن برنامه در Frama-C :
از منوي file گزينه source file را انتخاب كنيد و در پنجره اي كه ظاهر مي شود برنامه خود (يك برنامه به زبان C) را انتخاب كنيد و روي دكمه add كليك نماييد و OK را بزنيد. در صورتي كه برنامه خطايي نداشته باشد در اين ابزار باز مي شود.
یک گراف اجرای برنامه را به حالت های مختلف نمایش می دهد.
1- از منوي analyses گزينه show call graph را انتخاب نماييد. با توجه به برنامه شما گراف نمايش داده مي شود. (در پنجره نمايش گراف، سه دكمه global , Tree, both را مشاهده مي كنيد كه حالتهاي مختلف نمايش است.)
جهت به دست آوردن ورودی ها و خروجی از هر یک از functionهای برنامه استفاده مي شود.
1- به منو Analysesرفته سپس بر روی Analysesکلیک کنيد.
2- از منوی سمت چپ inout را انتخاب كنيد.
3- مقادیر out, input, inout را انتخاب کرده و بر روي Execute كليك كنيد.
4- نتیجه در تب console در پايين صفحه به نمایش در خواهد آمد. نتايج به دست آمده در اين تب راجع به ورودي ها و خروجي هاي برنامه است.
نتايج اعمال اين دستور ، اطلاعاتی نظیر تعداد if, loop, function call,exit point و ... است .
1- ابتدا دستور زير را در ترمینال وارد كنيد. (بجاي program.c نام برنامه خود را وارد كنيد ).
frama-c program.c -metrics
2- متریک های استفاده شده در برنامه مطابق شكل زير به دست می آید.
3- براي تبديل اين اطلاعات به فايل txt دستور زير را در ترمينال وارد نماييد :
Frama-c program.c -metrics > program.txt
بجاي program.c نام برنامه خود را واردكنيد.
براي مشاهده وابستگی های داده ای و كنترلي دستورات نسبت به هم از این گراف استفاده مي شود.
1- ابتدا دستور زير را در ترمينال وارد نماييد :
frama-c -pdg -pdg-dot graph -pdg-print program.c > program.dot
1- با وارد كردن اين دستور ، اطلاعات به دست آمده از PDG در فایل dot ذخیره مي گردد. (بجاي program.c نام برنامه خود را واردكنيد و در بخش بعد به جاي program.dot اسمي كه مي خواهيد فايل dot با آن ذخيره شود را وارد نماييد به همراه پسوند dot ).با توجه به برنامه انتخاب شده هشت فايل dot ايجاد شد (فايل هاي مشخص شده در كادر قرمز رنگ).
2- حال براي اينكه اطلاعات موجود در فايل dotقابل مشاهده باشد و به شكل گراف نمايش داده شود با استفاده از دستور زير تمام فايلهاي dot را به pdf تبديل كنيد. (بجاي program.main.dot نام تك تك فايل هاي dot را وارد نماييد برنامه خود را واردكنيد و در بخش بعدي به جاي main.pdf ، عنواني كه مي خواهيد فايل pdf با آن ذخيره شود را با پسوند pdf وارد نماييد).
dot -Tpdf program.main.dot > main.pdf
نكته : به ازاي تك تك اين دستورات فايل pdf ايجاد مي شود كه شامل گراف هاي برنامه است به عنوان نمونه گراف main برنامه انتخابي به صورت زير است :
با استفاده از اين دستور ،دستوراتی که روی دستورات دیگر تاثیر میگذارند را میتوان مشخص کرده كه خروجي به صورت گراف قابل مشاهده است.
1- ابتدا از طریق ترمینال دستور زیر را وارد نماييد تا اطلاعات در فایل dotذخیره گردد.
frama-c program.c -dot-postdom main
(بجاي program.c نام برنامه خود را واردكنيد ).
2- سپس فايلهاي dot را به PDF تبدیل کنيد.
يك نمونه از گراف ايجاد شده به ازاي تابع main :
نكته : به دليل حساس بودن اين ابزار به دستورات printf و scanf ، به جاي printf از return و به جاي scanf مقادير (7,6,9) وارد شده است تا خروجي هاي گراف به درستي به دست آيد.
با انتخاب یک متغیر از متغير هاي موجود در برنامه میتوان دستوراتی که روی آن متغیر تاثیر مستقیم و یا غیر مستقیم دارند را شناسایی كرد.
1- براي اين كار در ترمینال دستور زیر را وارد نماييد .
frama-c -slicing-wr temp program.c -slice-print > slice.txt
با استفاده از اين دستور نتايح به دست آمده در يك فايل txtذخيره مي شود. (بجاي program.c نام برنامه خود را واردكنيد ).
متغير temp كه در برنامه وجود دارد ، اسلايس در نظر گرفته شده است.
با استفاده از اين دستور مي توان ورودی و خروجی هاي برنامه را به دست آورد.
1- در محيط فراماسي و بعد از باز كردن برنامه،به منوي analyses رفته و بر روی Analysesکلیک کنيد .
2- از منوی سمت چپ user را انتخاب کرده و تيك users را زده، سپس روی execute کلیک كنيدتا نتيجه در کنسول تولید شود.
3- تب console در پايين صفحه نتايج به نمایش در خواهد آمد.
براي اعمال اين مشخصه ، دستور زير را در ترمينال وارد نماييد.(بجاي program.c نام برنامه خود را واردكنيد).
frama-c -wp program.c
اين دستور جهت تحليل روي مقادير تمام متغيرهاي موجود در برنامه مورد استفاده قرار مي گيرد و نتايج خروجي در تب Value ابزار Frama-c در پايين صفحه قابل مشاهده است. نتايج تب Console هم در ادامه قرار گرفته است.
1- در محيط فراماسي و بعد از باز كردن برنامه،به منوي analyses رفته و بر روی Analysesکلیک کنيد .
2- از منوی سمت چپ value analysis را انتخاب کرده و تيك val را بزنيد سپس بر روی execute کلیک می کنید .
3- حال روي هر متغيري در برنامه قرار بگيريد در تب value محدوده مقاديري كه اين متغير مي تواند بگيرد نمايش داده مي شود .(اين مقادير شامل مقادير اوليه تا مقادير نهايي مي باشد). در شكل هاي زير، نتيجه تحليل روي متغيرrem نشان داده شده است.
4- اطلاعات موجود در تب console در پايين صفحه به نمایش آمده است.
جهت تحليل وقوع يك متغير در طول برنامه مورد استفاده قرار مي گيرد. و راجع به متغير انتخاب شده اطلاعاتي را در تب information نمايش مي دهد.
1- در محيط فراماسي و بعد از باز كردن برنامه،به منوي analyses رفته و بر روی Analysesکلیک کنيد .
2- از منوی سمت چپ occurrence را انتخاب کرده و تيك occurrence را بزنيد سپس بر روی execute کلیک می کنید .
3- سپس متغير مورد نظر در برنامه را انتخاب كنيد. راست كليك كرده و occurrence را انتخاب نماييد تا تحليل روي متغير آغاز شود و تمام نقاطي كه نام اين متغير وجود دارد هايلايت مي شود. سپس در تب information اطلاعاتي راجع به متغير اعم از محلي يا سراسري بودن، در كدام تابع استفاده شده و .... نمايش داده مي شود. در ادامه عكسهاي مربوط به اين دستور را مشاهده مي كنيد.
4- بخشي از اطلاعات موجود در تب console در پايين صفحه به نمایش آمده است.
دستور Impact
اين تحليل روي تاثيرگذاري هر يك از متغيرها در تمام نقاط برنامه بحث مي كند. با انتخاب متغير ، تاثيراتي كه روي تمام بخشهاي برنامه مي گذارد هايلايت مي شود و اطلاعاتي در تب console درج مي شود كه در ادامه مشاهده مي كنيد.
1- در محيط فراماسي و بعد از باز كردن برنامه،به منوي analyses رفته و بر روی Analysesکلیک کنيد .
2- از منوی سمت چپ impact را انتخاب کرده و سپس بر روی executeکلیک می کنید .
3- سپس با راست كليك روي متغير مربوطه گزينه impact analysis را انتخاب مي نماييم.
4- حالا برخي نتايج زير در تب console قابل مشاهده است.
در اين مقاله سعي شد بررسي اجمالي دستورات و خصيصه هاي پركاربرد ابزار Frama-C جهت استفاده دانشجويان و علاقه مندان نمايش داده شود.
