https://virgool.ir/feed/@taraizadifa2026-11-12 03:25:16https://virgool.ir/images/default-avatar.jpghttps://virgool.ir/@taraizadihttps://virgool.ir/@taraizadi/آموزش-frama-c-t8vwtpz7al5lاين ابزار یک نرم افزار جهت تست و بررسی برنامه های تولید شده در زبان C است . مواردي كه در اين مقاله مورد بحث و بررسي قرار خواهند گرفت عبارتند از :call graphInoutMetricsPdgPost dominatorsSlicingUsersWPValue analysisOccurrenceImpactآموزش نصب 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آموزش باز كردن برنامه در Frama-C :از منوي file گزينه source file را انتخاب كنيد و در پنجره اي كه ظاهر مي شود برنامه خود (يك برنامه به زبان C) را انتخاب كنيد و روي دكمه add كليك نماييد و OK را بزنيد. در صورتي كه برنامه خطايي نداشته باشد در اين ابزار باز مي شود. Frama-cبرنامه باز شده در دستور call graphیک گراف اجرای برنامه را به حالت های مختلف نمایش می دهد.1- از منوي analyses گزينه show call graph را انتخاب نماييد. با توجه به برنامه شما گراف نمايش داده مي شود. (در پنجره نمايش گراف، سه دكمه global , Tree, both را مشاهده مي كنيد كه حالتهاي مختلف نمايش است.) call graphدستور inoutجهت به دست آوردن ورودی ها و خروجی از هر یک از functionهای برنامه استفاده مي شود.1- به منو Analysesرفته سپس بر روی Analysesکلیک کنيد.2- از منوی سمت چپ inout را انتخاب كنيد.3- مقادیر out, input, inout را انتخاب کرده و بر روي Execute كليك كنيد.Inout4- نتیجه در تب console در پايين صفحه به نمایش در خواهد آمد. نتايج به دست آمده در اين تب راجع به ورودي ها و خروجي هاي برنامه است.بخشي از نتايج Inout در تب كنسولدستور metricsنتايج اعمال اين دستور ، اطلاعاتی نظیر تعداد if, loop, function call,exit point و ... است .1- ابتدا دستور زير را در ترمینال وارد كنيد. (بجاي program.c نام برنامه خود را وارد كنيد ).frama-c program.c -metrics2- متریک های استفاده شده در برنامه مطابق شكل زير به دست می آید.خروجي دستور metrics در ترمينال3- براي تبديل اين اطلاعات به فايل txt دستور زير را در ترمينال وارد نماييد :Frama-c program.c -metrics > program.txtبجاي program.c نام برنامه خود را واردكنيد.تبديل خروجي metrics به فايل txtدستور pdgبراي مشاهده وابستگی های داده ای و كنترلي دستورات نسبت به هم از این گراف استفاده مي شود.1- ابتدا دستور زير را در ترمينال وارد نماييد :frama-c -pdg -pdg-dot graph -pdg-print program.c > program.dot1- با وارد كردن اين دستور ، اطلاعات به دست آمده از PDG در فایل dot ذخیره مي گردد. (بجاي program.c نام برنامه خود را واردكنيد و در بخش بعد به جاي program.dot اسمي كه مي خواهيد فايل dot با آن ذخيره شود را وارد نماييد به همراه پسوند dot ).با توجه به برنامه انتخاب شده هشت فايل dot ايجاد شد (فايل هاي مشخص شده در كادر قرمز رنگ).خروجي دستور اول و ايجاد فايل هاي dot2- حال براي اينكه اطلاعات موجود در فايل dotقابل مشاهده باشد و به شكل گراف نمايش داده شود با استفاده از دستور زير تمام فايلهاي dot را به pdf تبديل كنيد. (بجاي program.main.dot نام تك تك فايل هاي dot را وارد نماييد برنامه خود را واردكنيد و در بخش بعدي به جاي main.pdf ، عنواني كه مي خواهيد فايل pdf با آن ذخيره شود را با پسوند pdf وارد نماييد).dot -Tpdf program.main.dot > main.pdfتبديل فايلهاي dot به pdf در pdgنكته : به ازاي تك تك اين دستورات فايل pdf ايجاد مي شود كه شامل گراف هاي برنامه است به عنوان نمونه گراف main برنامه انتخابي به صورت زير است :گراف pdg تابع main دستور post dominatorsبا استفاده از اين دستور ،دستوراتی که روی دستورات دیگر تاثیر میگذارند را میتوان مشخص کرده كه خروجي به صورت گراف قابل مشاهده است.1- ابتدا از طریق ترمینال دستور زیر را وارد نماييد تا اطلاعات در فایل dotذخیره گردد.frama-c program.c -dot-postdom main(بجاي program.c نام برنامه خود را واردكنيد ).خروجي دستور post dominators2- سپس فايلهاي dot را به PDF تبدیل کنيد.تبديل فايل هاي dot به pdfيك نمونه از گراف ايجاد شده به ازاي تابع main :نكته : به دليل حساس بودن اين ابزار به دستورات printf و scanf ، به جاي printf از return و به جاي scanf مقادير (7,6,9) وارد شده است تا خروجي هاي گراف به درستي به دست آيد.دستور Slicingبا انتخاب یک متغیر از متغير هاي موجود در برنامه میتوان دستوراتی که روی آن متغیر تاثیر مستقیم و یا غیر مستقیم دارند را شناسایی كرد.1- براي اين كار در ترمینال دستور زیر را وارد نماييد .frama-c -slicing-wr temp program.c -slice-print > slice.txtدستورslicing در ترمينالبا استفاده از اين دستور نتايح به دست آمده در يك فايل txtذخيره مي شود. (بجاي program.c نام برنامه خود را واردكنيد ).متغير temp كه در برنامه وجود دارد ، اسلايس در نظر گرفته شده است.دستور Users با استفاده از اين دستور مي توان ورودی و خروجی هاي برنامه را به دست آورد.1- در محيط فراماسي و بعد از باز كردن برنامه،به منوي analyses رفته و بر روی Analysesکلیک کنيد .2- از منوی سمت چپ user را انتخاب کرده و تيك users را زده، سپس روی execute کلیک كنيدتا نتيجه در کنسول تولید شود.users3- تب console در پايين صفحه نتايج به نمایش در خواهد آمد.بخشي از خروجي دستور users در تب كنسولدستور WPبراي اعمال اين مشخصه ، دستور زير را در ترمينال وارد نماييد.(بجاي program.c نام برنامه خود را واردكنيد). frama-c -wp program.cخروجي دستور WP در ترمينالدستور Value Analysisاين دستور جهت تحليل روي مقادير تمام متغيرهاي موجود در برنامه مورد استفاده قرار مي گيرد و نتايج خروجي در تب Value ابزار Frama-c در پايين صفحه قابل مشاهده است. نتايج تب Console هم در ادامه قرار گرفته است.1- در محيط فراماسي و بعد از باز كردن برنامه،به منوي analyses رفته و بر روی Analysesکلیک کنيد .2- از منوی سمت چپ value analysis را انتخاب کرده و تيك val را بزنيد سپس بر روی execute کلیک می کنید . انتخاب دستور Value َAnalysis3- حال روي هر متغيري در برنامه قرار بگيريد در تب value محدوده مقاديري كه اين متغير مي تواند بگيرد نمايش داده مي شود .(اين مقادير شامل مقادير اوليه تا مقادير نهايي مي باشد). در شكل هاي زير، نتيجه تحليل روي متغيرrem نشان داده شده است.4- اطلاعات موجود در تب console در پايين صفحه به نمایش آمده است.نتايج به دست آمده از تحليل متغير rem در تب كنسولدستور Occurrenceجهت تحليل وقوع يك متغير در طول برنامه مورد استفاده قرار مي گيرد. و راجع به متغير انتخاب شده اطلاعاتي را در تب information نمايش مي دهد.1- در محيط فراماسي و بعد از باز كردن برنامه،به منوي analyses رفته و بر روی Analysesکلیک کنيد .2- از منوی سمت چپ occurrence را انتخاب کرده و تيك occurrence را بزنيد سپس بر روی execute کلیک می کنید .انتخاب دستور occurrence3- سپس متغير مورد نظر در برنامه را انتخاب كنيد. راست كليك كرده و occurrence را انتخاب نماييد تا تحليل روي متغير آغاز شود و تمام نقاطي كه نام اين متغير وجود دارد هايلايت مي شود. سپس در تب information اطلاعاتي راجع به متغير اعم از محلي يا سراسري بودن، در كدام تابع استفاده شده و .... نمايش داده مي شود. در ادامه عكسهاي مربوط به اين دستور را مشاهده مي كنيد.انتخاب متغيرخروجي occurrence4- بخشي از اطلاعات موجود در تب console در پايين صفحه به نمایش آمده است.خروجي دستور occurrence در تب كنسولدستور Impactاين تحليل روي تاثيرگذاري هر يك از متغيرها در تمام نقاط برنامه بحث مي كند. با انتخاب متغير ، تاثيراتي كه روي تمام بخشهاي برنامه مي گذارد هايلايت مي شود و اطلاعاتي در تب console درج مي شود كه در ادامه مشاهده مي كنيد.1- در محيط فراماسي و بعد از باز كردن برنامه،به منوي analyses رفته و بر روی Analysesکلیک کنيد .2- از منوی سمت چپ impact را انتخاب کرده و سپس بر روی executeکلیک می کنید .انتخاب دستور Impact3- سپس با راست كليك روي متغير مربوطه گزينه impact analysis را انتخاب مي نماييم.انتخاب متغير و خروجي تب information4- حالا برخي نتايج زير در تب console قابل مشاهده است.خروجي دستور Impact در تب كنسولدر اين مقاله سعي شد بررسي اجمالي دستورات و خصيصه هاي پركاربرد ابزار Frama-C جهت استفاده دانشجويان و علاقه مندان نمايش داده شود. taraizaditaraizadiWed, 12 Feb 2020 23:26:30 +0330