فراما-سی

**Frama-C**  مخفف (Framework for Modular Analysis of C programs) یا (چارچوب برای تجزیه و تحلیل مدولار برنامه های C) که جهت *تجزیه و تحلیل مدولار [[سی (زبان برنامه‌نویسی)|برنامه های C است]]* . Frama-C مجموعه ای از آنالایزرهای برنامه قابل تعامل برای برنامه های C است . Frama-C توسط کمیساریای فرانسوی l’Énergie Atomique et aux Énergies Alternatives ( لیست CEA )  و Inria توسعه یافته است . همچنین از ابتکار عمل زیرساخت های هسته ای بودجه دریافت کرده است. Frama-C ، به عنوان آنالایزر استاتیک ، برنامه ها را بدون اجرای آنها بازرسی می کند. با وجود نام آن ، این نرم‌افزار مربوط به پروژه فرانسوی Framasoft نیست .
این ابزار برای سیستم عامل های Mac و لینوکس ارائه شده و از طریق ماشین های مجازی همچون VM،Cygwin و یا WIndows Subsystem for Linux در ویندوز نیز قابل استفاده می باشد.

## معماری
Frama-C دارای یک معماری پلاگین مدولار  قابل مقایسه با Eclipse (نرم‌افزار) یا GIMP است .

