مقدمه:
مقوله کیفیت نرم افزار یکی از موضوعات بسیار مهم در فرآیند توسعه نرم افزار به حساب می آید. علیرغم بودجه های قابل توجهی که صرف توسعه نرم افزارها می شود، هزینه اندکی صرف آزمون آنها میگردد. در نتیجه بخش مهمی از خطاها در کد برنامه ها باقی مانده و در دستان کاربران نهایی نمایان می شوند. این امر، خسارات مالی و جانی هنگفتی را متوجه توسعه دهندگان و کاربران نرم افزارها می کند. اگر خطاهای نرم افزاری در مراحل ابتدایی توسعه نرم افزار شناسایی و رفع شوند، این هزینه ها و خسارات به میزان قابل توجهی کاهش خواهند یافت.
در این نوشته به ابزار توسعه یافته frama-c در حوزه کیفیت نرم افزار می پردازیم و می آموزیم چگونه با در اختیار داشتن کد برنامه ها می توان ورودی هایی تولید کرد که به کمک آنها معیارهای مختلف پوشش برنامه ها را برآورده نموده و مشکلات موجود را شناسایی کرد.
این ابزار در محیط سیستم عامل لینوکس و برای نرم افزار های تهیه شده به زبان C قابل استفاده می باشد. برای استفاده در سایر سیستم های عامل نیز می توان از ماشین های مجازی اعم از Virtual Box یا Virtual Machine استفاده کرد.
نصب frama-c :
برای نصب ما از ماشین مجازی Virtual Box و نسخه 18.04 سیستم عامل ubuntu استفاده کرده ایم.
برای نصب این ابزار در محیط ubuntu و در قسمت Terminal از دستورات زیر استفاده می کنیم :
بعد از نصب ابزار مورد نظر، اجرای آن به دو شکل قابل انجام خواهد بود. اول اجرای برنامه بصورت گرافیکی و دوم با استفاده از خط دستور Terminal.
جهت مشاهده محیط گرافیکی از دستور زیر استفاده می کنیم :
که محیط برنامه مطابق شکل خواهد بود :
برای تست نرم افزار آیتم های متنوعی وجود دارد و هر بخش نمایانگر بخشی از اطلاعات مربوط به نرم افزار می باشد. در این آموزش ما آیتم های زیر را مورد بررسی قرارمی دهیم:
همچنین از کد زیر که به زبان C نوشته شده است، برای انجام آزمایش استفاده می کنیم:
#include <stdio.h> int largest_element(int arr[], int num){ int i, max_element; max_element = arr[0]; for (i = 1; i < num; i++) if (arr[i] > max_element) max_element = arr[i]; return max_element; } int sum_array_elements( int arr[], int n ) { if (n < 0) { return 0; } else{ return arr[n] + sum_array_elements(arr, n-1); } } void bubble_sort(int arr[], int count) { int temp, i, j; for(i=count-2;i>=0;i--){ for(j=0;j<=i;j++){ if(arr[j]>arr[j+1]){ temp=arr[j]; arr[j]=arr[j+1]; arr[j+1]=temp; } } } for(i=0;i<count;i++) printf("%d-",arr[i]); } int main() { int count=10; int arr[count]; printf("Enter the array : "); for(int i=0;i<count;i++){ printf("\narray[%d] : ",i+1); scanf("%d",&arr[i]); } int n = sizeof(arr)/sizeof(arr[0]); printf("Largest element of array is %d", largest_element(arr, n)); printf("\nSum of array elements is:%d",sum_array_elements(arr,count)); printf("\nSorted elements is:"); bubble_sort(arr,count); return 0; }
برای ورود کد مورد نظر به این ابزار در منو Projects گزینه New Project را انتخاب و فایل برنامه مورد نظر را انتخاب می کنیم :
نمودار Call graph :
یک نمودار جریان کنترل است ، که بیانگر روابط فراخوان بین زیر خطوط در یک برنامه کامپیوتری است . هر گره یک روال را نشان می دهد و هر لبه (f، g) نشان می دهد که روش f فراخوانی g را فراخوانی می کند. بنابراین ، یک چرخه در نمودار ، تماسهای رویه بازگشتی را نشان می دهد.
برای اجرای این نمودار بر روی کد فوق، بعد از انتخاب فایل کد مربوطه در ابزار frama-c ، در منو Analyses گزینه show callgraph را انتخاب می کنیم تا نمودار مورد نظر تولید گردد :
تست ورودی و خروجی inout :
این تست با ایجاد ورودی ها و خروجی های متغیر برنامه مورد نظر را بررسی می کند.
جهت انجام این آزمایش در برنامه در منو Analyses گزینه Analyses را انتخاب کرده و در پنجره باز شده گزینه inout را انتخاب و گزینه های مربوط به ورودی و خروجی را مطابق شکل انتخاب می کنیم:
بعد از ارزیابی برنامه محل های ورودی و خروجی مشخص می شوند :
در قسمت console نیز ورودی ها و خروجی های تست شده نمایش داده می شود:
آزمون کاربران users :
در این آزمون می توانیم مشاهده کنیم هر تابع چه توابعی را فراخوانی کرده است. برای استفاده از این آزمون در منو Analyses گزینه Analyses را انتخاب کرده و در پنجره باز شده گزینه users را انتخاب و گزینه های مربوط به ورودی و خروجی را مطابق شکل انتخاب می کنیم:
و خروجی آن مطابق شکل زیر است :
سوئیچ metrics :
آنالیزهای frama-C معمولاً بر اساس اصطلاح داخلی انتزاعی داخلی خود عمل می کنند. فرایند نرمال سازی ، به عنوان مثال عبارات برگشتی گمشده را اضافه می کند ، همه حلقه ها را به عبارات while تبدیل می کند ، متغیرهای موقت را معرفی می کند و ...
اگرچه این روند نرمال سازی بر محتوای معنایی کد تأثیر نمی گذارد ، اما همتای دستوری آن است که در واقع تغییر کرده است. بنابراین می تواند بر معیارهای محاسبه شده از کد منبع تأثیر بگذارد.
با این حال ، frama-C همچنین درخت انتزاعی منبع (AST) اصلی را همانطور که هست نگه می دارد. حتی اگر تجزیه و تحلیل های frama-C معمولاً حول محور نمایش نرمال باشد ، برخی از امکانات برای دستکاری AST اصلی دیگر وجود دارد.
کاربران افزونه Metrics می توانند ماهیت AST را که باید از آن محاسبه شود ، مشخص کنند. برخی از معیارها فقط برای یک نمایندگی AST در دسترس هستند.
رفتار پیش فرض ، همانطور که توسط سوئیچ metrics فعال شده است ، محاسبه معیارهای نحوی در ASTنرمال است.
برای استفاده از این سوئیچ در بخش Terminal از دستور زیر استفاده می کنیم :
خروجی این دستور بصورت یک فایل متنی است که در کنار فایل کد برنامه ذخیره می گردد و بصورت زیر خواهد بود :
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing Array.c (with preprocessing) Array.c:45:[kernel] warning: Variable-sized local variable arr [metrics] Defined functions (4) ===================== bubble_sort (1 call); largest_element (1 call); main (0 call); sum_array_elements (2 calls); Undefined functions (9) ======================= __fc_vla_alloc (1 call); __fc_vla_free (1 call); printf_va_1 (1 call); printf_va_2 (1 call); printf_va_3 (1 call); printf_va_4 (1 call); printf_va_5 (1 call); printf_va_6 (1 call); scanf_va_1 (1 call); 'Extern' global variables (0) ============================= Potential entry points (1) ========================== main; Global metrics ============== Sloc = 68 Decision point = 8 Global variables = 0 If = 8 Loop = 5 Goto = 2 Assignment = 25 Exit point = 4 Function = 13 Function call = 13 Pointer dereferencing = 12 Cyclomatic complexity = 12
در این خروجی اعلام می شود که هر متغیر یا تابع چند بار فراخوانی شده است .
سوئیچ PDG :
در علم کامپیوتر ، نمودار وابستگی به برنامه (PDG) یک نمایش است ، که از نماد نمودار استفاده می کند و وابستگی به داده ها و وابستگی های کنترل را آشکار می کند. از این وابستگی ها در بهینه سازی کامپایلرها برای ایجاد دگرگونی ها در هنگام تجزیه و تحلیل وابستگی استفاده می شود تا از هسته های چندگانه استفاده شود و موازی سازی بهبود می یابد.
برای انجام این کار بر روی فایل کد، در بخش Terminal از دستور زیر استفاده می کنیم :
بعد از اجرای این دستور تعدادی فایل .dot در کنار فایل برنامه ایجاد می گردند. برای تبدیل این فایل ها به فرمت PDF و مشاهده نمودار آن از دستور زیر استفاده می کنیم :
که خروجی آن بصورت زیر است :
سوئیچ post dominator :
در نمودارهای جریان کنترلی ، گره d بر گره n غالب است (dominates) اگر هر مسیری از گره ورودی به n باید از d عبور کند. از نظر نشانه گذاری، به صورت d dom n (یا گاهی اوقات d >> n) نوشته می شود.
شبیه به تعریف تسلط فوق ، گره z گفته می شود که گره n را غالب می کند اگر همه مسیرها به گره خروجی نمودار که از n شروع می شود باید z را طی کنند. به طور مشابه ، سلطه گر آنی یک گره n پس تسلط از n است که به هیچ وجه تسلط هیچ یک از پس تسلط های دیگر n را ندارد.
در استفاده از این سوئیچ مشکلی در دستورات scanf و printf وجود دارد. برای رفع آن دستورات printf را که در روند اجرای برنامه تاثیری ایجاد نمی کنند را کامنت کرده، و به جای دریافت ورودی از کاربر با دستور scanf متغیرها را بصورت مستقیم مقدار دهی می کنیم.
برای استفاده از این سوئیچ نیز در بخش Terminal از دستور زیر استفاده می کنیم :
خروجی این دستور نیز فایل .dot است که در کنار فایل برنامه ایجاد می گردند. برای تبدیل این فایل ها به فرمت PDF و مشاهده نمودار آن از دستور زیر استفاده می کنیم :
dot -Tpdf main.main.dot > Postdom.pdf
و خروجی آن بصورت زیر است :
سوئیچ Slicing :
برش برنامه عبارت است از محاسبه مجموعه اظهارات برنامه ، برش برنامه ، كه ممكن است بر مقادیر در بعضی از نقاط مورد علاقه تأثیر بگذارد ، از آن به عنوان معیار برش استفاده می شود. برش برنامه می تواند در اشکال زدایی برای یافتن منبع خطاها آسان تر مورد استفاده قرار گیرد. سایر کاربردهای برش شامل نگهداری نرم افزار ، بهینه سازی ، آنالیز برنامه و کنترل جریان اطلاعات است.
برای استفاده از این سوئیچ در بخش Terminal از دستور زیر استفاده می کنیم :
خروجی این دستور بصورت یک فایل متنی است که در کنار فایل کد برنامه ذخیره می گردد و بصورت زیر خواهد بود :
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing Array.c (with preprocessing) Array.c:45:[kernel] warning: Variable-sized local variable arr [slicing] slicing requests in progress... [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization __fc_errno ∈ [--..--] __fc_stdin ∈ {{ NULL ; &S___fc_stdin[0] }} __fc_stdout ∈ {{ NULL ; &S___fc_stdout[0] }} __fc_fopen[0..511] ∈ {0} __fc_p_fopen ∈ {{ &__fc_fopen[0] }} S___fc_stdin[0..1] ∈ [--..--] S___fc_stdout[0..1] ∈ [--..--] Array.c:45:[value] allocating variable __malloc_main_l45 Array.c:45:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype [value] using specification for function printf_va_2 Array.c:48:[value] entering loop for the first time [value] using specification for function printf_va_3 [value] using specification for function scanf_va_1 Array.c:7:[value] warning: accessing uninitialized left-value. assert \initialized(arr + 0); Array.c:9:[value] entering loop for the first time Array.c:10:[value] warning: accessing uninitialized left-value. assert \initialized(arr + i); Array.c:11:[value] warning: accessing uninitialized left-value. assert \initialized(arr + i); [value] using specification for function printf_va_4 Array.c:20:[value] warning: detected recursive call (sum_array_elements <- sum_array_elements :: Array.c:55 <- main) Use -val-ignore-recursive-calls to ignore (beware this will make the analysis unsound) [value] user error: Degeneration occurred: results are not correct for lines of code that can be reached from the egeneration point. [slicing] initializing slicing ... [slicing] interpreting slicing requests from the command line... [pdg] computing for function main [from] Computing for function __fc_vla_alloc [from] Done for function __fc_vla_alloc [from] Computing for function printf_va_2 [from] Done for function printf_va_2 [from] Computing for function printf_va_3 [from] Done for function printf_va_3 [from] Computing for function scanf_va_1 [from] Done for function scanf_va_1 [from] Computing for function largest_element [from] Done for function largest_element [from] Computing for function printf_va_4 [from] Done for function printf_va_4 [from] Computing for function sum_array_elements [from] Computing for function sum_array_elements <-sum_array_elements [from] Done for function sum_array_elements [from] Non-terminating function sum_array_elements (no dependencies) [from] Done for function sum_array_elements Array.c:58:[pdg] warning: no final state. Probably unreachable... [pdg] done for function main [slicing] applying all slicing requests... [slicing] applying 0 actions... [slicing] applying all slicing requests... [slicing] applying 1 actions... [slicing] applying actions: 1/1... [slicing] exporting project to 'Slicing export'... [slicing] applying all slicing requests... [slicing] applying 0 actions... [sparecode] remove unused global declarations from project 'Slicing export tmp' [sparecode] removed unused global declarations in new project 'Slicing export' [slicing] warning: call to deprecated function '-slice-print'. Should use '<normal slicing command> -then-on 'Slicing export' -print' instead. /* Generated by Frama-C */ #include "stdio.h" void main(void) { int *arr; unsigned int __lengthof_arr; int count = 10; __lengthof_arr = (unsigned int)count; int n = (int)((sizeof(int) * __lengthof_arr) / sizeof(*(arr + 0))); return; }
سوئیچ WP :
افزونه WP ضعیف ترین حساب پیش شرط را برای حاشیه نویسان ACSL از طریق برنامه های C اجرا می کند.
برای هر یادداشت کد ، این تکنیک مجموعه ای از تعهدات اثبات را ایجاد می کند ، یعنی. فرمول منطقی مرتبه اول ریاضی است که می تواند به اثباتگرهای قضیه خودکار مانند Alt-Ergo یا دستیاران اثبات تعامل مانند Coq ارسال شود. سایر پیش نمایش ها نیز از طریق پلتفرم why پشتیبانی می شوند.
برای استفاده از این سوئیچ نیز از بخش Terminal استفاده و دستور زیر را اجرا می کنیم :
خروجی این دستور نیز بصورت فایل متنی در کنار فایل کد ذخیره و بصورت زیر خواهد بود :
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing Array.c (with preprocessing) Array.c:45:[kernel] warning: Variable-sized local variable arr [wp] Running WP plugin... Array.c:42:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, enerating default assigns from the prototype Array.c:42:[kernel] warning: Neither code nor specification for function __fc_vla_free, enerating default assigns from the prototype [wp] warning: Missing RTE guards Array.c:29:[wp] warning: Missing assigns clause (assigns 'everything' instead) Array.c:38:[wp] warning: Missing assigns clause (assigns 'everything' instead) Array.c:28:[wp] warning: Missing assigns clause (assigns 'everything' instead) Array.c:50:[wp] warning: Allocation, initialization and danglingness not yet implemented (\initialized(param0)) Array.c:45:[wp] warning: Cast with incompatible pointers types (source: sint32*) (target: int8*) Array.c:48:[wp] warning: Missing assigns clause (assigns 'everything' instead) Array.c:45:[wp] warning: Cast with incompatible pointers types (source: sint8*) (target: int32*) [wp] 2 goals scheduled [wp] [Qed] Goal typed_main_assert_alloca_bounds : Valid [wp] [Alt-Ergo] Goal typed_bubble_sort_call_printf_va_1_pre : Timeout (Qed:25ms) (10s) [wp] Proved goals: 1 / 2 Qed: 1 (0.57ms) Alt-Ergo: 0 (interrupted: 1)
