با استفاده از دو دستور زیر ابزار frama-c نصب می کنیم .
Sudo apt-get update -y
Sudo apt-get install –yframa-c
برای اجرای محیط CLI و محیط گرافیکی نرم افزار به ترتیب دستورات زیر اجرا می شود :
Frama-c
Frama-c-gui
برای مشاهده پلاگین های موجود دستور زیر اجرا می شود :
Frama-c-plugin
ابتدا پروژه search.cکه یک پروژه دلخواه می باشد در قسمت new projectدر projectبه صورت زیر اجرا می کنیم.
پروژه search.c را اضافه خواهیم کرد.
بر روی قسمت Analysesمی رویم حال قسمت های خواسته شده در تمرین را طی مراحلی انجام می دهیم.
برای مشاهده ی Callgraphگزینه ی Analysesانتخاب کرده، سپس گزینه ی Show callgraphرا انتخاب می نماییم.Callgraphها بصورت های Both)،Tree،Global) نمایش داده خواهد شد .
? Global:
? Tree:
? Both:
در منوی Analysesبر روی Analysesکلیک میکنیم و از قسمت سمت چپ برنامه باز شده Inoutرا انتخاب کرده و سپس در قسمت سمت راست همانند شکل زیر موارد مورد نظر راانتخاب می کنیم.
سپس بر روی Executeکلیک کرده و به قسمت Consoleمی رویم در این قسمت موارد علامت زده راهمانند شکل زیر مشاهده می کنیم.
در Terminalبا دستور شکل زیر می توان این مورد را بدست اورد .
همچنین مانند شکل زیر میتوان خروجی این مرحله را در یک فایل txtذخیره نماییم .که در قسمتtamrin1 پوشه metricذخیره کرده ایم. در این شکل اعلام میشود که هر متغیر یا تابع چند بار فراخوانی شدهاست.
درTerminalو زدن commandشکل زیر یک فایل dotتولید میشود.
حالا برای تبدیل این فایل به pdfمانند شکل زیر عمل میکنیم.
آنگاه به شکل زیر می رسیم.
در Terminalدستور شکل زیر را اعمال میکنیم، دستوری که با فلش قرمز مشخص شده است slicing در برنامه انجام می شود .سپس با دستوری که با فلش سبز نشان داده شده است خروجی در یک فایل txt ذخیره می شود .
از قسمت Analysisمانند شکل زیر عمل میکنیم و سپس Executeکلیک میکنیم.
در Terminalدستور شکل زیر را اعمال مینماییم.
در این قسمت یک مشکل وجود دارد این ابزار با scanfو printfمشکل دارد ما با گرفتنورودی از خود برنامه و تبدیل printfبه returnمشکل را حل کردیم. راه حل دیگر استفاده از" قبل از\است.
زمانی که فایل را به pdfتبدیل مینماییم در شکل پایین نمایش داده شده است.
حال گراف به صورت شکل زیر می باشد:
بر اساس منطق برنامه میگوییم متغیر ها در چه بازه ای هستند. با استفاده از دستور زیر اینکار را انجام می دهیم.
موارد ستفاده یک متغیر در برنامه رابیان خواهد کرد و اینکه این متغیر در برنامه به ازای ورودی هامتفاوت از چه مسیرهایی عبور می کند. به عبارتی دیگر، رخدادهایی که در برنامه برای این متغیر پیش خواهد آمد، نشان می دهد .
در برنامه متغیر tmpرا در نظر گرفتیم که در سربرگ information اطلاعات این متغیر را خواهید دید .
روی متغیر tmpراست کلیک کرده و گزینه occurrence را کلیک می کنیم .
در سه شکل زیر مسیرهایی که متغیر tmp عبور می کند را خواهید دید .
در این قسمت مقدارهای که یک متغیر در برنامه خواهد گرفت را مشخص خواهد کرد . برنامه search.c در frama-cباز می کنیم و از سربرگ Analysis قسمت Value analysis مطابق شکل انتخاب خواهیم کرد.
بر روی متغیر k کلیک تا مقادیرش را در برنامه مشاهده کنیم .
بر روی سربرگ vlue کلیک می کنیم . مقدار 5 را برای متغیر k خواهیم دید .
بر روی هر کدام از متغیرهای برنامه کلیک نماییم مقدار متغیر در دستورات مختلف خواهیم دید.
تاثیری که یک متغیر را در دستورات و عبارت برنامه مثل حلقه یwhile خواهد گذاشت را مشاهده خواهیم کرد . از منوی Analysis گزینه Impact را انتخاب خواهیم کرد .
در مثال زیر بدلیل نشان دادن کاربرد Impact از برنامه ی دیگری (برنامه غیر از search.c) که این موضوع را واضح نشان می دهد، استفاده کردم .Impact Analysis نشان می دهد در تابع main ،خط 12 (tmp = p) از کجا شروع می شود و بر کدام دستورات یا متغیرها تاثیر می گذارد و تغییر دهنده اشاره گر می باشد و تاثیرگذاری متغیر مربوطه در نقاط مختلف برنامه را نشان می دهد .
