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

コンパイル オプションの効率的な収集

Polyspace® 検証は、コンパイル段階またはリンク作成段階で次の理由により停止する場合があります。

  • Polyspace コンパイラは C または C++ 規格 (コンパイラの選択によって異なります) に厳密に準拠します。Polyspace 解析で使用される C/C++ 言語規格を参照してください。この規格からの逸脱がコンパイラで許容されている場合、Polyspace の既定のオプションを使用したコンパイルではコンパイラをエミュレートできません。

  • コンパイラが、標準の型とは異なる引数や戻り値の型をもつ標準ライブラリ関数を宣言しています。この関数の定義も指定しない場合、Polyspace では検証の効率を高めるため、通常のプロトタイプをもつ標準ライブラリ関数の独自の定義が使用されます。型の不一致は、リンク エラーの原因になります。

コンパイル エラーや標準ライブラリ関数のエラーは簡単に回避できます。エラーを回避するには、通常、特定の解析オプションを指定します。場合によっては、数行のコードを追加しなければならない場合があります。次に例を示します。

  • コンパイラの動作を厳密にエミュレートするには、ターゲットおよびコンパイラのオプションを指定します。それでもコンパイル エラーが発生する場合は、オプション [プリプロセッサ定義] (-D) を使用して、認識されない特定のキーワードを置き換えたり、削除したりしなければならない場合があります。ただし、このオプションでは、文字列を別の文字列へと単純に置き換えることのみ可能です。より複雑な置き換えの場合、#define ステートメントをコードに追加しなければならない場合があります。

  • 標準ライブラリ関数のスタブ化によるエラーを回避するには、#define を使って特定の Polyspace 固有マクロを定義し、Polyspace が標準ライブラリ関数の独自の定義を使用しないようにしなければならない場合があります。

この変更を元のコードに追加する代わりに、変更をすべて含む polyspace.h ファイルを 1 つ作成します。オプション [インクルード] (-include) を使用して、検証対象のすべてのソース ファイルで polyspace.h ファイルを強制的にインクルードさせることができます。

この方法には以下の利点があります。

  • リンクまたは後続の段階ではなく、コンパイル中にエラーが検出されるため、エラー検出がさらに高速になる。

  • 元のソース ファイルを変更する必要なし。

  • このファイルは元の .c ファイルの最初のファイルとして自動的にインクルードされる。

  • このファイルは同じ環境で開発が行われている他のプロジェクトでも再利用可能。

例1 例

これはオプション [インクルード] (-include) と共に使用可能なファイルの例です。

// The file may include (say) a standard include file implicitly 
// included by the cross compiler 

#include <stdlib.h> 
#include "another_file.h" 

// Workarounds for compilation errors
#define far 
#define at(x) 

// Workarounds for errors due to redefining standard library functions

#define POLYSPACE_NO_STANDARD_STUBS    // use this flag to prevent the
           //automatic stubbing of std functions 
#define __polyspace_no_sscanf 
#define __polyspace_no_fgetc 
void sscanf(int, char, char, char, char, char); 
void fgetc(void);

参考

トピック