https://virgool.io/feed/@soodehmahmoodi سوده محمودی fa 2026-06-17 04:59:41 https://static.virgool.io/images/default-avatar.jpg https://virgool.io/@soodehmahmoodi https://virgool.io/@soodehmahmoodi/%D8%AA%D8%B3%D8%AA-%D9%86%D8%B1%D9%85-%D8%A7%D9%81%D8%B2%D8%A7%D8%B1-%D8%AA%D9%88%D8%B3%D8%B7-%D8%A7%D8%A8%D8%B2%D8%A7%D8%B1-frama-c-nov7x32fuz3o در این نوشته به ابزار توسعه یافته frama-c در حوزه کیفیت نرم افزار می پردازیم و می آموزیم چگونه با در اختیار داشتن کد برنامه ها می توان ورودی هایی تولید کرد که به کمک آنها معیارهای مختلف پوشش برنامه ها را برآورده نموده و مشکلات موجود را شناسایی کرد.این ابزار در محیط سیستم عامل لینوکس و برای نرم افزار های تهیه شده به زبان C قابل استفاده می باشد. برای استفاده در سایر سیستم های عامل نیز می توان از ماشین های مجازی اعم از Virtual Box یا Virtual Machine استفاده کرد.نصب frama-c :برای نصب از ماشین مجازی Virtual Box و نسخه 18.04 سیستم عامل ubuntu استفاده کرده ایم.برای نصب ابزار از دستور زیر استفاده می‌کنیم:sudo apt-get install frama-cبرای اجرای محیط CLI و محیط گرافیکی نرم‌افزار به ترتیب دستورات زیر اجرا می‌شود:frama-cframa-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.cdigraph 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; __retresMetrics:آنالیزهای 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 = 3PDG:در علم کامپیوتر ، نمودار وابستگی به برنامه (PDG) یک نمایش است ، که از نماد نمودار استفاده می کند و وابستگی به داده ها و وابستگی های کنترل را آشکار می کند. از این وابستگی ها در بهینه سازی کامپایلرها برای ایجاد دگرگونی ها در هنگام تجزیه و تحلیل وابستگی استفاده می شود تا از هسته های چندگانه استفاده شود و موازی سازی بهبود می یابد.Generate dot files:frama-c -pdg -pdg-dot pref test.cGenerate graph from dot files:dot -Tps [dot-file-name] -o [output-file-name].psor in pdf format:dot –Tpdf [dot-file-name] > [output-file-name].pdfpost 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) s.mhmudi s.mhmudi Sun, 16 Feb 2020 13:40:57 +0330