Frama-C برای تولید یک درخت نحو انتزاعی به CIL ( C Intermediate Language ) متکی است . درخت نحوی انتزاعی از یادداشتهای نوشته شده در زبان خصوصیات ANSI / ISO C ((ACSL پشتیبانی می کند.

چندین ماژول می توانند درخت ترکیبی انتزاعی را برای افزودن حاشیه نویسی (ANSI / ISO C (ACSL زبان اضافه کنند . در میان اغلب استفاده می شود افزونه های عبارتند از:
* *تجزیه و تحلیل ارزش(Value analysis) -* یک مقدار یا مجموعه ای از مقادیر ممکن را برای هر متغیر در یک برنامه محاسبه می کند. این افزونه از تکنیک های تفسیر انتزاعی استفاده می کند و بسیاری از افزونه های دیگر از نتایج آن استفاده می کنند.
* *جسی(Jessie) -* خواص را به صورت قیاسی تأیید می کند. جسی برای اطمینان از ارسال تعهدات اثبات شده به پیش پرده های قضیه اتوماتیک مانند Z3 ، Simplify ، Alt-Ergo یا قضیه تعاملی مانند Coq یا چرا ، به پشتیبان چرا  یا Why3 تکیه می کند. با استفاده از جسی ، اجرای حباب مرتب سازی یا سیستم رای گیری الکترونیکی اسباب بازی می تواند ثابت شود که مشخصات مربوط به آنها را برآورده می کند. از یک الگوی حافظه جدایی با الهام از منطق جدایی استفاده می کند .
* *WP (ضعیف ترین پیش شرط)* - مشابه *جسی* ، خواص را به صورت قیاسی تأیید می کند. بر خلاف جسی ، بر پارامتر کردن با توجه به مدل حافظه تمرکز دارد. WP طوری طراحی شده است که برخلاف جسی که برنامه C را مستقیماً به زبان Why وارد می کند ، با سایر افزونه های Frama-C مانند افزونه تجزیه و تحلیل ارزش همکاری می کند. WP می تواند به صورت اختیاری از پلت فرم Why3 برای استناد به بسیاری از پیش بینی های خودکار و تعاملی دیگر استفاده کند.
* *آنالیز تاثیرات(Impact analysis)* - تأثیرات تغییر در کد منبع C را برجسته می کند.
* *برش(Slicing)* - برش برنامه را قادر می سازد. این برنامه تولید یک برنامه جدید C کوچکتر است که برخی از ویژگی های داده شده را حفظ می کند. 
* *کد یدکی(Spare code)* - کد بی فایده را از یک برنامه C حذف می کند.

سایر افزونه ها عبارتند از:
* *سلطه گرها(Dominators)* - سلطه گران و پیشفرض اظهارات را محاسبه می کند.
* *از تحلیل(From analysis)* - وابستگی های عملکردی را محاسبه می کند.

## امکانات
Frama-C برای اهداف زیر قابل استفاده است:
* برای درک کد C که شما ننوشتید. به طور خاص ، Frama-C به شما امکان می دهد مجموعه ای از مقادیر را مشاهده کند ، برنامه را به برنامه های کوتاه تر تقسیم کند و در برنامه حرکت کند.
* برای اثبات خصوصیات رسمی روی کد. با استفاده از مشخصات نوشته شده در زبان مشخصات ANSI / ISO C ، آن را قادر می سازد تا از خواص کد برای هرگونه رفتار احتمالی اطمینان حاصل کند. Frama-C شماره های شناور را کنترل می کند. 
* برای اجرای استانداردهای کدگذاری یا قراردادهای کد در کد منبع C ، با استفاده از افزونه های سفارشی 
* برای تهیه کد C در برابر برخی نقص های امنیتی 

## نحوه ی نصب frama-c
* ubuntu

جهت نصب بر روی ubuntu می توان مانند زیر عمل نمایید ابتدا terminal را باز می کنیم و با استفاده از دستور زیر نصب انجام می شود
```shell
sudo apt-get update -y

sudo apt-get install -y frama-c
```
نصب با استفاده از opam برای نصب frama-c به روش opam به شکل زیر است. Opam یک Package Manager برای OCamle است. برای نصب opam از دستور زیر استفاده میشود:
```shell
sudo apt-get install opam
```
Frama-c یک سری dependency های غیر OCamle ای از جمله Gtk و GMP دارد. در بسیاری از سیستم ها opam میتواند این وابستگی های خارجی را با پلاگین depext فراهم کند. برای استفاده از depext اینگونه عمل میکنیم:
```shell
opam install depext
opam depext frama-c
```
اگر سیستم توسط depext پشتیبانی نشود باید Gtk, GtkSourceView, GnomeCanvas و GMP جداگانه نصب شوند.
```shell
opam install frama-c
```

* Fedora

۱- برای نصب Frama-C نیاز به مخزن RPM Fusion داریم در صورتی که این مخزن نصب نیست از طریق مراحل زیر اقدام به نصب نمایید.

۱-۱- باید ابتدا به سایت rpm fusion رفته به آدرس rpmfusion.org رفته و بر اساس معماری Fedora خود مخزن را دانلود نمایید.

۲-۱- پس از دانلود در ترمینال سیستم عامل با دستور rpm -ivh مخزن را نصب نمایید.

۲- سپس باید مخزن را آپدیت نمایید از طریق دستور dnf update میتوانید به جدید ترین پکیج ها دسترسی داشته باشید.

۳- سپس باید پکیج های مختلف شامل jcc و glibc و ++G را نصب نماییم برای نصب هر یک کافیست از دستور
```shell
dnf install [package name]
```
مثال :
```shell
dnf install jcc

dnf install glibc

dnf install g++
```
۴- در ادامه پس از نصب تمام پکیج های مورد نیاز بالا باید پکیج xkit را نصب کنید که مشابه دستورهای بالا قابل انجام خواهد بود.

۵- سپس به سایت frama-c رفته به آدرس frama-c.com و نسخه frama-c را بر اساس نوع سیستم عامل و معماری آن دانلود نمایید.

۶- سپس باید فایل tar را uncompress کنید ( توضیحات بیشتر برای استفاده از دستور tar )

۷- برای بهبود GUI برنامه Frama-c باید از پکیج Bladez از طریق دستور dnf install bladez نصب کنید.

۸- داخل پوشه extract شده frama-c رفته و ترمینال را باز کرده و با دستور install/. برنامه را نصب کنید.


## محیط frama-c
جهت مشاهده محیط گرافیکی frama-c کافیست در ترمینال دستور زیر را وارد نمایید
```shell
frama-c-gui
```

## منابع

## پیوند به بیرون
* 
* لیست بحث فریم-سی
* سیستم ردیابی اشکال Frama-C

رده:ابزارهای تحلیل ایستای برنامه
رده:ابزارهای روش‌های صوری
رده:ابزارهای آزمون نرم‌افزار
رده:زبان‌های برنامه‌نویسی خانواده سی
رده:نرم‌افزارهای دارای پروانه ال‌جی‌پی‌ال
رده:نرم‌افزارهای لینوکس