s.mhmudi
s.mhmudi
خواندن ۱۱ دقیقه·۵ سال پیش

تست نرم افزار توسط ابزار frama-c

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

این ابزار در محیط سیستم عامل لینوکس و برای نرم افزار های تهیه شده به زبان C قابل استفاده می باشد. برای استفاده در سایر سیستم های عامل نیز می توان از ماشین های مجازی اعم از Virtual Box یا Virtual Machine استفاده کرد.

نصب frama-c :

برای نصب از ماشین مجازی Virtual Box و نسخه 18.04 سیستم عامل ubuntu استفاده کرده ایم.برای نصب ابزار از دستور زیر استفاده می‌کنیم:

sudo apt-get install frama-c

برای اجرای محیط CLI و محیط گرافیکی نرم‌افزار به ترتیب دستورات زیر اجرا می‌شود:

frama-c

frama-c-gui

برای مشاهده پلاگین‌های موجود دستور زیر اجرا می‌شود:

frama-c -plugins

در ادامه دستورات تولید خروجی‌های مورد انتظار آورده شده است. همچنین از کد زیر که به زبان C نوشته شده است، برای انجام آزمایش استفاده می کنیم:

#include <stdio.h>
int square(int x);
int calculateResult(int a, int b);
int main()
{	int result = calculateResult(2, 3);
	return 0;}
int square(int x)
{	return x*x;}
int calculateResult(int a, int b)
{	int result = square(a) + square(b);
	return result;}

Call graph:

یک نمودار جریان کنترل است ، که بیانگر روابط فراخوان بین زیر خطوط در یک برنامه کامپیوتری است . هر گره یک روال را نشان می دهد و هر لبه (f، g) نشان می دهد که روش f فراخوانی g را فراخوانی می کند. بنابراین ، یک چرخه در نمودار ، تماسهای رویه بازگشتی را نشان می دهد.

برای اجرای این نمودار بر روی کد فوق، بعد از انتخاب فایل کد مربوطه در ابزار frama-c ، در منو Analyses گزینه show callgraph را انتخاب می کنیم تا نمودار مورد نظر تولید گردد :

frama-c-gui -cg [output-text-call-graph-file-name] test.c

