このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

Polyspace ヘッダー ファイルの使用によるエラーの修正

問題

C/C++ ソース コードを Polyspace® で解析するときに、コンパイラ ヘッダーへのパスを指定していない場合、Polyspace は解析に独自バージョンのヘッダーを使用します。

場合によっては、これらの Polyspace ヘッダーによるコンパイル エラーが表示されます。通常、エラー メッセージでは polyspaceroot\polyspace\verifier\cxx\include のサブフォルダーの 1 つが示されます。ここで、polyspaceroot は Polyspace インストール フォルダーです。たとえば、C:\Program Files\Polyspace\R2025a です。通常、そのエラー メッセージは標準ライブラリ関数に関連しています。

たとえば、次の C++14 コードの解析時に std::is_empty でエラーが表示される場合があります。

#include <type_traits>

struct S final { };

bool f(void) {
    return std::is_empty<S>::value;
}
エラー メッセージは次のようになります。
Error: a "final" class type cannot be used as a base class
また、パス polyspaceroot\polyspace\verifier\cxx\include\include-libcxx\type_traits が示されます。このエラーが発生するのは、Polyspace ヘッダー ファイル内の std::is_empty の実装が final クラスを使用したインスタンス化を許可していない場合があるからです。

考えられる解決策

Polyspace 解析に対して、"コンパイラ ヘッダー ファイル" を含むフォルダーを指定します。

polyspace-configure を使用してビルド コマンドから Polyspace プロジェクトまたはオプション ファイルを作成すると、そのプロジェクトまたはオプション ファイルにコンパイラ ヘッダー パスが自動的に追加されます。そうでない場合は、次のようにこのパスを明示的に追加しなければなりません。

  • ユーザー インターフェイスで、このフォルダーをプロジェクトに追加します。

    詳細は、ユーザー インターフェイスでの Polyspace の実行を参照してください。

  • コマンド ラインで、コマンド polyspace-bug-finder または polyspace-bug-finder-server にフラグ -I を使用します。

    詳細は、-I を参照してください。

UNIX® ベースのプラットフォームで GNU® C でコンパイルする場合、/usr/include を使用します。組み込みコンパイラでは、ヘッダー ファイルは通常コンパイラ インストール フォルダーのサブフォルダーにあります。いくつかのコンパイラ用のインクルード フォルダーの例を次に示します。

  • Wind River® Diabたとえば、/apps/WindRiver/Diab/5.9.4/diab/5.9.4.8/include/ のような場合です。

  • IAR Embedded Workbench: たとえば、C:\Program Files\IAR Systems\Embedded Workbench 7.5\arm\inc のような場合です。

  • Microsoft® Visual Studio®:たとえば、C:\Program Files\Microsoft Visual Studio 14.0\VC\include のような場合です。

コンパイラのヘッダー ファイルへのパスについては、コンパイラのドキュメンテーションを参照してください。または、Polyspace 解析への標準ライブラリ ヘッダーの指定を参照してください。

参考

トピック