アサーションまたはメモリ割り当て関数に関連する Polyspace コンパイル警告の修正

問題

Polyspace^® では、解析の効率を高めるために標準ライブラリ関数の独自の実装を使用します。標準ライブラリ関数を再定義して関数本体を Polyspace に提供した場合、その定義が解析で使用されます。

ただし、一部の標準ライブラリ関数については、関数を再定義して関数本体を提供した場合でも、Polyspace の独自の実装が引き続き使用されます。これらの関数には、関数 assert やメモリ割り当て関数 (malloc、calloc、alloca など) が含まれます。

次のような警告メッセージが表示されます。

Body of routine "malloc" was discarded.

原因

これらの関数には Polyspace の解析において特別な意味があるため、再定義することは許可されていません。次に例を示します。

関数 malloc の Polyspace 実装では、malloc を使用して割り当てられたメモリが後で解放されるかどうかを確認できます。
assert の Polyspace 実装は、解析を強化するために内部で使用されます。

解決法

独自の再定義を特に使用する必要がない場合は、この警告を無視します。解析結果は、標準ライブラリ関数の元の仕様に準拠した Polyspace 実装に基づきます。

独自の再定義を使用する必要がある場合は、再定義した関数が元の関数と同様に動作することを確認したうえで、関数の名前を変更します。オプション [プリプロセッサ定義] (-D) を使用して、解析のためだけに関数の名前を変更できます。たとえば、関数 malloc の名前を my_malloc に変更するには、オプションの引数に malloc=my_malloc を使用します。