تحلیل و تست نرم افزار با ابزار Frama-c

سلام :)

ابزار Frama-c نرم افزاری بوده که برای تست و آزمون نرم افزار جهت رفع مشکلاتی که در زمان نوشتن برنامه و یا تغییراتی که در برنامه ایجاد می شود ، استفاده می شود .

+ این ابزار برای زبان های نوشته شده به زبان c استفاده می شود .

+ ابزار Frama-c در محیط لینوکس قابل اجرا می باشد . ( و البته در MAC هم ) => Linux base

خوب سیستم عاملی که ما باهاش کار میکنیم Ubuntu 18.04 هستش .چرا؟ جلو تر میگم چرا ؛)

نصب Frama-c

همان طور که گفته شد می توان Frama-c را روی سیستم عامل های Linux base نصب کرد .

ما روی Ubuntu 18.04 LTS نصب میکنیمش به دلیل آنکه در حال حاضر جدید ترین LTS میباشد و در نسخه های 19 به بالا در نصب دچار مشکل میشویم احتمالا ! چرا ؟ چون میبایست از Opam استفاده کنیم که خوب یکم داستان دار میشه ! حتی ممکنه روی سیستم شما نه تنها نصب نشه بلکه مشکل هم برای سیستم ایجاد کنه.

اما نترسین خبری نیست ! حلش میکنیم بدون کوچکترین مشکل

شما باید ابتد Ubuntu را نصب کنید که میتوان هم به صورت مجازی و هم به عنوان سیستم عامل دیگری در سیستم خود نصب کنید . کار سختی نیست میتوانید با یک سرچ ساده پیدا کنید . اگر خیلی آشنا نیستین با Ubuntu پیشنهاد میکنیم به صورت مجازی بالا بیارین. از لینک پایین استفاده کنید برای نصب.

حالا اگر به پیشنهاد بنده Ubuntu 18.04 را نصب کرده باشین خیلی راحت Frama-c را نصبش میکنیم .

1 : ابتدا terminal را باز میکینم .

2 : دستور مقابل را وارد میکنیم => sudo apt-get install frama-c

و تمام !!

برای اجرای آن در همان ترمینال این کد را میزنیم => frama-c-gui

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

frama-c-base

خوب حالا frama-c را باز کرده ایم .

باز کردن برنامه ی مورد نظر

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

این کد برای تبدیل اعداد دودویی به مبنای 10 و 8 و 16 میباشد که ما از آن استفاده میکنیم .

#include<stdio.h> // include stdio.h library

void convert_(int, int);

int main(void)

{

int num, choice, base;

while(1)

{

printf("Select conversion: \n\n");

printf("1. Decimal to binary. \n");

printf("2. Decimal to octal. \n");

printf("3. Decimal to hexadecimal. \n");

printf("\nEnter your choice: ");

scanf("%d", &choice);

switch(choice)

{

case 1:

base = 2;

break;

case 2:

base = 8;

break;

case 3:

base = 16;

break;

default:

printf("Invalid choice.\n\n");

continue;

}

printf("Enter a number: ");

scanf("%d", &num);

printf("Result = ");

convert_(num, base);

printf("\n\n");

}

return 0; // return 0 to operating system

}

خوب حالا فایل که کد بالا در آن است و دارای پسوند c. میباشد را باز میکنیم .چجوری؟ اینجوری ...

برای باز کردن فایل C بر روی منو file رفته و گزینه source file را انتخاب کرده و سپس فایل مورد نظر را یافته و انتخاب کنید.

خوب حالا برنامه ی نوشته شده را میبینیم . حالا نوبت میرسد به تحلیل های ما روی برنامه نوشته شده.

نکته : تلاش ما در اینجا آشنایی کار با frama-c هست . فرض ما بر این است که با روش های تحلیل آشنایی کمی داشته باشید .

call graph and tree view

گزارش call graph به نوعی یک گزارش ظاهری بوده که از طریق آن میتوانید یک گراف اجرای برنامه و درخت آن را نمایش داد. برای تهیه یک call graph کافیست تا به منو analyses رفته و گزینه show entire callgraph را انتخاب کنید سپس باید همانند شکل زیر گرافی برای شما ظاهر شود.

inout

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

برای تهیه inout برنامه ابتدا به منو Analyses رفته سپس بر روی Analysesکلیک کرده و از منوی سمت چپ inout را کلیک کرده و مقادیر out, input, inout را انتخاب کرده و نتیجه در کنسول (تب های پایین صفحه frama-c) به نمایش در خواهد آمد.

Metrics

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

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

با این حال ، frama-C همچنین درخت انتزاعی منبع (AST) اصلی را همانطور که هست نگه می دارد. حتی اگر تجزیه و تحلیل های frama-C معمولاً حول محور نمایش نرمال باشد ، برخی از امکانات برای دستکاری AST اصلی دیگر وجود دارد.

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