digraph G {
  ratio=0.500000;
  &quotUV square (657)&quot [color=&quot#80E090&quot, label=&quotsquare&quot, style=&quotbold&quot, ];
  &quotUV calculateResult (663)&quot [color=&quot#80E090&quot, label=&quotcalculateResult&quot,
                              shape=diamond, style=&quotbold&quot, ];
  &quotUV main (666)&quot [color=&quot#00E050&quot, label=&quotmain&quot, shape=diamond,
                   style=&quotbold&quot, ];
  
  subgraph cluster_663 { color=&quot#80E090&quot label=&quotS 663&quot style=&quotbold&quot &quotUV calculateResult (663)&quot&quotUV square (657)&quot
     };
  subgraph cluster_666 { color=&quot#00E050&quot label=&quotS 666&quot style=&quotbold&quot &quotUV main (666)&quot
     };
  
  &quotUV calculateResult (663)&quot -> &quotUV square (657)&quot [color=&quot#80E090&quot, ];
  &quotUV main (666)&quot -> &quotUV calculateResult (663)&quot [color=&quot#00E050&quot, ];
  
  }

Inout:

این تست با ایجاد ورودی ها و خروجی های متغیر برنامه مورد نظر را بررسی می کند.

جهت انجام این آزمایش در برنامه در منو Analyses گزینه Analyses را انتخاب کرده و در پنجره باز شده گزینه inout را انتخاب و گزینه های مربوط به ورودی و خروجی را انتخاب می کنیم:

Frama-c –inout test.c

[inout] InOut (internal) for function square:
        Operational inputs:
          x
        Operational inputs on termination:
          x
        Sure outputs:
          __retres
[inout] InOut (internal) for function calculateResult:
        Operational inputs:
          a; b
        Operational inputs on termination:
          a; b
        Sure outputs:
          result; tmp; tmp_0
[inout] InOut (internal) for function main:
        Operational inputs:
          \nothing
        Operational inputs on termination:
          \nothing
        Sure outputs:
          result; __retres


Metrics:

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

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

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

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

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

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

Frama-c –metrics test.c

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

[metrics] Defined functions (3)
          =====================
           calculateResult (1 call); main (0 call); square (2 calls); 
          
          Undefined functions (0)
          =======================
           
          
          'Extern' global variables (3)
          =============================
           __FC_errno; __fc_stdin; __fc_stdout
          
          Potential entry points (1)
          ==========================
           main; 
          
          Global metrics
          ============== 
          Sloc = 10
          Decision point = 0
          Global variables = 5
          If = 0
          Loop = 0
          Goto = 0
          Assignment = 3
          Exit point = 3
          Function = 3
          Function call = 3
          Pointer dereferencing = 0
          Cyclomatic complexity = 3


PDG:

در علم کامپیوتر ، نمودار وابستگی به برنامه (PDG) یک نمایش است ، که از نماد نمودار استفاده می کند و وابستگی به داده ها و وابستگی های کنترل را آشکار می کند. از این وابستگی ها در بهینه سازی کامپایلرها برای ایجاد دگرگونی ها در هنگام تجزیه و تحلیل وابستگی استفاده می شود تا از هسته های چندگانه استفاده شود و موازی سازی بهبود می یابد.

Generate dot files:

frama-c -pdg -pdg-dot pref test.c

Generate graph from dot files:

dot -Tps [dot-file-name] -o [output-file-name].ps

or in pdf format:

dot –Tpdf [dot-file-name] > [output-file-name].pdf


post dominators:

در نمودارهای جریان کنترلی ، گره d بر گره n غالب است (dominates) اگر هر مسیری از گره ورودی به n باید از d عبور کند. از نظر نشانه گذاری، به صورت d dom n (یا گاهی اوقات d >> n) نوشته می شود.

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

در استفاده از این سوئیچ مشکلی در دستورات scanf و printf وجود دارد. برای رفع آن دستورات printf را که در روند اجرای برنامه تاثیری ایجاد نمی کنند را کامنت کرده، و به جای دریافت ورودی از کاربر با دستور scanf متغیرها را بصورت مستقیم مقدار دهی می کنیم.

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

frama-c -dot-postdom pd test.c

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


Slicing:

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

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

frama-c -slice-rd result -print test.c

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

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test.c (with preprocessing)
[slicing] slicing requests in progress...
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] 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}
  __p_fc_fopen ∈ {{ &__fc_fopen[0] }}
  S___fc_stdin[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
              [--..--]
              [0].[bits 80 to 95] ∈ UNINITIALIZED
              [0].__fc_flags ∈ [--..--]
              [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdin[0] }}
              [0].__fc_real_data ∈
              {{ NULL ; &S___fc_real_data_0_S___fc_stdin[0] }}
              {[0].__fc_real_data_max_size; [1]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof}} ∈
              [--..--]
              [1].[bits 80 to 95] ∈ UNINITIALIZED
              [1].__fc_flags ∈ [--..--]
              [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdin[0] }}
              [1].__fc_real_data ∈
              {{ NULL ; &S___fc_real_data_1_S___fc_stdin[0] }}
              [1].__fc_real_data_max_size ∈ [--..--]
  S___fc_inode_0_S___fc_stdin[0..1] ∈ [--..--]
  S___fc_real_data_0_S___fc_stdin[0..1] ∈ [--..--]
  S___fc_inode_1_S___fc_stdin[0..1] ∈ [--..--]
  S___fc_real_data_1_S___fc_stdin[0..1] ∈ [--..--]
  S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
               [--..--]
               [0].[bits 80 to 95] ∈ UNINITIALIZED
               [0].__fc_flags ∈ [--..--]
               [0].__fc_inode ∈
               {{ NULL ; &S___fc_inode_0_S___fc_stdout[0] }}
               [0].__fc_real_data ∈
               {{ NULL ; &S___fc_real_data_0_S___fc_stdout[0] }}
               {[0].__fc_real_data_max_size; [1]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof}} ∈
               [--..--]
               [1].[bits 80 to 95] ∈ UNINITIALIZED
               [1].__fc_flags ∈ [--..--]
               [1].__fc_inode ∈
               {{ NULL ; &S___fc_inode_1_S___fc_stdout[0] }}
               [1].__fc_real_data ∈
               {{ NULL ; &S___fc_real_data_1_S___fc_stdout[0] }}
               [1].__fc_real_data_max_size ∈ [--..--]
  S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
  S___fc_real_data_0_S___fc_stdout[0..1] ∈ [--..--]
  S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
  S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
