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 حذف می کند.
این نوشته برگرفته از سایت ویکی پدیا می باشد، اگر نادرست یا توهین آمیز است، لطفا گزارش دهید: گزارش تخلفاین ابزار برای سیستم عامل های 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 حذف می کند.
wiki: فراما سی