آزمون نرم افزار به کمک ابزار frama-c

مقدمه ای بر آزمون نرم افزار:

آزمودن نرم افزار یک عنصر حیاتی از تضمین کیفیت است و همچنین بیانگر بازبینی نهایی مشخصات، طراحی و تولید کد است.

هنگامی که کد منبع تولید شد، نرم افزار باید آزموده شود تا هر تعدادی از خطاها را که امکان داشته باشد، قبل از تحویل به مشتری کشف کرد. هدف، طراحی موارد آزمون است که احتمال یافتن خطا ها را بالا ببرند. اینجاست که تکنیک های آزمون نرم افزار وارد صحنه می شوند. این تکنیک ها راهنمایی سیستماتیک برای طراحی آزمون است.

آزمون نرم افزار از دو دیدگاه مطرح می شود:

الف: با استفاده از تکنیک های طراحی موارد آزمون با منطق داخلی برنامه (جعبه سفید) تمرین می شود.

ب: با خواسته های نرم افزار با استفاده از تکنیک های طراحی موارد آزمون (جعبه سیاه) تمرین می شود.

در حقیقت آزمون، تنها مرحله ای از فرآیند نرم افزار است که بیشتر ویرانگر بنظر می رسد تا سازنده.

اهداف آزمون نرم افزار عبارتند از:

الف: آزمون، فرآیند اجرای برنامه به قصد یافتن خطاست.

ب: مورد آزمون خوب، موردی است که احتمال یافتن خطاهای کشف شده در آن، بالا باشد.

ج: آزمون موفق، آزمونی است که خطاهای کشف نشده را کشف کند.

اگر آزمون با موفقیت انجام شود، خطاهای نرم افزار بر ملا خواهد شد ولی آزمون نمی تواند عدم وجود خطا و نقایص را اثبات نماید و همچنین کار آزمون رفع خطا نمی باشد.

اصول آزمون عبارتند از:

الف: همه آزمون ها باید تا حد خواسته های مشتری قابل ردیابی باشند.

ب: آزمون باید مدتها قبل از شروع آزمون، طرح ریزی شود.

ج: اصل پارتو «که بیان می کند 80 درصد همه خطاهای کشف شده طی آزمون، احتمالا در 20 درصد همه مولفه های برنامه قابل کشف هستند» در آزمون نرم افزار صدق می کند.

د: آزمون باید در ابعاد کوچک آغاز شود و به ابعاد بزرگتر گسترش یابد.

ه: آزمون کامل امکانپذیر نیست.

و: برای آنکه آزمون بیشترین بازدهی را داشته باشد، باید توسط یک شخص ثالث بی طرف انجام شود.

آزمون پذیری

آزمون پذیری نرم افزار میزانی از سهولت آزمودن یک برنامه کامپیوتری است. بدلیل آنکه آزمون دشوار است بهتر است بدانیم چه چیزی آن را به جریان می اندازد. گاهی برنامه نویسان مشتاق به انجام کارهایی هستند که به فرآیند آزمون کمک می کند و لیست کنترلی از نکات طراحی، ویژگی ها و غیره می تواند در بحث با آنها مفید واقع شود.

لیست کنترلی زیر ویژگی هایی نرم افزار آزمون پذیر مطرح می کند:

الف: قابلیت کار: هر چه بهتر کار کند، آزمون آن کارامد تر است.

ب: قابلیت مشاهده: آنچه می بینید، همان است که آزمایش می کنید.

ج: کنترل پذیری: هر چه بهتر بتوان نرم افزار را کنترل کرد، آزمون را بیشتر می توان خودکار و بهینه کرد.

د: تجزیه پذیری: با کنترل دامنه کاربرد آزمون، می توان مسایل را سریعتر جداسازی کرد و آزمونهای مجدد را با هوشمندی بیشتر انجام داد.

ه: سادگی: هر چه مورد آزمون کوچکتر باشد، سریعتر می توان آن را آزمود.

و: پایداری: هر چه تعداد تغییرات کمتر باشد، آزمون کمتر با مانع مواجه می شود.

