I have just started learning FramaC for testing of IOT programs. Is there a way to analyse large programs such as IoT OS in Frama C efficiently? How to import single modules without compiling for analysis as the presence of header files is causing errors.How can we import only certain modules and then analyze them. Any advice would be appreciated. Thank You.
root@nirnai:/home/vboxuser# frama-c-gui
Error creating proxy: The connection is closed (g-io-error-quark, 18)
Error creating proxy: The connection is closed (g-io-error-quark, 18)
Error creating proxy: The connection is closed (g-io-error-quark, 18)
Error creating proxy: The connection is closed (g-io-error-quark, 18)
Error creating proxy: The connection is closed (g-io-error-quark, 18)
(frama-c-gui:2821): dconf-WARNING **: 16:22:40.318: failed to commit changes to dconf: The connection is closed
/home/vboxuser/Downloads/RIOT-master/core/thread.c:29:10: fatal error: thread.h: No such file or directory
29 | #include "thread.h"
| ^~~~~~~~~~
compilation terminated.
(frama-c-gui:2821): dconf-WARNING **: 16:22:50.987: failed to commit changes to dconf: The connection is closed
You can't avoid having all the #include needed to analyze a C source file. In fact Frama-C uses an external pre-processor (GNU cpp by default), and this pre-processor needs to be provided all the appropriate headers. On the other hand, depending on the kind of analysis you want to do, you may be able to analyze C source files one by one or not: typically the WP plug-in provides a modular analysis, while an Eva analysis usually requires having the body of all the functions that can be called from the entry point you have chosen.
Now, in order for us to give a more meaningful answer, you need to show us exactly how you intend to parse your source files with Frama-C, that is by using the command line tool and not the menu in the GUI. Usually, you need to provide some pre-processing directives, either via the -cpp-extra-args option or a compilation database file and the -json-compilation-database option. Chapter 5 of the Frama-C user manual explains in detail how to provide the appropriate pre-processing arguments. In addition, Chapter 12 introduces the various scripts that help setting up an appropriate environment for analyzing complex projects with Frama-C.
On a side note (because of the #include <thread.h> in your question), note that Frama-C is not equipped now to deal with multi-threaded programs: depending on whether a shared memory variable is declared volatile or not, analyses will either assume that the value is completely unknown or will only change when assigned explicitly in the code (i.e. ignoring possible interaction from another thread).