frama-c [內核]用戶錯誤：無效的符號

當我試圖獲得代碼的pdg時，我得到這個無效的符號錯誤，沒有幫助的行號。任何人都可以提出這個錯誤的含義嗎？請注意，代碼編譯並使用g ++運行問題是如何獲取此錯誤的確切行號。執行frama-c [內核]用戶錯誤：無效的符號

命令：

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.

來源

2015-12-18 uday kiran

-cpp-命令應該是一個預處理命令，而不是編譯。你應該使用''-C -E''而不是''-c''，而不是''-o''。 – Anne

郵資-C是指分析Ç代碼，而不是C++代碼。這些是兩種不同的語言，除非你編寫純C語言（注意一些在兩種語言中看起來在語法上相似的構造實際上具有不同的語義），Frama-C無法解析你的test.cpp文件。

另外，正如Anne在評論中提到的那樣，您給出的-cpp-command是不正確的：您已要求g++提供二進制文件，而Frama-C期待預處理C.事實上，錯誤行在您的日誌中提到：/tmp/test.cppe1a338.i:1:，但這是沒有意義的，因爲test.cppe1a338是一個二進制文件。使用合適的-cpp-command（例如Frama-C默認提供的一個），Frama-C將找到#line註釋，這將允許它在原始文件中的適當位置報告任何錯誤，而不是中間結果。

來源

2015-12-18 15:14:35 Virgile

frama-c [內核]用戶錯誤：無效的符號

回答

相關問題