مقاله‌ی زیر به همراه خلاصه آن در وب‌سایت ویکیپدیا آمده است. موضوع آن را مشخص کنید

مقاله: frama-c دارای یک معماری پلاگین مدولار قابل‌مقایسه با eclipse (نرم‌افزار) یا gimp است. frama-c برای تولید یک درخت نحو انتزاعی به cil (c intermediate language) متکی است. درخت نحوی انتزاعی از یادداشتهای نوشته‌شده در زبان خصوصیات ansi / iso c ((acsl پشتیبانی می‌کند. چندین ماژول می‌توانند درخت ترکیبی انتزاعی را برای افزودن حاشیه‌نویسی (ansi / iso c (acsl زبان اضافه کنند. در میان اغلب استفاده می‌شود افزونه‌های عبارتند از: تجزیه و تحلیل ارزش (value analysis) - یک مقدار یا مجموعه‌ای از مقادیر ممکن را برای هر متغیر در یک برنامه محاسبه می‌کند. این افزونه از تکنیک‌های تفسیر انتزاعی استفاده می‌کند و بسیاری از افزونه‌های دیگر از نتایج آن استفاده می‌کنند. جسی (jessie) - خواص را به صورت قیاسی تأیید می‌کند. جسی برای اطمینان از ارسال تعهدات اثبات‌شده به پیش پرده‌های قضیه اتوماتیک مانند z ۳، simplify، alt-ergo یا قضیه تعاملی مانند coq یا چرا، به پشتیبان چرا یا why ۳ تکیه می‌کند. با استفاده از جسی، اجرای حباب مرتب‌سازی یا سیستم رای گیری الکترونیکی اسباب‌بازی می‌تواند ثابت شود که مشخصات مربوط به آنها را برآورده می‌کند. از یک الگوی حافظه جدایی با الهام از منطق جدایی استفاده می‌کند. wp (ضعیف‌ترین پیش‌شرط) - مشابه جسی، خواص را به صورت قیاسی تأیید می‌کند. بر خلاف جسی، بر پارامتر کردن با توجه به مدل حافظه تمرکز دارد. wp طوری طراحی‌شده است که برخلاف جسی که برنامه c را مستقیما به زبان why وارد می‌کند، با سایر افزونه‌های frama-c مانند افزونه تجزیه و تحلیل ارزش همکاری می‌کند. wp می‌تواند به صورت اختیاری از پلت فرم why ۳ برای استناد به بسیاری از پیش بینی‌های خودکار و تعاملی دیگر استفاده کند. آنالیز تاثیرات (impact analysis) - تأثیرات تغییر در کد منبع c را برجسته می‌کند. برش (slicing) - برش برنامه را قادر می‌سازد. این برنامه تولید یک برنامه جدید c کوچکتر است که برخی از ویژگی‌های داده‌شده را حفظ می‌کند. کد یدکی (spare code) - کد بی‌فایده را از یک برنامه c حذف می‌کند. سایر افزونه‌ها عبارتند از: سلطه گرها (dominators) - سلطه گران و پیشفرض اظهارات را محاسبه می‌کند. از تحلیل (from analysis) - وابستگی‌های عملکردی را محاسبه می‌کند. frama-c برای اهداف زیر قابل‌استفاده است: برای درک کد c که شما ننوشتید. به طور خاص، …
خلاصه: 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 نیست. 
موضوع:
فراما سی