ز: درک پذیری: هر چه اطلاعات بیشتری داشته باشیم، آزمون هوشمندانه تر انجام می شود.

ویژگی های یک آزمون خوب:

الف: آزمون خوب باید با احتمال زیادی خطا ها را کشف کند

ب: آزمون خوب دارای زواید نیست یعنی دو آزمون برای یک هدف یکسان طراحی نشود.

ج: آزمون خوب باید در بین آزمون های دیگر بهترین باشد.

د: آزمون خوب نباید بیش از حد ساده و نه بیش از حد پیچیده باشد.

نمایش برنامه:

تحلیل هایی که از نمایش برنامه بدست می آید در نهایت می تواند به آزمون نرم افزار کمک کند. نمایش برنامه دارای کاربردهای مختلفی است که بعضی از آنها عبارتند از:

الف: بهینه سازی برنامه ها

ب: فهم برنامه و مهندسی مجدد نرم افزار

ج: امنیت نرم افزار

د: درستی سنجی

نمایش برنامه ها به دو دسته تقسیم می شوند:

الف: نمایش ایستای برنامه: یعنی بدون نیاز به اجرای برنامه می توان برنامه مورد نظر را به یک ساختار نمایشی مناسب تبدیل نمود.

ب: نمایش پویای برنامه: یعنی لازم است برنامه مورد نظر توسط یک سری ورودی اجرا شود و پس از اجرا می توان داده های تولید شده از اجرا را به نحو مناسبی نمایش داد.

حال به منظور آشنایی با آزمون و تحلیل برنامه ها می خواهیم استفاده از ابزار Frama-C را مطرح نماییم.

Frama-C (Framework for Modular Analyses of C)

توضیح کلی راجع به Frama-C:

Frama-C یک نرم افزار متن باز است که مجموعه ای از ابزارها است که به آنالیز کد منبع نرم افزار نوشته شده در C اختصاص داده شده است.

Frama-C چندین تکنیک تجزیه و تحلیل ایستا را در یک چارچوب مشترک جمع آوری می کند. رویکرد مشترک Frama-C به تحلیلگران اجازه می دهد تا براساس نتایج قبلا توسط سایر تحلیلگران در این چارچوب تصمیم گیری کنند. Frama-C ابزار پیچیده ای مانند برش بندی و تحلیل وابستگی را نیز ارائه می دهد.

معماری Frama-C:

Frama-C با معماری افزونه Plug-in که قابل مقایسه با Gimp یا Eclipse است، سازماندهی می شود. یک کرنل مشترک ، اطلاعات را متمرکز و تحلیل ها را هدایت می کند. افزونه ها از طریق رابط های تعریف شده توسط کرنل با یکدیگر تعامل دارند. این امر باعث ایجاد استحکام در توسعه Frama-C می شود در حالی که اجازه می دهد طیف گسترده ای از کارایی را داشته باشد.

Frama-C قابل توسعه است و شامل چندین افزونه آماده برای استفاده از تجزیه و تحلیل استاتیک کد C است ، اما مهمتر از آن ، هر افزونه جدید ممکن است از نتایج یا ویژگی های ارائه شده توسط افزونه های موجود استفاده کند. این اجازه می دهد تا افزونه های بسیار قدرتمند با تلاش نسبتاً کمی نوشته شود. از دیدگاه توسعه دهنده افزونه ، اهداف اصلی پلتفرم Frama-C ارائه خدمات برای سهولت است.

در شکل زیر معماری Frama-C نشان داده شده است.

افزونه ها در Frama-C:

سه افزونه پر اهمیت که توسط سایر افزونه ها استفاده می شود:

Eva (Evolved Value analysis)

این افزونه دامنه تغییرات متغیرها را محاسبه می کند و کاملاً اتوماتیک است، اگرچه کاربر ممکن است تجزیه و تحلیل را درجا راهنمایی کند. Eva طیف گسترده ای از ساختار های C را در اختیار دارد. این افزونه از تکنیک های مفسر انتزاعی استفاده می کند.

Jessie and Wp

