メインコンテンツ

-no-assumption-on-absolute-addresses

絶対アドレスの使用が有効であるという仮定の削除

構文

-no-assumption-on-absolute-addresses

説明

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

-no-assumption-on-absolute-addresses は、コードで使用されている絶対アドレスが有効であるという既定の仮定を削除します。このオプションを使用した場合、絶対アドレスをポインターに代入すると、検証でオレンジの [絶対アドレスの使用] チェックが生成されます。それ以外の場合、このチェックは既定でグリーンになります。

アドレスを代入するポインターの型によって、アドレスに格納される初期値が決まります。たとえば、アドレスを int* ポインターに代入する場合、このチェックの後の検証では、そのアドレスが指すメモリ ゾーンが int の値で初期化されると想定されます。値はデータ型 int で許容される任意の値になります。

ユーザー インターフェイス (Polyspace® デスクトップ製品のみ) では、[構成] ペインの [その他] フィールドにこのオプションを入力します。Otherを参照してください。

オプション -no-assumption-on-absolute-addresses を使用すると、コードのオレンジ チェックの数が増えることがあります。たとえば、次の表では、オプションを有効にするとオレンジ チェックが追加されることが説明されています。

[絶対アドレスの使用] がグリーン[絶対アドレスの使用] がオレンジ
void main() {
    int *p = (int *)0x32;
    int x;
    x=*p;
}

この例では、ソフトウェアにより以下が生成されます。

  • アドレス 0x32 がポインター p に代入されたときにグリーンの [絶対アドレスの使用] チェック。

  • ポインター p が読み取られたときにグリーンの [不適切にデリファレンスされたポインター] チェック。

    xint の変数に許容されるすべての値をもつ可能性があります。

void main() {
    int *p = (int *)0x32;
    int x;
    x=*p;
}

この例では、ソフトウェアにより以下が生成されます。

  • アドレス 0x32 がポインター p に代入されたときにオレンジの [絶対アドレスの使用] チェック。

  • ポインター p が読み取られたときにグリーンの [不適切にデリファレンスされたポインター] チェック。

    xint の変数に許容されるすべての値をもつ可能性があります。

[絶対アドレスの使用] チェックを最大限に利用するには、開発の初期段階でこのチェックを既定のグリーンのままにします。統合段階では、オプション -no-assumption-on-absolute-addresses を使用し、絶対メモリ アドレスのすべての使用を検出します。これらを参照し、アドレスが有効であることを確認します。

バージョン履歴

R2016a で導入