DIY Electronic projects
Frama-C Framework for Modular Analysis of C programs - Printable Version

+- DIY Electronic projects (https://forum.yu3ma.net)
+-- Forum: IT (https://forum.yu3ma.net/forumdisplay.php?fid=63)
+--- Forum: Sigurnost i zaštita (https://forum.yu3ma.net/forumdisplay.php?fid=64)
+--- Thread: Frama-C Framework for Modular Analysis of C programs (/showthread.php?tid=1917)



Frama-C Framework for Modular Analysis of C programs - 1van - 06-03-2018

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.

https://frama-c.com/

[Image: attachment.php?aid=26825]


RE: Frama-C Framework for Modular Analysis of C programs - mikikg - 06-03-2018

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 ...


RE: Frama-C Framework for Modular Analysis of C programs - 1van - 06-03-2018

Quote:Available plug-ins (https://frama-c.com/plugins.html)

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