frama-c [kernel] user error: Invalid symbol

Question

When am trying to get pdg of a code i am getting this invalid symbol error wiht no line numbers for help. Can any one suggest what this error means? note that code compiles and runs with g++ Question is how to get exact line number for this error.

command executed:

frama-c -continue-annot-error -kernel-verbose 3  -no-annot -no-frama-c-stdlib -cpp-command " /usr/bin/g++  -iquote../../inc -std=c++11 fPIC -Wno-write-strings -Wno-narrowing  -gdwarf-3  -o test.o -c" -pdg -pdg-dot test -pdg-print test.cpp

Error message :

[kernel] computing the AST
[kernel] parsing
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing /usr/local/share/frama-c/libc/__fc_builtin_for_normalization.i to Cabs
[kernel] Parsing /usr/local/share/frama-c/libc/__fc_builtin_for_normalization.i
[kernel] Converting /usr/local/share/frama-c/libc    /__fc_builtin_for_normalization.i from Cabs to CIL
[kernel] Parsing test.cpp (with preprocessing)
[kernel] Parsing /tmp/test.cppe1a338.i to Cabs
[kernel] Parsing /tmp/test.cppe1a338.i
/tmp/test.cppe1a338.i:1:[kernel] user error: Invalid symbol
[kernel] user error: stopping on file "test.cpp"
                 that has errors.
[kernel] Frama-C aborted: invalid user input.

The -cpp-command is supposed to be a preprocessing command, not a compilation on. You should use something like -C -E instead of -c, and no -o. — Anne

Virgile Virgile · Accepted Answer · 2015-12-18T15:14:35

Frama-C is meant to analyze C code, not C++ code. These are two different languages, and unless you write plain C (with the caveat that some constructions that look syntactically similar in both languages have in fact different semantics), there is no way Frama-C can parse your test.cpp file.

In addition, as mentioned by Anne in comment, the -cpp-command you have given is incorrect: you have asked g++ to provide a binary file, whereas Frama-C is expecting pre-processed C. As a matter of fact, the error line is mentioned in your log: /tmp/test.cppe1a338.i:1:, but this is meaningless since test.cppe1a338 is a binary file. With an appropriate -cpp-command (such as the one Frama-C gives you by default), Frama-C will find #line annotations which will allow it to report any error at the appropriate location in the original file instead of the intermediate result.

frama-c [kernel] user error: Invalid symbol

1 Answers