構造体の不完全または部分的割り当てを許可する (-size-in-bytes)

メモリ バッファーが十分でないポインターが構造体を指すことを許可

説明

このオプションは Code Prover 解析のみに影響します。

検証において、構造体を指すけれども構造体の一部のフィールドに対してのみ十分なバッファーがあるポインターのデリファレンスを許可するように指定します。

このタイプのポインターは小さい構造体へのポインターがより大きな構造体のポインターにキャストされるときに生成されます。キャストによって生成されたポインターは、大きい方の構造体の一部のフィールドにのみ十分なバッファーをもちます。

オプションの設定

以下のいずれかの方法を使用してオプションを設定します。

  • Polyspace® ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [チェック動作] ノードを選択してから、このオプションを選択します。

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [チェック動作] ノードを選択してから、このオプションを選択します。

  • コマンド ラインとオプション ファイル: オプション -size-in-bytes を使用します。コマンド ライン情報を参照してください。

このオプションを使用する理由

このオプションを使用して、不適切にデリファレンスされたポインターのチェックを緩和します。構造体のすべてのフィールドに対して、ポインターに十分なバッファーが許可されていない場合でも、構造体をポイントすることができます。

設定

オン

バッファー不足のポインターがデリファレンスされるとき、デリファレンスが許可されたバッファー範囲内で発生するかぎり、Polyspace は [不適切にデリファレンスされたポインター] エラーを生成しません。

たとえば、次のコードではポインター p は構造体 BIG の最初の 2 つのフィールドに対して十分なバッファーがあります。したがって、オプションがオンに設定されている場合、Polyspace は最初の 2 つのデリファレンスを有効であると見なします。3 番目のデリファレンスにより、p は許可されたバッファーの範囲外になります。したがって、Polyspace は 3 番目のデリファレンスに対して [不適切にデリファレンスされたポインター] エラーを生成します。

#include <stdlib.h>
 
typedef struct _little { int a; int b; } LITTLE;
typedef struct _big { int a; int b; int c; } BIG;
 
void main(void) {
   BIG *p = malloc(sizeof(LITTLE));
 
   if (p!= ((void *) 0) ) {
      p->a = 0 ;    
      p->b = 0 ;
      p->c = 0 ;   // Red IDP check
     }
}
オフ (既定の設定)

構造体のすべてのフィールドに対して、ポインターに十分なバッファーがない場合、Polyspace はポインターの構造体へのデリファレンスを許可しません。最初にポインターをデリファレンスするときに、[不適切にデリファレンスされたポインター] エラーが発生します。

たとえば、次のコードでポインター p が構造体 BIG の最初の 2 つのフィールドに対して十分なバッファーがある場合でも、Polyspace は p のデリファレンスを無効であると見なします。

#include <stdlib.h>
 
typedef struct _little { int a; int b; } LITTLE;
typedef struct _big { int a; int b; int c; } BIG;
 
void main(void) {
   BIG *p = malloc(sizeof(LITTLE));
 
   if (p!= ((void *) 0) ) {
      p->a = 0 ;   // Red IDP check
      p->b = 0 ;
      p->c = 0 ;        
   }
}

ヒント

  • このオプションをオンに設定しない場合、部分的に割り当てされた構造体のフィールドにポインターを指すことはできません。

    たとえば、前述の例でオプションをオンに設定せずに割り当てを実行すると、

    int *ptr = &(p->a);
    Polyspace は割り当てを無効とみなします。ptr をデリファレンスすると、[不適切にデリファレンスされたポインター] エラーが発生します。

  • このオプションを使用すると、オレンジ チェックの数が若干増加する可能性があります。

コマンド ライン情報

パラメーター: -size-in-bytes
既定値: オフ
例 (Code Prover): polyspace-code-prover -sources file_name -size-in-bytes
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -size-in-bytes

参考

|

トピック