|
Frama-C stands for ''Framework for Modular Analysis of C programs''. Frama-C is a set of interoperable program analyzers for C programs. Frama-C has been developed by Commissariat à l'Énergie Atomique et aux Énergies Alternatives and Inria. Frama-C enables the analysis of C programs without executing them. == Architecture == Frama-C has a modular plugin architecture comparable to that of Eclipse (software) or GIMP. Frama-C relies on CIL (C Intermediate Language) to generate an abstract syntax tree. The abstract syntax tree supports annotations written in ANSI/ISO C Specification Language (ACSL). Several modules can manipulate the abstract syntax tree to add ANSI/ISO C Specification Language (ACSL) annotations. Among frequently used plugins are: * ''Value analysis'' computes a value or a set of possible values for each variable in a program. This plugin uses abstract interpretation techniques and many other plugins make use of its results. * ''Jessie'' verifies properties in a deductive manner. Jessie relies on the Why or Why3 back-end to enable proof obligations to be sent to automatic theorem provers like Z3, Simplify, Alt-Ergo or interactive theorem provers like Coq or Why. Using Jessie, (an implementation of bubble-sort ) or (a toy e-voting system ) can be proved to satisfy their respective specifications. It uses a separation memory model inspired by separation logic. * ''WP'' similar to ''Jessie'', verifies properties in a deductive manner. Unlike Jessie, it focuses on parameterization with regards to the memory model. WP is designed to cooperate with other Frama-C plugins such as the value analysis plug-in, unlike Jessie that compiles the C program directly into the Why language. WP can optionally use the Why3 platform to invoke many other automated and interactive provers. * ''Impact analysis'' highlights the impacts of a modification in the C source code. * ''Slicing'' enables slicing of a program. It enables generation of a smaller new C program that preserves some given properties. * ''Spare code'' removes useless code from a C program. Other plugins are: * ''Dominators'' computes dominators and postdominators of statements. * ''From analysis'' computes functional dependencies. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Frama-C」の詳細全文を読む スポンサード リンク
|