آموزش ابزار Frama-c برای آزمون نرم افزار

ابزار Frama-C مخفف (Framework for Modular Analysis of C programs) یا (چارچوب برای تجزیه و تحلیل مدولار برنامه های C) که جهت تحلیل کدهای برنامه به زبان c مورد استفاده می باشد.ابزار Frama-C مجموعه ای از آنالایزرهای برنامه قابل تعامل برای برنامه های C است.به عنوان آنالایزر استاتیک، برنامه ها را بدون اجرای آنها بازرسی می کند.این ابزار برای سیستم عامل های Mac و لینوکس ارائه شده و از طریق ماشین های مجازی همچون VM،Cygwin و یا WIndows Subsystem for Linux در ویندوز نیز قابل استفاده می باشد.من از سیستم عامل Ubuntu 18.04 LTS که بر روی VMware نصب کردم استفاده می کنم و آموزش بر اساس این سیستم عامل تهیه کردمسیستم عامل ubuntu نصب شده بر روی VMطریقه نصب Frama-cجهت نصب Frama-c در ubuntu ابتدا terminal را باز میکینم و با استفاده از دستور زیر نصب انجام می شودsudo apt-get update -y sudo apt-get install -y frama-cو تمام، frama-c بر روی سیستم عامل شما نصب شد. اکنون می توانیم به دو صورت از این ابزار استفاده نمایید یکی با استفاده از خط دستور terminal و دیگری محیط گرافیکی ابزار است.جهت مشاهده ی محیط گرافیکی درون terminal دستور زیر را وارد می نماییمframa-c-guiکه محیط آن به شکل زیر می باشدمحیط ابزار frama-cدر صورتی که در زمان اجرای frama-c-gui با خطای زیر مواجه شدیدGtk-Message: Failed to load module "canberra-gtk-module" خطای با استفاده از این دستور مشکل برطرف می شودsudo apt-get install libcanberra-gtk*شروع کارما در این بخش به بررسی call graph, inout, users, metrics, pdg, post dominators, slicing, WP بر روی سورس کد زبان C که در ادامه آن را قرار می دهم میپردازیم، هرچند برای تست نرم افزار آیتم های متنوعی وجود دارد اما ما فقط مواردی که گفتیم می پردازیمسورس برنامهسورس کدی که ما انتخاب کردیم، مرتب سازی انتخابی (Selection Sort ) می باشد که شامل دو تابع یکی جهت مرتب سازی و دیگر چاپ نتیجه در خروجی است.#include <stdio.h> void selection_sort(int a[],int n); void show_sort_output(int a[],int n); void main() { int a[30], n; int i; printf(&quot\nEnter size of an array: &quot); scanf(&quot%d&quot, &n); printf(&quot\nEnter elements of an array:\n&quot); for(i=0; i<n; i++) scanf(&quot%d&quot, &a[i]); selection_sort(a,n); printf(&quot\n\nAfter sorting:\n&quot); show_sort_output(a,n); } void selection_sort(int a[],int n) { int i, j, min, temp; for (i=0; i<n; i++) { min = i; for (j=i+1; j<n; j++) { if (a[j] < a[min] min = j; } temp = a[i]; a[i] = a[min]; a[min] = temp; } } void show_sort_output(int a[],int n) { int i; for(i=0; i<n; i++) printf(&quot\n%d&quot, a[i]); }برای ورود کد مورد نظر به ابزار در منو Projects گزینه New Project را انتخاب و فایل برنامه مورد نظر را انتخاب می کنیمایجاد پروژه جدید در Frama-cنمودار Call graph:یک نمودار جریان کنترل است، که بیانگر روابط فراخوان بین زیر خطوط در یک برنامه کامپیوتری است. به طور کلی فراخوانی متدها(پروسیجرها، توابع و ...) برنامه را نمایش می دهد.با استفاده از محیط گرافیکی:جهت مشاهده call graph سورس کد خودمان از منوی Analyses گزینه show callgraph را انتخاب می کنیم call graph در frama-cنتیجه به شکل زیر می باشدcall graphبا استفاده از terminal:همچنین می توان با استفاده از دستور زیر درون terminal نتیجه را به صورت متنی ذخیره کردframa-c-gui -cg call_graph.txt main.cکه call_graph.txt فایل خروجی می باشد و main.c سورس کد برنامهتست ورودی و خروجی inout:جهت به دست آوردن ورودی ها و خروجی از هر یک از توابع برنامه مورد استفاده قرار می گیردبا استفاده از محیط گرافیکی:برای تهیه inout برنامه ابتدا به منو Analyses رفته سپس بر روی Analyses کلیک کرده و از منوی سمت چپ inout را کلیک کرده و مقادیر out, input, inout را انتخاب کرده و نتیجه در کنسول به نمایش در خواهد آمد.به عنوان مثال بخشی از نتیجه تولید شده در console برای تابع selection_sort به شکل زیر می باشد، که در آن ورودی ها و خروجی های این تابع را بررسی کرده است[inout] Out (internal) for function selection_sort: a[0..29]; i; j; min; temp [inout] Inputs for function selection_sort: a[0..29] [inout] InOut (internal) for function selection_sort: Operational inputs: a[0..29]; a; n Operational inputs on termination: a[0..29]; a; n Sure outputs: iبا استفاده از terminal: می توانیم با استفاده از دستور زیر درون terminal نتیجه را به صورت متنی ذخیره کنیمframa-c -inout main.c > inout.txtبا اجرای دستور بالا همان نتایج تولید شده درون consol در بخش گرافیک ابزار درون فایل inout.txt ذخیره می شوندآزمون کاربران users:این آزمون توابع فراخوانی شده، printf ها و scanf های یک تابع را نشان میدهد.با استفاده از محیط گرافیکی:برای استفاده از این آزمون در منو Analyses گزینه Analyses را انتخاب کرده و در پنجره باز شده گزینه users را انتخاب میکنیم سپس مقدار user- را انتخاب کرده و بر روی execute کلیک می کنیم تا در کنسول نتیجه تولید شود.frama-c users نتیجه ی این آزمون بر روی سورس کد ما به شکل زیر می باشدshow_sort_output: printf_va_4 main: selection_sort show_sort_output printf_va_1 scanf_va_1 printf_va_2 scanf_va_2 printf_va_3 printf_va_4از این خروجی متوجه می شویم که هر یک از توابع ما چه توابعی صدا زدن، چه دستورات ورودی و خرجی داشتن(printf و scanf)، برای مثال تابع main توابع selection_sortو show_sort_output را صدا زده است و همچنین دارای دو printf و یک scanf هست.با استفاده از terminal: می توانیم با استفاده از دستور زیر درون terminal نتیجه را به صورت متنی ذخیره کنیمframa-c -users main.c > user.txtآنالیز metric:در Metrics اطلاعاتی نظیر تعداد توابع، entry point، حلقه های تکرار، شرط ها و ... را به دست بیاورید.جهت بدست آوردن metric از دستور زیر استفاده می کنیمframa-c main.c -metricsکه main.c نام سورس کد ما هستش، جهت ذخیره خروجی درون فایل txt از دستور زیر استفاده می کنیمframa-c main.c -metrics > metric.txtخروجی به شکل زیر می باشد: Defined functions (3) ===================== main (0 call); selection_sort (1 call); show_sort_output (1 call); Undefined functions (6) ======================= printf_va_1 (1 call); printf_va_2 (1 call); printf_va_3 (1 call); printf_va_4 (1 call); scanf_va_1 (1 call); scanf_va_2 (1 call); 'Extern' global variables (0) ============================= Potential entry points (1) ========================== main; Global metrics ============== Sloc = 39 Decision point = 5 Global variables = 0 If = 5 Loop = 4 Goto = 0 Assignment = 13 Exit point = 3 Function = 9 Function call = 8 Pointer dereferencing = 7 Cyclomatic complexity = 8همانطور که مشاهده می نمایید ما سه تابع داریم، نقطه ی ورود ما تابع main است، 5 شرط، 4 حلقه، 3 نقطه ی خرج و .... داریمآنالیز metricآنالیز PDG:گراف PDG گراف وابستگی برنامه یا Program Dependence Graph، یک گراف تولید شده از وابستگی های داده ای و وابستگی اجرایی دستورات نسبت به هم تهیه می شوند.برای استخراج PDG ابتدا سورس کد را به قالب فایل dot تبدیل کرده و سپس آن به pdf تبدیل می کنیم، برای اینکار به شکل زیر عمل میکنیم:با استفاده از دستور زیر فایل .dot را تولید کردهframa-c -pdg -pdg-dot graph -pdg-print main.c > pdg.dotسپس با دستور زیر آن را به pdf تبدیل می کنیمdot -Tpdg graph.main.dot > pdg.pdfخروجی pdgآنالیز Postdominators:در Post Dominator دستوراتی که بر روی دستورات دیگر تاثیر میگذارد را مشخص می کنیم و به شکل یک گراف به نمایش داده می شود. این آنالیز با scanf و printf مشکل دارد و باعث ایجاد خطا می شود برای استفاده از این آنالیز، من ورودی را دستی وارد کردم و حذف scanf ها، همچنین کامنت کردن دستورات printf که سورس کد به شکل زیر تغییر کرد:#include <stdio.h> void selection_sort(int a[],int n); void show_sort_output(int a[],int n); void main() { int a[30], n; int i; //printf(&quot\nEnter size of an array: &quot); //scanf(&quot%d&quot, &n); n=5; //printf(&quot\nEnter elements of an array:\n&quot); for(i=0; i<n; i++) a[i]=i; selection_sort(a,n); //printf(&quot\n\nAfter sorting:\n&quot); show_sort_output(a,n); } void selection_sort(int a[],int n) { int i, j, min, temp; for (i=0; i<n; i++) { min = i; for (j=i+1; j<n; j++) { if (a[j] < a[min]) min = j; } temp = a[i]; a[i] = a[min]; a[min] = temp; } } void show_sort_output(int a[],int n) { int i; //for(i=0; i<n; i++) //printf(&quot\n%d&quot, a[i]); }با استفاده از دستور زیر گراف تولید می نماییمframa-c main.c -dot-postdom mainو با استفاده از دستور زیر آن را به pdf تبدیل می کنیمdot -Tpdf main.main.dot > postdom.pdfخروجی:Postdominatorsبرش بندی یا Slicingیک برش از برنامه حاوی دستوراتی از آن است که ویژگیهای مشخصی از برنامه را به نمایش میگذارد.. برشبندی برای اولین بار برای یافتن عامل بروز خرابی برنامهها ارائه شد؛ اما بعد از آن، کاربردهای مختلفی پیدا کرد. برای مثال، برای یافتن دو برنامه که از نظر معنایی به یکدیگر شباهت دارند میتوان از برشبندی استفاده نمود. به همینترتیب، برای یافتن میزان چسبندگی یک برنامه از برشبندی استفاده میکنند.در Slicing بر اساس تعیین یک متغیر میتوان دستوراتی که بر روی آن متغیر تاثیر مستقیم و یا غیر مستقیم دارند را شناسایی کنیم.برش بندی را می توان به دو صورت wr و rd انجام دهیم که در ادامه تفاوت این دو را مشاهده می نماییدبا استفاده از دستور زیر بر روی متغیر a ، slicing انجام میدهیم و عبارت wr به این معنی میباشد که در متغیر مورد نظر نوشته شده است.frama-c -slice-wr a main.c -slice-print > slice_a_wr.txtیا با دستور زیر بر روی متغیر a و عبارت rd به این معنی می باشد که از متغیر مورد نظر خوانده شده است(استفاده شده است)frama-c -slice-rd a main.c -slice-print > slice_a_rd.txtهمانطور که در تصویر مشخص است در فایل سمت چب بر اساس rd متغیر a تولید شده است تابع show_sort_output نیز آورده شده است ولی در برش wr وجود ندارد.آنالیز WP:خواص را به صورت قیاسی تأیید می کند، بر پارامتر کردن با توجه به مدل حافظه تمرکز دارد. WP طوری طراحی شده است که برنامه C را مستقیماً به زبان Why وارد می کند ، با سایر افزونه های Frama-C مانند افزونه تجزیه و تحلیل ارزش همکاری می کند. WP می تواند به صورت اختیاری از پلت فرم Why3 برای استناد به بسیاری از پیش بینی های خودکار و تعاملی دیگر استفاده کند.برای تهیه WP باید از طریق ترمینال دستور زیر را اعمال نماییم.frama-c -wp -wp-rte main.c > wp.txtخروجی تولید شده:[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing main.c (with preprocessing) [wp] Running WP plugin... [rte] annotating function main [rte] annotating function selection_sort [rte] annotating function show_sort_output main.c:12:[wp] warning: Allocation, initialization and danglingness not yet implemented (\initialized(param0)) main.c:11:[wp] warning: Missing assigns clause (assigns 'everything' instead) main.c:9:[wp] warning: Allocation, initialization and danglingness not yet implemented (\initialized(param0)) main.c:23:[wp] warning: Missing assigns clause (assigns 'everything' instead) main.c:20:[wp] warning: Missing assigns clause (assigns 'everything' instead) main.c:36:[wp] warning: Missing assigns clause (assigns 'everything' instead) [wp] 20 goals scheduled [wp] [Qed] Goal typed_main_call_scanf_va_1_pre : Valid [wp] [Alt-Ergo] Goal typed_main_assert_rte_signed_overflow : Valid [wp] [Alt-Ergo] Goal typed_main_call_scanf_va_1_pre_2 : Timeout (Qed:4ms) (10s) [wp] [Alt-Ergo] Goal typed_main_call_printf_va_1_pre : Timeout (Qed:2ms) (10s) [wp] [Alt-Ergo] Goal typed_main_call_printf_va_2_pre : Timeout (Qed:18ms) (10s) (Stronger) [wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_signed_overflow : Valid [wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access : Unknown (Qed:5ms) (204ms) [wp] [Alt-Ergo] Goal typed_main_call_scanf_va_2_pre : Timeout (Qed:9ms) (10s) (Stronger) [wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_signed_overflow_2 : Valid [wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access_2 : Unknown (Qed:5ms) (153ms) [wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access_4 : Unknown (Qed:5ms) (205ms) [wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access_3 : Unknown (Qed:5ms) (204ms) [wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access_6 : Valid [wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access_5 : Unknown (Qed:5ms) (255ms) [wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_signed_overflow_3 : Unknown (Qed:7ms) (182ms) [wp] [Alt-Ergo] Goal typed_show_sort_output_assert_rte_mem_access : Unknown (Qed:7ms) (154ms) [wp] [Alt-Ergo] Goal typed_show_sort_output_assert_rte_signed_overflow : Valid [wp] [Alt-Ergo] Goal typed_main_call_printf_va_3_pre : Timeout (Qed:8ms) (10s) (Stronger) [wp] [Alt-Ergo] Goal typed_main_call_scanf_va_2_pre_2 : Timeout (Qed:8ms) (10s) (Stronger) [wp] [Alt-Ergo] Goal typed_show_sort_output_call_printf_va_4_pre : Timeout (Qed:6ms) (10s) [wp] Proved goals: 6 / 20 Qed: 1 (0.47ms-5ms-10ms) Alt-Ergo: 5 (8ms-19ms) (47) (interrupted: 7) (unknown: 7)