frama-c [kernel]用户错误:符号无效

Question

当我试图获得一个代码的pdg时，我得到了这个无效的符号错误，没有帮助行号。有谁能暗示这个错误是什么意思吗？请注意，代码编译和运行时带有g++的问题是如何获取此错误的确切行号。

已执行命令：

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

错误消息：

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

Answer 1

Frama-C用于分析C代码，而不是C++代码。这是两种不同的语言，除非您编写纯C语言(注意，在两种语言中看起来语法相似的一些结构实际上具有不同的语义)，否则Frama-C无法解析您的test.cpp文件。

此外，正如Anne在评论中提到的，您给出的日志是不正确的:您要求g++提供一个二进制文件，而Frama-C需要经过预处理的C。事实上，错误行在您的日志中提到：/tmp/test.cppe1a338.i:1:，但这是没有意义的，因为test.cppe1a338是一个二进制文件。使用适当的-cpp-command (比如Frama-C默认给你的注释)，Frama-C将找到#line注释，这将允许它在原始文件中的适当位置报告任何错误，而不是中间结果。