[value] computing for function calculateResult <- main.
        Called from test.c:10.
[value] computing for function square <- calculateResult <- main.
        Called from test.c:21.
[value] Recording results for square
[value] Done for function square
[value] computing for function square <- calculateResult <- main.
        Called from test.c:21.
[value] Recording results for square
[value] Done for function square
[value] Recording results for calculateResult
[value] Done for function calculateResult
[value] Recording results for main
[value] done for function main
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[slicing] warning: No internal slicing request from the command line.
[slicing] warning: Adding an extra request on the entry point of function: main.
[pdg] computing for function main
[from] Computing for function calculateResult
[from] Computing for function square <-calculateResult
[from] Done for function square
[from] Done for function calculateResult
[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'
/* Generated by Frama-C */
typedef __builtin_va_list va_list;
typedef unsigned int size_t;
typedef unsigned int ino_t;
typedef unsigned int gid_t;
typedef unsigned int uid_t;
typedef long time_t;
typedef unsigned int blkcnt_t;
typedef unsigned int blksize_t;
typedef unsigned int dev_t;
typedef unsigned int mode_t;
typedef unsigned int nlink_t;
typedef long off_t;
struct stat {
   dev_t st_dev ;
   ino_t st_ino ;
   mode_t st_mode ;
   nlink_t st_nlink ;
   uid_t st_uid ;
   gid_t st_gid ;
   dev_t st_rdev ;
   off_t st_size ;
   time_t st_atime ;
   time_t st_mtime ;
   time_t st_ctime ;
   blksize_t st_blksize ;
   blkcnt_t st_blocks ;
};
struct __fc_pos_t {
   unsigned long __fc_stdio_position ;
};
typedef struct __fc_pos_t fpos_t;
struct __fc_FILE {
   unsigned int __fc_stdio_id ;
   fpos_t __fc_position ;
   char __fc_error ;
   char __fc_eof ;
   int __fc_flags ;
   struct stat *__fc_inode ;
   unsigned char *__fc_real_data ;
   int __fc_real_data_max_size ;
};
typedef struct __fc_FILE FILE;
extern int __FC_errno;
extern FILE *__fc_stdin;
extern FILE *__fc_stdout;
/*@ assigns \nothing; */
extern int remove(char const *filename);
/*@ assigns \nothing; */
extern int rename(char const *old_name, char const *new_name);
/*@ ensures
      \result ≡ \null ∨
      (\valid(\result) ∧ \fresh{Old, Here}(\result,sizeof(FILE)));
    assigns \nothing;
 */
extern FILE *tmpfile(void);
/*@ assigns \result, *(s+(..));
    assigns \result \from *(s+(..));
    assigns *(s+(..)) \from \nothing;
 */
extern char *tmpnam(char *s);
/*@ requires \valid(stream);
    ensures \result ≡ 0 ∨ \result ≡ -1;
    assigns \result;
    assigns \result \from stream, stream->__fc_stdio_id;
 */
extern int fclose(FILE *stream);
/*@ requires stream ≡ \null ∨ \valid_read(stream);
    ensures \result ≡ 0 ∨ \result ≡ -1;
    assigns \result;
    assigns \result \from stream, stream->__fc_stdio_id;
 */
extern int fflush(FILE *stream);
FILE __fc_fopen[512];
FILE * const __p_fc_fopen = __fc_fopen;
/*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
    assigns \result;
    assigns \result \from *(filename+(..)), *(mode+(..)), __p_fc_fopen;
 */
extern FILE *fopen(char const *filename, char const *mode);
/*@ ensures
      \result ≡ \null ∨
      (\valid(\result) ∧ \fresh{Old, Here}(\result,sizeof(FILE)));
    assigns \result;
    assigns \result \from fildes, *(mode+(..));
 */
extern FILE *fdopen(int fildes, char const *mode);
/*@ ensures \result ≡ \null ∨ \result ≡ \old(stream);
    assigns *stream;
 */
extern FILE *freopen(char const *filename, char const *mode, FILE *stream);
/*@ assigns *stream;
    assigns *stream \from buf; */
extern void setbuf(FILE *stream, char *buf);
/*@ assigns *stream;
    assigns *stream \from buf, mode, size; */
extern int setvbuf(FILE *stream, char *buf, int mode, size_t size);
/*@ assigns *stream;
    assigns *stream \from stream->__fc_stdio_id; */
extern int fprintf(FILE *stream, char const *format , ...);
/*@ assigns *stream;
    assigns *stream \from stream->__fc_stdio_id; */
extern int fscanf(FILE *stream, char const *format , ...);
/*@ assigns *__fc_stdout;
    assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ assigns *__fc_stdin; */
extern int scanf(char const *format , ...);
/*@ assigns *(s+(0 .. n-1)); */
extern int snprintf(char *s, size_t n, char const *format , ...);
/*@ assigns *(s+(0 ..)); */
extern int sprintf(char *s, char const *format , ...);
/*@ assigns *stream;
    assigns *stream \from *(format+(..)), arg; */
extern int vfprintf(FILE *stream, char const *format, va_list arg);
/*@ assigns *stream;
    assigns *stream \from *(format+(..)), *stream; */
extern int vfscanf(FILE *stream, char const *format, va_list arg);
/*@ assigns *__fc_stdout;
    assigns *__fc_stdout \from arg; */
extern int vprintf(char const *format, va_list arg);
/*@ assigns *__fc_stdin;
    assigns *__fc_stdin \from *(format+(..)); */
extern int vscanf(char const *format, va_list arg);
/*@ assigns *(s+(0 .. n-1));
    assigns *(s+(0 .. n-1)) \from *(format+(..)), arg;
 */
extern int vsnprintf(char *s, size_t n, char const *format, va_list arg);
/*@ assigns *(s+(0 ..));
    assigns *(s+(0 ..)) \from *(format+(..)), arg; */
extern int vsprintf(char *s, char const *format, va_list arg);
/*@ assigns *stream; */
extern int fgetc(FILE *stream);
/*@ ensures \result ≡ \null ∨ \result ≡ \old(s);
    assigns *(s+(0 .. n-1)), *stream, \result;
    assigns *(s+(0 .. n-1)) \from *stream;
    assigns *stream \from *stream;
    assigns \result \from s, n, *stream;
 */
extern char *fgets(char *s, int n, FILE *stream);
/*@ assigns *stream; */
extern int fputc(int c, FILE *stream);
/*@ assigns *stream;
    assigns *stream \from *(s+(..)); */
extern int fputs(char const *s, FILE *stream);
/*@ assigns \result, *stream;
    assigns \result \from *stream;
    assigns *stream \from *stream;
 */
extern int getc(FILE *stream);
/*@ assigns \result;
    assigns \result \from *__fc_stdin; */
extern int getchar(void);
/*@ ensures \result ≡ \old(s) ∨ \result ≡ \null;
    assigns *(s+(..)), \result;
    assigns *(s+(..)) \from *__fc_stdin;
    assigns \result \from s, __fc_stdin;
 */
extern char *gets(char *s);
/*@ assigns *stream;
    assigns *stream \from c; */
extern int putc(int c, FILE *stream);
/*@ assigns *__fc_stdout;
    assigns *__fc_stdout \from c; */
extern int putchar(int c);
/*@ assigns *__fc_stdout;
    assigns *__fc_stdout \from *(s+(..)); */
extern int puts(char const *s);
/*@ assigns *stream;
    assigns *stream \from c; */
extern int ungetc(int c, FILE *stream);
/*@ requires \valid((char *)ptr+(0 .. nmemb*size-1));
    requires \valid(stream);
    ensures \result ≤ \old(nmemb);
    ensures \initialized((char *)\old(ptr)+(0 .. \result*\old(size)-1));
    assigns *((char *)ptr+(0 .. nmemb*size-1)), \result;
    assigns *((char *)ptr+(0 .. nmemb*size-1)) \from size, nmemb, *stream;
    assigns \result \from size, *stream;
 */
extern size_t fread(void *ptr, size_t size, size_t nmemb, FILE *stream);
/*@ requires \valid_read((char *)ptr+(0 .. nmemb*size-1));
    requires \valid(stream);
    ensures \result ≤ \old(nmemb);
    assigns *stream, \result;
    assigns *stream \from *((char *)ptr+(0 .. nmemb*size-1));
    assigns \result \from *((char *)ptr+(0 .. nmemb*size-1));
 */
extern size_t fwrite(void const *ptr, size_t size, size_t nmemb, FILE *stream);
/*@ assigns *pos;
    assigns *pos \from *stream; */
extern int fgetpos(FILE *stream, fpos_t *pos);
/*@ assigns *stream, __FC_errno;
    assigns *stream \from offset, whence; */
extern int fseek(FILE *stream, long offset, int whence);
/*@ assigns *stream;
    assigns *stream \from *pos; */
extern int fsetpos(FILE *stream, fpos_t const *pos);
/*@ assigns \result, __FC_errno;
    assigns \result \from *stream;
    assigns __FC_errno \from *stream;
 */
extern long ftell(FILE *stream);
/*@ assigns *stream;
    assigns *stream \from \nothing; */
extern void rewind(FILE *stream);
/*@ assigns *stream;
    assigns *stream \from \nothing; */
extern void clearerr(FILE *stream);
/*@ assigns \result;
    assigns \result \from *stream; */
extern int feof(FILE *stream);
/*@ assigns \result;
    assigns \result \from *stream; */
extern int fileno(FILE *stream);
/*@ assigns *stream;
    assigns *stream \from \nothing; */
extern void flockfile(FILE *stream);
/*@ assigns *stream;
    assigns *stream \from \nothing; */
extern void funlockfile(FILE *stream);
/*@ assigns \result, *stream;
    assigns \result \from \nothing;
    assigns *stream \from \nothing;
 */
extern int ftrylockfile(FILE *stream);
/*@ assigns \result;
    assigns \result \from *stream; */
extern int ferror(FILE *stream);
/*@ assigns __fc_stdout;
    assigns __fc_stdout \from __FC_errno, *(s+(..)); */
extern void perror(char const *s);
/*@ assigns \result, *stream;
    assigns \result \from *stream;
    assigns *stream \from *stream;
 */
extern int getc_unlocked(FILE *stream);
/*@ assigns \result;
    assigns \result \from *__fc_stdin; */
extern int getchar_unlocked(void);
/*@ assigns *stream;
    assigns *stream \from c; */
extern int putc_unlocked(int c, FILE *stream);
/*@ assigns *__fc_stdout;
    assigns *__fc_stdout \from c; */
extern int putchar_unlocked(int c);
/*@ assigns *stream;
    assigns *stream \from \nothing; */
extern void clearerr_unlocked(FILE *stream);
/*@ assigns \result;
    assigns \result \from *stream; */
extern int feof_unlocked(FILE *stream);
/*@ assigns \result;
    assigns \result \from *stream; */
extern int ferror_unlocked(FILE *stream);
/*@ assigns \result;
    assigns \result \from *stream; */
extern int fileno_unlocked(FILE *stream);
int square(int x);
int calculateResult(int a, int b);
int main(void)
{
  int __retres;
  int result;
  result = calculateResult(2,3);
  __retres = 0;
  return __retres;
}
int square(int x)
{
  int __retres;
  __retres = x * x;
  return __retres;
}
int calculateResult(int a, int b)
{
  int result;
  int tmp;
  int tmp_0;
  { /* sequence */
    tmp = square(a);
    tmp_0 = square(b);
  }
  result = tmp + tmp_0;
  return result;
}

Users:

در این آزمون می توانیم مشاهده کنیم هر تابع چه توابعی را فراخوانی کرده است. برای استفاده از این آزمون در منو Analyses گزینه Analyses را انتخاب کرده و در پنجره باز شده گزینه users را انتخاب و گزینه های مربوط به ورودی و خروجی را انتخاب می کنیم و خروجی آن مطابق زیر است :

[users] ====== DISPLAYING USERS ======
        calculateResult: square
        main: square calculateResult
        ====== END OF USERS ==========

WP:

افزونه WP ضعیف ترین حساب پیش شرط را برای حاشیه نویسان ACSL از طریق برنامه های C اجرا می کند.

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

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

  • frama-c -wp -wp-rte test.c

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

[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_square_assert_rte_signed_overflow_2 : Unknown (66ms)
[wp] [Alt-Ergo] Goal typed_calculateResult_assert_rte_signed_overflow_2 : Unknown (60ms)
[wp] [Alt-Ergo] Goal typed_calculateResult_assert_rte_signed_overflow : Unknown (56ms)
[wp] Proved goals:    1 / 4
     Qed:             0 
     Alt-Ergo:        1  (24ms) (3) (unknown: 3)


framacتست نرم افزارابزارpdg
s.mhmudi
s.mhmudi
سوده محمودی
شاید از این پست‌ها خوشتان بیاید