به نام خدا
توضیح کلی نرم افزار Frama-c
نرم افزار Frama-c یک نرم افزار جهت تست و بررسی برنامه های تولید شده که به زبان C می باشد و می تواند خروجی های مختلفی از جمله : Call Graph , Inout, Metrics, PDG, Post Dominator, Slicing, User, WP, Sparecode و Dependencies, Occurrence به کاربر بدهد که بوسیله این خروجی ها کاربر می تواند نسبت به عیب یابی و تست نرم افزار اقدام نماید .
طریقه نصب Frama-c
برای نصب برنامه Frama-c حتما باید سیستم عامل لینوکس داشته باشد و در اینجا ما از نسخه ubuntu استفاده می کنیم .
طبق دستور العمل سایت https://frama-c.com/install-aluminium-20160501.html به اینگونه عمل می کنیم :
If you are using Debian >= Squeeze 6.0 or Ubuntu >= Lucid Lynx 10.04 then
a Frama-C package is provided:
sudo apt-get install frama-c
or, if you don't want the Gtk-based GUI:
sudo apt-get install frama-c-base
محیط کار برنامه Frama-c
پس از نصب برنامه با جستجو نام frama-c در لیست برنامه ها باید آیکون آن پیدا شود و با کلیک بر روی آن برنامه با موفقیت باز شود که به شکل زیر خواهد بود.
برای شروع عملیات های مورد نظر ابتدا به یک برنامه C نیازمند خواهید بود. برای آموزش از یک برنامه ساده استفاده کنید زیرا برخی از ویژگی های این نرم افزار پیچیدگی بالایی پیدا خواهد کرد.
فایل مورد نیاز باید با پسوند c. باشد و فایل های cpp. را که مربوط به ++C میشود را اجرا نخواهد کرد و اگر دستورات شما در با زبان ++C نوشته شده میتوانید آن را به c. تغییر دهید اما حتما مطمئن شوید که دستورات مشترک با زبان c داشته باشید در غیر این صورت برای باز کردن فایل با خطا مواجه میشوید.
برای باز کردن فایل C بر روی منو file رفته و گزینه source file را انتخاب کرده و سپس فایل مورد نظر را یافته و انتخاب کنید.
پس از اضافه کردن فایل c به نرم افزار باید دستورات به شکل زیر نمایش داده شود. نکته:دستورات زیر مربوط به فایل c می باشد که در این تمرین قرار گرفته است و بر اساس فایل c شما دستورات متفاوت خواهد بود.
از منوی Analyses می توانیم خروجی ها مختلفی را بگیریم
گزارش call graph به نوعی یک گزارش ظاهری بوده که از طریق آن میتوانید یک گراف اجرای برنامه را به حالت های مختلف نمایش می دهد. برای تهیه یک call graph کافیست تا به منو analyses رفته و گزینه show entire callgraph را انتخاب کنید سپس باید همانند شکل زیر گرافی برای شما ظاهر شود
این گزارش جهت به دست آوردن ورودی ها و خروجی از هر یک از function های برنامه شما خواهد بود.
برای تهیه inout برنامه ابتدا به منو Analyses رفته سپس بر روی Analysesکلیک کرده و از منوی سمت چپ inout را کلیک کرده و مقادیر out, input, inout را انتخاب کرده و نتیجه در کنسول به نمایش در خواهد آمد.
در Metrics اطلاعاتی نظیر تعداد if, loop, function call,exit point و ... را به دست بیاورید.
برای تهیه Metrics ابتدا باید دستور frama-c [project.c] -metrics را در ترمینال وارد کرده و متریک های استفاده شده در برنامه به دست می آید.
در قسمت [project.c] باید نام فایل به همراه فرمت آن قرار دهید.
گراف PDG یک گراف تولید شده از وابستگی های داده ای و وابستگی اجرایی دستورات نسبت به هم تهیه می کند که با استفاده از این گراف به سادگی میتوانید دستورات را شناسایی کنید.
اطلاعات بیشتر را میتوانید در این آموزش به دست بیاورید
برای تهیه PDG ابتدا باید از طریق ترمینال اطلاعات به دست آمده از PDG را در فایل dot ذخیره کرده سپس آن را به PDF تبدیل نماییم. در ابتدا دستور زیر را اجرا کرده تا PDG را در فایل projectpdg.dot ذخیره نماید تا سپس آن را به PDF تبدیل نماییم.
1frama-c -pdg -pdg-dot graph -pdg-print project.c > projectpdg.dot
1dot -Tpdf graph.main.dot > projectpdg.pdf
postDom
با زدن دستور زیر می توان خروجی postdom را بدست می آید
در Slicing بر اساس تعیین یک متغیر میتوان دستوراتی که بر روی آن متغیر تاثیر مستقیم و یا غیر مستقیم دارند را شناسایی کنیم برای اطلاعات بیشتر میتوانید به این آدرس مراجعه کنید.
برای تهیه slicing باید در ترمینال دستور زیر را اعمال کرد. برای متغیر ptr اسلایس را در نظر گرفته ایم و در نهایت در فایل slice.txt ذخیره می کنیم. در روال برنامه ابتدا PDG را به دست آورده و سپس Slicing را آغاز کرده است.
1frama-c -slice-wr ptr project.c > slice.txt
با استفاده از Users میتوانید ورودی و خروجی ها را پیدا کنید.
برای تهیه گزارش User ابتدا به برنامه بازگشته و سپس بر روی Analysis رفته و بر روی منوی user کلیک کرده و مقدار user- را انتخاب کرده و سپس بر روی execute کلیک می کنیم تا در کنسول نتیجه تولید شود.
برای تهیه WP باید از طریق ترمینال دستور زیر را اعمال نماییم.
1frama-c -wp project.c
امروزه بررسی و رفع ایراد نرم افزار ها یکی از معضلات تیم برنامه نویسی و تست نرم افزار است که اکثرا بدون استفاده از نرم افزار یا ابزار صورت می گیرد. داشتن علم آزمون نرم افزار قطعا میتواند این چنین موانع را از میان بردارد.
قطعا امروزه برنامه نویسی با زبان های جدیدتر صورت می گیرد همچنین Frama-c یکی از چند صد نرم افزار آزمون نرم افزار بوده که با فراگرفتن دانش آزمون نرم افزار میتوانید موارد مشابه را در زبان های دیگر نیز پیاده سازی کرده و از آن در رفع ایرادات نهفته و آشکار برنامه خود استفاده کنید.
این مقاله معرفی کوتاهی از برنامه Frama-c بوده که پرکاربرد ترین گزارشات این برنامه توضیح داده شد.
برای فراگیری بیشتر علم آزمون نرم افزار میتوانید مباحث ذکر شده را مانند slicing, pdg و ... را جستجو کرده و مقالات انتشار یافته را به دست آورده و اطلاعات بیشتر کسب کنید.