این افزونه ها مبتنی بر ضعیف ترین روش های محاسبه پیش شرط هستند. آنها اجازه می دهند تا ثابت كنند كه توابع C مشخصات آنها را مطابق با ACSL بیان می كنند. این اثبات ها ماژولار هستند: از مشخصات توابع نامیده شده برای اثبات بدون مراجعه به کد آنها استفاده می شود.

در دسترس بودن سه افزونه فوق امکان نوشتن افزونه های اضافی را فراهم می کند. در ادامه یک لیست غیر جامع از افزونه ها که قبلاً نوشته شده اند و با Frame-C توزیع شده اند آورده شده است. توجه داشته باشید که برخی از این افزونه ها هنوز در دست ساخت هستند.

Impact analysis

این افزونه مکانهایی را در کد منبع که تحت تأثیر یک تغییر قرار می گیرند برجسته می کند.

Scope & Data-flow browsing

این افزونه به کاربر اجازه می دهد تا داده های برنامه را از تعریف تا استفاده یا استفاده از آن به تعریف دیگر هدایت کند.

Variable occurrence browsing

این افزونه همچنین به عنوان یک مثال ساده برای توسعه افزونه جدید ، به کاربر اجازه می دهد تا در جایی که از یک متغیر معین استفاده می شود ، به عبارات برسد.

Metrics calculation

این افزونه به کاربر اجازه می دهد تا معیارهای مختلفی را از کد منبع محاسبه کند.

Semantic constant folding

این افزونه از نتایج افزونه تجزیه و تحلیل ارزش تکامل یافته استفاده می کند تا در کد منبع ، عبارات ثابت را با مقادیر آنها جایگزین کند. از آنجا که به EVA تکیه می کند ، قادر است بیش از این ساده سازی ها را نسبت به تجزیه و تحلیل نحوی انجام دهد.

Slicing

این افزونه کد را مطابق با معیار ارائه شده توسط کاربر، برش می دهد: یک نسخه از برنامه را ایجاد می کند، اما فقط بخش هایی را که با توجه به معیار داده شده لازم هستند، نگه می دارد.

Spare code

"کد یدکی" را حذف کنید، کدی که به نتایج نهایی برنامه کمک نمی کند.

E-ACSL

برای بررسی ادعای زمان اجرا، یادداشتهای مربوط به کد C را ترجمه کنید.

Aoraï

مشخصات بیان شده به صورت فرمول LTL (منطق زمانی خطی) را تأیید کنید.

