Search code examples
frama-c

How do i analyse a complex project like open62541?

I am a student and currently trying to analyse the reference implementation for the OPC Ua protocol in C with cppcheck and frama-c. My goal is not to do very dedicated testing but more some general/basic tests to see if there are some obvious issues with the code.

The project can be found here

I am running a VM with Ubuntu 19.10 and Frama-C version 20.0 (Calcium).

The steps i performed are as follows:

git clone https://github.com/open62541/open62541.git
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 /path/to/source
frama-c -json-compilation-database /path/to/compile_commands.json

Until now everything works as expected and there are no Errors.

However now i am having trouble understanding how to continue. Do i need to do my analysis on all files seperately or is it possible to throw in the whole project like with cppcheck?

How would i approach this in general? Do i need to to analyse all files step by step?

For example i tried:

frama-c -json-compilation-database /path/to/compilation_commands.json -val /path/to/open62541/src/

which returns:

[kernel] Parsing src (with preprocessing)
gcc: warning: /path/to/open62541/src/: linker input file unused because linking not done
[kernel] User Error: cannot find entry point `main'.
  Please use option `-main' for specifying a valid entry point.
[kernel] Frama-C aborted: invalid user input.

So apperantly frama-c requires an entry point, however i do not know which entry point i need to specify.

Any help regarding this is much appreciated. I apologize for my lack of understanding. This is my first project of this kind and i am a little bit overwhelmed by frama-c and the complexity of the open62541 project.

Solution

  • Do i need to do my analysis on all files separately or is it possible to throw in the whole project like with cppcheck?

    Frama-C can actually analyze the entire project in one go provided multiple files do not define the same symbols. See http://blog.frama-c.com/index.php?post/2018/01/25/Analysis-scripts%3A-helping-automate-case-studies, paragraph "Setting sources and testing parsing":

    The list of source files to be given to Frama-C can be obtained from the compile_commands.json file. However, it is often the case that the software under analysis contains several binaries, each requiring a different set of sources. The JSON compilation database does not map the sources used to produce each binary, so it is not always possible to entirely automate the process.

    The key point in your case is that the compilation_commands.json instructs Frama-C on how to parse each file, but you must still supply the files you want to see parsed yourself. With your current command-line, Frama-C tries to interpret /path/to/open62541/src/ as a file (and fails), and has no other file to parse. This is why you get the error User Error: cannot find entry point 'main'.

    Thus, you must specify the files you want to parse on the command-line. This can be done in two ways:

    I used the first approach, but I suggest you use the second, as frama-c-script is very helpful to start a first analysis.

    Once you have done this listing step, you will encounter at least three more problems:

    • Frama-C will choke on # include <sys/param.h>, because this file is not present in the standard C library bundled with Frama-C. Either remove this include in the source files, or add an empty sys/param.h somewhere
    • some .c files refer to generated headers that are not present in the git repo of open62541. So you will need to compile the repo to get those headers before launching Frama-C.
    • Frama-C will also choke on the definition of the macro UA_STATIC_ASSERT in architecture_definitions.h. I did not investigate whether one of the definitions was accepted, and I simply defined it to the empty macro.

    After all this, you should be good to go.