2

どのインクルード ファイルを使用するかをFrama-Cに伝える方法を決めるのに、いくつか問題があります。私は通常、オプションを追加します：

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

Frama-C の標準仕様を備えています。しかし、Frama-C ライブラリにないものが必要になることがよくあります。

たとえば、解析したいソース ファイルの 1 つは で定義されているマクロを使用しています<sys/wait.h>が、Frama-C には独自の があるためframa-c/libc/sys/wait.h、gcc ファイルは含まれていません。残念ながら、Frama-C はマクロを定義しておらず、最終的に定義が失われています。もちろん、ソース ファイルを変更したくありません。

my_libc/sys/wait.hFrama-C ファイルを含み、GCC ファイルにないものをコピーできるファイルでローカル ディレクトリを構築することを考えていました。

次に使用します：

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

しかし、GCC インクルード ファイルから定義を抽出するのは非常に難しい可能性があるため、私のソリューションには少し不安があります...

どう思いますか？それは良い考えだと思いますか？より良い組織についてアドバイスはありますか?

4

1 に答える 1

2

この解決策は問題ないようです (gcc のヘッダーから定義を抽出するのは確かに複雑な場合がありますが、選択肢はあまりありません。ある時点でマクロを提供する必要があり、おそらくヘッダー全体を Frama で終わらせたくないでしょう。 -C)。

私は前処理の専門家ではありませんが、提案するオプションを使用して両方を含めることができるかどうかはわかりません.2つのmy_libc/sys/wait.hヘッダーになり、常に最初のヘッダーを選択します. 2 つの解決策があります。$FRAMAC_SHARE/libc/sys/wait.h-cpp-extra-argssys/wait.hcpp

  • 独自の標準ヘッダーを定義し (おそらく Frama-C の libc からのコピー アンド ペーストを使用)、それらのみを使用します。
  • #include <libc/sys/wait.h>、および haveを使用してヘッダーを定義し、ヘッダー-cpp-extra-args=... -I$(frama-c -print-path)の相対パスに関する混乱を避けます。

どちらの場合も、アプリケーションで使用されるすべてのヘッダーのファイルを提供する必要があることに注意してください。それらのほとんどが、対応する Frama-C ファイルへのリダイレクトまたはコピーにすぎない場合でも同様です。しかし、いくつかのシェル コマンドを実行する必要があると思います。

于 2012-11-12T13:35:56.507 に答える