如何指定Frama-C包含文件的路徑？

Question

我有一些問題來決定如何告訴Frama-C ，其中包括文件使用。我通常添加選項：

-cpp-extra-args="-I $(frama-c -print-path)/libc" 

爲了從Frama-C獲得標準規格。 但我經常需要的東西並不在郵資-C庫。

例如，我要分析的源文件的人使用它在<sys/wait.h>， 定義，但因爲郵資-C擁有自己的frama-c/libc/sys/wait.h，不包括海灣合作委員會的文件的宏。 不幸的是，郵資-C沒有定義宏，定義最終丟失。 當然，我不想更改源文件！

我想建立一個本地目錄 與my_libc/sys/wait.h文件，其中將包括 郵資-C文件，在其中我可以複製缺什麼從GCC文件 的。

我會再使用：

-cpp-extra-args="-I my_libc -I $(frama-c -print-path)/libc" 

但我有點被我的解決方案，因爲擔心這可能是相當棘手的來自GCC提取定義包括文件...

你覺得呢？這看起來不錯嗎？ 你有關於更好組織的建議嗎？

Answer 1

該解決方案似乎罰款（提取gcc的頭文件的定義確實是複雜的，但你沒有太多的選擇有：你必須在某個時候提供宏，你可能不希望把整個頭結束於Frama-C）。

我沒有預處理的專家，但我不知道，你就可以包括my_libc/sys/wait.h和$FRAMAC_SHARE/libc/sys/wait.h與-cpp-extra-args選項，您建議：你最終有兩個sys/wait.h頭和cpp始終會選擇第一個。我看到兩個解決方案：

• 你定義自己的標準頭（可能與郵資-C的libc中copy'n粘貼），並且只使用它們
• 定義你的頭，用#include <libc/sys/wait.h>，並有-cpp-extra-args=... -I$(frama-c -print-path)，避免混淆標題的相對路徑。

注意，在這兩種情況下，你必須由您的應用程序使用的所有頭提供的文件，即使他們大多僅僅是重定向或相應郵資-C文件的副本。但我想你應該用幾個shell命令來完成。