رفتار پیش فرض ، همانطور که توسط سوئیچ metrics فعال شده است ، محاسبه معیارهای نحوی در ASTنرمال است.

برای استفاده از این سوئیچ در بخش Terminal از دستور زیر استفاده می کنیم :

• frama-c Array.c –metrics > Metrics.txt

خروجی این دستور بصورت یک فایل متنی است که در کنار فایل کد برنامه ذخیره می گردد و بصورت زیر خواهد بود

pdg

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

برای تهیه PDG ابتدا باید از طریق ترمینال اطلاعات به دست آمده از PDG را در فایل dot ذخیره کرده سپس آن را به PDF تبدیل نماییم. در ابتدا دستور زیر را اجرا کرده تا PDG را در فایل projectpdg.dot ذخیره نماید تا سپس آن را به PDF تبدیل نماییم تا قابل دیدن شود. 2 دستور آخر.

حالا pdf را باز کنید و نتیجه را ببینید . اینجا نتیجه را بارگذاری نکردم تا نتیجه را خودتون ببینید ؛)

Post Dominator

در Post Dominator دستوراتی که بر روی دستورات دیگر تاثیر میگذارد را میتوان مشخص کرده و به شکل یک گراف رسیدن به مقصد به نمایش در خواهد آورد.

برای تهیه Post dominator باید از طریق ترمینال دستور زیر را نوشته تا ابتدا گزارش را در فایل dot ذخیره کرد تا سپس آن را به PDF تبدیل کرد اما نکته ای که وجود دارد وجود printf و scanf در دستورات است که باید این دستورات را از طریق مقدار دهی داخلی مقدار داد و از return استفاده کرد تا گراف post dominator ایجاد شود.

روش راحت تر برای حل مشکل printf ؟ کافیه این دستور را کامنت کرد => /* comment */

این هم نتیجه در pdf :

Slicing

عبارت است از محاسبه مجموعه اظهارات برنامه ، برش برنامه ، كه ممكن است بر مقادیر در بعضی از نقاط مورد علاقه تأثیر بگذارد ، از آن به عنوان معیار برش استفاده می شود. برش برنامه می تواند در اشکال زدایی برای یافتن منبع خطاها آسان تر مورد استفاده قرار گیرد. سایر کاربردهای برش شامل نگهداری نرم افزار ، بهینه سازی ، آنالیز برنامه و کنترل جریان اطلاعات است.

برای استفاده از این سوئیچ در بخش Terminal از دستور زیر استفاده می کنیم :

• frama-c -slice-wr n Array.c -slice-print > Slice.txt

خروجی این دستور بصورت یک فایل متنی است که در کنار فایل کد برنامه ذخیره می گردد و بصورت زیر خواهد بود.

Users

با استفاده از Users میتوانید ورودی و خروجی ها را پیدا کنید.

برای تهیه گزارش User ابتدا به برنامه بازگشته و سپس بر روی Analysis رفته و بر روی منوی user کلیک کرده و مقدار user- را انتخاب کرده و سپس بر روی execute کلیک می کنیم تا در کنسول نتیجه تولید شود.

Wp

بر اساس منطق برنامه میگوییم متغیر ها در چه بازه ای هستند.

برای هر یادداشت کد ، این تکنیک مجموعه ای از تعهدات اثبات را ایجاد می کند ، یعنی. فرمول منطقی مرتبه اول ریاضی است که می تواند به اثباتگرهای قضیه خودکار مانند Alt-Ergo یا دستیاران اثبات تعامل مانند Coq ارسال شود. سایر پیش نمایش ها نیز از طریق پلتفرم why پشتیبانی می شوند.

برای استفاده از این سوئیچ نیز از بخش Terminal استفاده و دستور زیر را اجرا می کنیم :

• frama-c -wp Array.c > WP.txt

خروجی این دستور نیز بصورت فایل متنی در کنار فایل کد ذخیره و بصورت زیر خواهد بود :

Sparecode

افزونه Spare code در حذف کد غیر ضروری در یک برنامه کمک می کند.

افزونه Spare code یک برنامه خروجی تولید می کند که تضمین میکند کد C قابل جبران باشد و همان رفتار را با برنامه تحلیل شده از نظر مقادیر اختصاص داده شده به متغیرهای خروجی عملکرد اصلی داشته باشد.

value

مجموعه ای از مقادیر ممکن را برای هر متغیر در هر نقطه از برنامه محاسبه می کند.

Occurrence

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

همانطور که از مثال نشان داده شده است ، تجزیه و تحلیل مستعارها(alias) را در نظر می گیرد.