Quote:Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C.
Frama-C gathers several static analysis techniques in a single collaborative framework. The collaborative approach of Frama-C allows static analyzers to build upon the results already computed by other analyzers in the framework. Thanks to this approach, Frama-C provides sophisticated tools, such as a slicer and dependency analysis.
06-03-2018, 01:28 PM (This post was last modified: 06-03-2018, 01:51 PM by mikikg.)
Nije los alat ali generalno svi integrisani alati za te potrebe (IDE) imaju vec to u sebi, za staticnu i za dinamicnu analizu code-a + profileri.
Trenutno radim nesto u Android Studio i tamo sam to sve video.
Inace ovaj Android Studio je jedan od najboljih IDE za razvoj koje sam video do sad, fenomenalan alat sa inteliSense ... Nezgodno je sto je predisponiran samo za razvoj Android aplikacija ...
Mislim moze u njemu bilo sta da se kodira u C/C++ ali njegova snaga dolazi kada se dotaknes Java-e i JNI wrappera pa ti u code-u to sve izlinkuje, daje ti precice do klasa/metoda, ima fine editore za XML i resurs fajlove, tu je i Cmake, Gradle, device explorer, vrhunski Android emulator i svasta jos ...
Three heavyweight plug-ins that are used by the other plug-ins:
Evolved Value analysis (EVA)
This plug-in computes variation domains for variables. It is quite automatic, although the user may guide the analysis in places. It handles a wide spectrum of C constructs. This plug-in uses abstract interpretation techniques.
Jessie and Wp, two deductive verification plug-ins
These plug-ins are based on weakest precondition computation techniques. They allow to prove that C functions satisfy their specification as expressed in ACSL. These proofs are modular: the specifications of the called functions are used to establish the proof without looking at their code.
The availability of the above three plug-ins make it possible to write additional plug-ins that provide a wide palette of possibilities with relatively little effort. Here is a non-exhaustive list of plug-ins that have already been written and are distributed with Frama-C. Note that some of these plug-ins are still in development.
For browsing unfamiliar code:
Impact analysis
This plug-in highlights the locations in the source code that are impacted by a modification.
Scope & Data-flow browsing
This plug-in allows the user to navigate the dataflow of the program, from definition to use or from use to definition.
Variable occurrence browsing
Also provided as a simple example for new plug-in development, this plug-in allows the user to reach the statements where a given variable is used.
Metrics calculation
This plug-in allows the user to compute various metrics from the source code.
For code transformation:
Semantic constant folding
This plug-in makes use of the results of the evolved value analysis plug-in to replace, in the source code, the constant expressions by their values. Because it relies on EVA, it is able to do more of these simplifications than a syntactic analysis would.
Slicing
This plug-in slices the code according to a user-provided criterion: it creates a copy of the program, but keeps only those parts which are necessary with respect to the given criterion.
Spare code: remove "spare code", code that does not contribute to the final results of the program.
E-ACSL: translate annotations into C code for runtime assertion checking.
For verifying functional specifications:
Aoraï: verify specifications expressed as LTL (Linear Temporal Logic) formulas
Other functionalities documented together with the EVA plug-in can be considered as verifying low-level functional specifications (inputs, outputs, dependencies,…)
For test-case generation:
PathCrawler automatically finds test-case inputs to ensure coverage of a C function. It can be used for structural unit testing, as a complement to static analysis or to study the feasible execution paths of the function.
For concurrent programs:
Mthread
This plug-in automatically analyzes concurrent C programs, using the EVA plug-in, taking into account all possible thread interactions. At the end of its execution, the concurrent behavior of each thread is over-approximated, resulting in precise information about shared variables, which mutex protects a part of the code, etc.
Front-end for other languages
Frama-Clang
This plug-in provides a C++ front-end to Frama-C, based on the clang compiler. It transforms C++ code into a Frama-C AST, which can then be analyzed by the plug-ins above. Note however that it is very experimental and only supports a subset of C++11
“If you think you are too small to make a difference, try sleeping with a mosquito.” - Dalai Lama XIV
