5

I need to use frama-c value analysis plug-in to analyze some projects. These projects use CMake build infrastructure as their build system.

I have used frama-c to analyze each file separately. This way, the information about the entry point will be lost. More precisely, frama-c requires an entry point for the files that do not include a "main" function and therefore it is challenging to cover all functions and choose the best entry point within a single file from the project.

My question is that is there a way that we can run frama-c on the entire project as a whole unit (not file by file)?

Mehrnoosh EP
  • 161
  • 7

1 Answers1

4

Frama-C accepts multiple files on its command-line. This will work if the configuration of the preprocessor (option -cpp-extra-args, used in particular for includes) is the same accross all files.

If you need different preprocessor settings for different files, you should preprocess each file alone (only cpp, no Frama-C), and save each result as a .i file. Then, you can supply all those preprocessed files to Frama-C simultaneously. Usually, the first operation can be done by tweaking the build process.

byako
  • 3,372
  • 2
  • 21
  • 36
  • Thanks for your great solution, it worked! I just have a question about saving the preprocessed file. When I use the command "frama-c -cpp-command 'gcc -C -E -I. -o %2 %1' small.c small.i", frama-c complains that small.i does not exist and considers it as another input, not the output file name! For now I was able to get the preprocessed result using -print option, but that prints some extra kernel messages as well, which is not as desirable. What is your suggestion for saving .i file? Thanks! @byako – Mehrnoosh EP Feb 17 '16 at 03:34
  • 2
    @MehrnooshEP you don't have to provide the name of the intermediate `.i` file in this setting, frama-c will take care of that itself. It is only if you choose to pre-process a C file outside of frama-c that you need to save a `.i` file and give it as input to Frama-C. In other word, you can do either `frama-c -cpp-command bla file.c` or `cpp -o file.i file.c && frama-c file.i`, but **not** `frama-c -cpp-command bla file.c file.i` – Virgile Feb 17 '16 at 08:03
  • @Virgile I see, I was mixing the two! Thanks for the explanation. – Mehrnoosh EP Feb 17 '16 at 19:41