Raheleh.Shahidifar

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