سایر عملکردهای ثبت شده به همراه افزونه EVA (که از آدرس زیر می توانید دستورالعمل جامعی از آنرا مشاهده نمایید: https://frama-c.com/download/frama-c-eva-manual.pdf) را می توان به عنوان تأیید مشخصات عملکردی سطح پایین (ورودی ها ، خروجی ها ، وابستگی ها ، ...) در نظر گرفت. که البته در بخش پایانی این گزارش بعضی دیگر از قابلیت ها و افزونه ها مطرح می شود.

PathCrawler

به طور خودکار ورودی های مورد آزمایش را برای اطمینان از پوشش یک عملکرد C پیدا می کند. این افزونه می تواند برای آزمایش واحد ساختاری، به عنوان یک مکمل برای تجزیه و تحلیل استاتیک یا برای مطالعه مسیرهای اجرای عملی از عملکرد مورد استفاده قرار گیرد.

Mthread

افزونه بطور خودکار برنامه های C همروند را با استفاده از افزونه EVA با در نظر گرفتن تمام محاورات نخی ممکن تجزیه و تحلیل می کند. در پایان اجرای آن ، رفتار همروندی هر نخ بیش از حد تقریبی است و در نتیجه اطلاعات دقیقی در مورد متغیرهای مشترک حاصل می شود ، که mutex از بخشی از کد و غیره محافظت می کند.

Frama-Clang

این افزونه بر اساس کامپایلر clang، یک C++ سمت کاربر به Frama-C را فراهم می کند. کد C ++ را به یک Frame-C AST تبدیل می کند، که می تواند توسط افزونه های بالا مورد تجزیه و تحلیل قرار گیرد. توجه داشته باشید که این فرایند بسیار تجربی است و فقط از زیر مجموعه C ++ 11 پشتیبانی می کند.

در پایان این بخش باید به دو موضوع اشاره کرد که ابتدا موضوع توسعه افزونه ها است در Frama-C توسط علاقمندان قابل انجام است و موضوع بعدی اینکه در خارج از تیم Frama-C افزونه های دیگری وجود دارد که در آدرس زیر با عنوان Frama-C Wiki قابل دستیابی است:

https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:external_plugins

تصویر زیر افزونه ها را بصورت اجمالی نشان می دهد:

امکانات Frama-C:

الف: استفاده از Frama-C برای درک کد

زبان C مدت طولانی است که مورد استفاده قرار می گیرد و امروزه برنامه های بی شماری از ساختار C استفاده می کنند. این همه جا به دلایل تاریخی و به این دلیل که C برای تعداد قابل توجهی از برنامه ها (به عنوان مثال کد تعبیه شده) به خوبی سازگار است. با این حال، زبان C شامل مفاهیم و ساختار های سرهم بندی شده هم است. بسیاری از افزونه های Frama-C قادرند فاش کنند که کد C مورد تجزیه و تحلیل واقعاً چیست؟

بکمک Frama-C ، شما می توانید مجموعه ای از مقادیر ممکن برای متغیرهای برنامه را در هر نقطه از اجرای برنامه مشاهده کنید. برنامه اصلی را به برنامه های ساده تبدیل کنید و همچنین جریان داده در برنامه را از تعریف تا استفاده یا از استفاده تا تعریف ردگیری نمایید.

ب: ارائه ویژگی های فرمال برای نرم افزار های حیاتی

Frama-C اجازه می دهد تا تطابق کد منبع با مشخصات فرمال ارائه شده تأیید گردد. مشخصات عملکردی را می توان با زبان اختصاصی ، ACSL نوشت.

منظور از ACSL: ANSI/ISO C Specification Language است که یک زبان مشخصات رفتاری برای برنامه های C است که از JML: Java Modeling Language الهام گرفته است. مستندات ACSL را در این آدرس مطالعه نمایید. https://frama-c.com/download/acsl.pdf

بخش های ساختیافته در اسناد طراحی شما نیز می تواند به عنوان مشخصات فرمال در نظر گرفته شود. به عنوان مثال ، لیست متغیرهای سراسری که قرار است یک تابع از آن بخواند یا بنویسد یک مشخصات رسمی است. Frama-C می تواند این اطلاعات را به طور خودکار از کد تابع بدست آورده و به شما امکان می دهد تا از بر آورده شدن این قسمت از سند طراحی اطمینان حاصل کنید که البته بسیار سریعتر و کم خطر تر نسبت به بررسی کد این کار را انجام می دهد.

نصب Frama-C:

روش پیشنهادی نصب Frama-C از تیم توسعه ی آن، استفاده از مخزن OPAM است. برای اینکار در اوبنتو نسخه های 18.4 و بعد از آن کافی است مراحل زیر طی شود:

add-apt-repository ppa:avsm/ppa

apt update

apt install opam

احتمال دارد که بعد از نصب خطایی از سمت لینوکس مبنی بر اینکه مقداردهی اولیه صورت نگرفته است صادر شود که در اینصورت از دستور زیر استفاده میشود:

opam init --reinit –ni

برای آنکه افزونه های اصلی Frama-C نصب شود باید از دستور های زیر استفاده کرد:

opam install depext

opam depext frama-c

نصب برنامه ی به کمک دستور opam بصورت زیر است:

opam install frama-c

بعد از اجرای این دستور برنامه بصورت کامل نصب می شود. با استفاده از دستور frama-c-gui می توان واسط گرافیکی برنامه را فراخوانی کرد.

بعد از این دستور برنامه اجرا می شود.

تحلیل های مختلف در Frama-C :

حال باید یک برنامه نوشته شده به زبان C را در نرم افزار باز کرد و سپس بعضی از تحلیل ها را بر روی آن برنامه انجام دهیم. برای اینکار کافی است از منوی بالای صفحه گزینه ProjectàNew Project را انتخاب کرده و سپس فایلی که میخواهیم را طبق عکس های زیر انتخاب می کنیم. باید توجه داشت که اگر می خواهیم بیش از یک frama-c را داشته باشیم باید به همان تعداد ترمینال باز کرده و دستور frama-c-gui را صادر نماییم.

بعد از مراحل گفته برنامه مورد نظر در Frama-C باز می شود. تصویر زیر همین موضوع را نشان می دهد. حالا همه چیز برای تحلیل و آزمون برنامه آماده است.

Callgraph

در این بخش تصویری شماتیک از توابع موجود در برنامه و نحوه وابستگی آنها نمایش داده می شود. برای اینکار کافی است مانند تصویر از منوی بالای صفحه Analysesàshow callgraph را انتخاب کرده و نتیجه به دو صورت Global , Tree قابل مشاهده است. البته Both باعث می شود هر دو حالت در یک تصویر ظاهر شود.

Inout

همانطور که قبلا توضیح داده شد افزونه مهمی به نام Eva وجود دارد که یکی از کارهایی که انجام میدهد موضوع بررسی مکان های ورودی و خروجی است. در ترمینال لیست افزونه های موجود در frama-c خود را می توانید مشاهده نمایید و به کمک آنها تحلیل ها را انجام دهید ولی ما در این دستور کار به جهت سادگی بیشتر با واسط گرافیکی کار کردیم. دستور زیر برای مشاهده افزونه ها

frama-c –plugins

برگردیم به افزونه inout که خود از طریق گزینه analysisàanalysis قابل دستیابی است.

گزینه inout انتخاب شده و توضیح کامل درباره هر گزینه در تصویر زیر داده شده است.

با انتخاب گزینه inout تصویر زیر حاصل می شود.

دایره های سبز رنگ محل ورودی و خروجی ها نشان می دهد و دایره های نارنجی رنگ محل assert ها را نشان می دهد که مکان مقدار دهی اولیه یک متغیر و یا برگشت از تابع و ... است. در قسمت console هم اطلاعاتی درباره مقادیر ورودی و خروجی آورده شده است.

Metrics

این افزونه اندازه گیری پیچیدگی بر روی کد برنامه به زبان C را انجام می دهد. این افزونه می تواند بر روی درخت نحوی انتزاعی (AST) نرمال شده و یا بر روی کد اصلی برنامه کار کند. این افزونه می تواند مقادیر مختلف را در کد برنامه بطور خودکار اندازه گیری کند.

همچنین از Metrics در اندازه گیری سه حالت زیر نیز استفاده می شود:

الف: پیچیدگی سیکلوماتیک McCabe: در واقع اندازه گیری تعداد مسیرهای کد است و محاسبه پیچیدگی جریان کنترلی برنامه است. عدد سیکلوماتیک یک کد نشان دهنده ارتباط ضعیفی با تعداد نقایص است.

ب: پیچیدگی Halstead: به عنوان مجموعه ای از معیارهای نرم افزاری است که توسط موریس Halstead در سال 1977 معرفی شد. هدف شناسایی خصوصیات قابل اندازه گیری کد و فراتر از اندازه گیری پیچیدگی تنها است.

ج: پوشش Eva: این بخش از افزونه Metrics به عنوان کمک به اکتشاف کد جدید با افزونه Frama-C Eva به نظر می رسد. اولین قدم ها برای ایجاد یک کد جدید می تواند کاملاً پیچیده باشد و بیشتر اوقات ، Eva به دلیل عدم دقت بیش از حد متوقف می شود. این عدم دقت می تواند علل متفاوتی داشته باشد مانند بدنه عملکردهای کتابخانه وجود ندارد ، ناخوشایند خواندن در حافظه ، ...

حالا برای مشاهده صورت اولیه از افزونه metrics از دستور frama-c quicksort.c –metrics استفاده کرد و البته با کمی تغییر اطلاعات را در فایل txt ذخیره کرد.

حالا به کمک دستور frama-c -metrics-h می توان سوییچ های مختلف این دستور را مشاهده نمود.

PDG: Program Dependence Graph

گراف وابستگی برنامه در واقع گرافی است که وابستگی داده ای و کنترلی دستورات یک برنامه را به هم نشان می دهد.

منظور از وابستگی داده ای آن است که دستور S دارای وابستگی داده ای با دستور T است، اگر یک مسیر جریان کنترلی از Tبه S وجود داشته باشد و متغیری در T تعریف شده باشد که در S استفاده شده باشد.

به لبه هایی که مشخص کننده وابستگی داده ای بین دستورات برنامه هستند، اصطلاحا لبه های وابستگی داده ای یا لبه های تعریف/استفاده گفته میشود. گره های برنامه )دستورات( و لبه های وابستگی داده ای بین آنها تشکیل گراف وابستگی داده ای میدهند.

برای تعریف وابستگی کنترلی می گوییم Y به X دارای وابستگی کنترلی است، اگر و فقط اگر X مستقیما تعیین کنند که Y اجرا شود (دستورات درون یک شاخه از یک گزاره معمولا به آن گزاره دارای وابستگی کنترلی هستند(.

برای ترسیم گراف PDG از دستورات زیر استفاده میشود که دستور دوم برای تبدیل فایل dot به فایل pdf است.

Post dominators

دستور )گره( X دستور Y را پس تسلط میکند (post dominates) اگر هر مسیر محتمل برنامه از Y به دستور خروجی (Exit) باید حتما از دستور X عبور کند.

برای رسم post dominators باید دستور زیر را در ترمینال وارد نماییم.

frama-c quicksort.c –dot-postdom main

در خروجی حالا به تعداد توابع که در برنامه داشته باشید فایل dot تولید می شود. ما دو تابع داریم پس همانطور که در تصویر نشان داده شده دو فایل dot تولید می شود که باید تبدیل به فایل pdf کنیم. در این مرحله مشاهده میکنید که در خط 4 از تابع main خطا گرفته و فایل pdf تولید شده خالی از محتوا است. دلیل این موضوع اینست که postdominators کلا با دستورات printf و scanf مشکل دارد. لذا باید این دستورات را تبدیل به کامنت (توضیحات) کنیم تا خطا بر طرف شود.

و سپس همان دستورات بالا را تکرار میکنیم.

Slicing

یک برش برنامه، حاوی بخشهایی از یک برنامه است که )به طور بالقوه( بر مقادیری که در یک نقطه مشخص برنامه محاسبه میشوند، تاثیر میگذارد. به چنین نقطه مشخصی اصطلاحاً معیار برشبندی گفته میشود .

بخشهایی از برنامه که تاثیر مستقیم یا غیرمستقیم بر مقادیر محاسبه شده در یک معیار برشبندی C دارند، یک برش برحسب معیار C را ایجاد می کنند. به فرآیند محاسبه برشهای برنامه، برشبندی گفته میشود.

•مفهوم برش بندی برای اولین بار توسط Weiser ارائه شد. Weiser معتقد بود که یک برش برنامه منطبق بر انتزاع های ذهنی است که افراد هنگام اشکالزدایی یک برنامه انجام میدهند. روشهای مختلفی برای محاسبه برشها و انواع مختلفی از برشبندی پیشنهاد شده است، که دلیل اصلی این تنوع، این واقعیت است که کاربردهای مختلف، نیازمند خواص و ویژگیهای مختلفی از برشها هستند. معیار برش را می توان با یک یا چند گزینه خط فرمان مشخص کرد. هر یک از گزینه های زیر یک عنصر قابل مشاهده را مشخص می کند تا در کد حاصل حفظ شود. به عنوان مثال ، با گزینه lice-Return f- ، این افزونه اطمینان می دهد که ، هر بار که تابع f در کد اصلی خاتمه یابد، در کد بریده شده خاتمه می یابد، و مقدار برگشتی در هر دو مورد یکسان است.

-slice-calls f1,...,fn

Selects every call to the functions f1,...,fn, and all their effects.

-slice-return f1,...,fn

Selects the result (returned value) of functions f1,...,fn.

-slice-value v1,...,vn

Selects the result of left-values v1,...,vn at the end of the function given as entry point.

-slice-wr v1,...,vn

Selects the write accesses to left-values v1,...,vn.

-slice-rd v1,...,vn

Selects the read accesses to left-values v1,...,vn.

-slice-pragma f1,...,fn

Uses the slicing pragmas in the code of functions f1,...,fn as slicing criteria.

-slice-assert f1,...,fn

Selects the assertions of functions f1,...,fn.

-slice-loop-inv f1,...,fn

Selects the loop invariants of functions f1,...,fn.

-slice-loop-var f1,...,fn

Selects the loop variants of functions f1,...,fn.

-slice-threat f1,...,fn

Selects the threats (emitted by the value analysis) of functions f1,...,fn.

-slice-undef-functions

Allows the use of the -slicing-level option for calls to undefined functions, i.e. for function prototypes (by default, prototypes of undefined functions are never specialized).

-slicing-level n

Sets the level of slicing/specialization used for function calls. The possible values for n are:

0: doesn't slice the called functions,

1: allows slicing of the called functions, but doesn't perform specialization of these functions,

2: allows slicing and specialization of the called functions, but at most one slice/specialization by function,

3: allows several slice/specializations by function.

در دو تصویر زیر نیز به کمک دستور frama-c –slicing-h کلیه دستورات و گزینه های برش بندی نمایش داده می شود.

حالا سه برش را طبق تصویر زیر انجام میدهیم و خروجی هر کدام را به ترتیب در فایل های 1.txt , 2.txt , 3.txt ذخیره میکنیم.

خروجی هر کدام از سه برش فوق بصورت زیر است:

Users

این افزونه برای نشان دادن و آزمون بر روی دستورات فراخوانی توابع است. این افزونه امکانات زیادی ندارد و به کمک دستور زیر می توان آن را اجرا کرد. ما طبق همین دستور فایل 4.txt را بعنوان خروجی دریافت کرده ایم.

frama-c –users quicksort.c > 4.txt

WP

افزونه WP بعد از حساب های ضعیف ترین پیش شرط نامگذاری شد که یک تکنیک مورد استفاده برای اثبات ویژگی های برنامه می باشد. ابزارهای اخیر این تکنیک را با کارآیی عالی پیاده سازی می کنند، به عنوان مثال Boogie و Why. در حال حاضر یک افزونه Frama-C به نام Jessie در INRIA وجود دارد که ضعیف ترین حساب پیش شرط را برای برنامه های C با وارد کردن آنها به زبان Why کامپایل می کند.

افزونه WP یک اجرای جدید از چنین حساب های ضعیف پیش شرط برای برنامه های مفسر C است که بر پارامتر کردن w.r.t مدل حافظه تمرکز دارد. این یک کار تکمیلی برای افزونه Jessie است ، که به تفکیک مدل حافظه که مبنای کار Burstall است، وابسته است. مدل حافظه Jessie برای تنوع زیادی از برنامه های ساختیافته C بسیار کارآمد است. با این حال، این افزونه وقتی که دستکاری حافظه سطح پایین، مانند نقش های ناهمگن، درگیر می شوند، بدرستی کار نمیکند. علاوه بر این ، Jessie با کامپایل برنامه C به Why کار میکند، راهکاری که کاربر را از ترکیب حساب ضعیف ترین پیش شرط با سایر تکنیک ها، مانند افزونه Eva رها می کند. افزونه WP با همکاری فکری طراحی شده است. یعنی ممکن است شما برای اثبات برخی تفسیر های برنامه های C خود از WP استفاده کنید و دیگران را با افزونه های مختلف اثبات کنید. پیشرفت های اخیر کرنل Frama-C پس از آن مسئولیت مدیریت اثبات جزئی و تحکیم کلی آنها را بر عهده دارد.

منظور از Weakest Preconditions چیست؟

اصول ضعیف ترین حساب پیش شرط در اصل کاملاً ساده است. با توجه به تفسیر کد از برنامه شما، مثلاً عبارت Q پس از یک عبارت stmt، ضعیف ترین پیش شرط P با تعریف "ساده ترین" ویژگی P است که باید قبل از stmt معتبر باشد به گونه ای که Q بعد از اجرای stmt نگه داشته شود.

Hoare Triples از نظر ریاضی، چنین ویژگی را با یک سه گانه Hoare بیان می کند:

{P} stmt {Q}

که می خواند: "هر زمان که P نگه داشته باشد ، پس از اجرای stmt ، Q را نگه می دارد".

بنابراین ، ما می توانیم ضعیف ترین پیش شرط را به عنوان تابعی از wp بر روی عبارات و خصوصیات تعریف کنیم به گونه ای که سه گانه Hoare زیر همیشه نگه می دارد:

{wp(stmt,Q)} stmt {Q}

به عنوان مثال ، یک انتساب ساده را در مورد متغیر محلی عدد صحیح x در نظر بگیرید. ما داریم:

{x + 1 > 0} x = x + 1; {x > 0}

این موضوع را باید در این حالت ساده درک کرد، ضعیف ترین پیش شرط برای انتساب ویژگی Q بیش از x با جایگزین کردن x با x + 1 در Q تعیین شود. به طور کلی ، برای هر جمله و هر ویژگی می توان ضعیف ترین پیش شرط را تعریف کرد.

درباره اجرای wp ابتدا به کمک دستور frama-c –wp-h گزینه های مختلفی که این افزونه به ما میدهد را مشاهده میکنیم که بسیار مفصل است.

ساده ترین حالت استفاده از این افزونه با دستور زیر است که خروجی را در فایل wp.txt ذخیره کرده ایم.

Frama-c –wp quicksort.c > wp.txt

Impact

افزونه تجزیه و تحلیل impact اجازه ی محاسبه خودکار مجموعه عبارات تأثیر پذیرفته شده توسط عوارض جانبی عبارت دیگر در یک برنامه C را می دهد. عبارت هایی که در این مجموعه قرار ندارند ، تضمین می شوند که تحت تأثیر گزاره انتخابی قرار نگرفته اند. افزونه impact از طریق یک فهرست متنی در هر جمله در رابط کاربر گرافیکی Frama-C در دسترس است. تصویر نحوه ی انجام آن را نشان می دهد.

نتایج impact در گزینه console قابل مشاهده است.

Occurrence analysis plug-in

افزونه تجزیه و تحلیل Occurrence استفاده از یک متغیر در یک برنامه C را نشان می دهد. این تحلیل مقادیر سمت چپ را که ممکن است به متغیر انتخاب شده دسترسی پیدا کند، مورد توجه قرار می دهد.

در نتیجه مکان هایی که متغیر استفاده شده است در خروجی نشان می دهد و همچنین اطلاعاتی در گزینه console وجود دارد.

RTE: Runtime error annotation generation plug-in

افزونه RTE به شما امکان تشخیص خطای اجرا را می دهد که در سه حالت زیر بوجود می آید:

الف: خطاهای معمول زمان اجرا

ب: سرریز در عملکردهای عدد صحیح بدون علامت

ج: توابعی که در شروع برنامه فرخوانی می شوند

برای اینکار از دستور frama-c –rte quicksort.c استفاده می شود.

در انتها برنامه ای که آزمون بر روی آن انجام شده، آورده میشود:
#include<stdio.h>

void quicksort(int number[25],int first,int last){

   int i, j, pivot, temp;

   if(first<last){

      pivot=first;

      i=first;

      j=last;

      while(i<j){

         while(number[i]<=number[pivot]&&i<last)

            i++;

         while(number[j]>number[pivot])

            j--;

         if(i<j){

            temp=number[i];

            number[i]=number[j];

            number[j]=temp;

         }

      }

      temp=number[pivot];

      number[pivot]=number[j];

      number[j]=temp;

      quicksort(number,first,j-1);

      quicksort(number,j+1,last);

   }

}

int main(){

   int i, count, number[25];

   printf(&quotHow many elements are u going to enter?: &quot);

   scanf(&quot%d&quot,&count);

   printf(&quotEnter %d elements: &quot, count);

   for(i=0;i<count;i++)

      scanf(&quot%d&quot,&number[i]);

   quicksort(number,0,count-1);

   printf(&quotOrder of Sorted elements: &quot);

   for(i=0;i<count;i++)

      printf(&quot %d&quot,number[i]);

   return 0;

}