-asm-begin -asm-end

コンパイラ固有の asm 関数の解析からの除外

構文

-asm-begin "mark1[,mark2,...]" -asm-end "mark1[,mark2,...]"


説明

-asm-begin "mark1[,mark2,...]" -asm-end "mark1[,mark2,...]" は、コンパイラ固有のアセンブリ言語のソース コード関数を解析から除外します。これら 2 つのオプションは一緒に使用しなければなりません。

Polyspace^® は、ほとんどのインライン アセンブラーを既定で認識します。このオプションは、アセンブリ コードの開始が原因でコンパイル エラーが発生する場合にのみ使用してください。詳細については、アセンブリ コードに関する Code Prover の仮定を参照してください。

問題となるコード ブロックを 2 つの #pragma 命令によってマークします。1 つはアセンブリ コードの最初に、もう 1 つは最後に置きます。コマンドの使用に際しては、-asm-begin のマークの順序が -asm-end のマークの順序と同じになるようにします。

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

例

コードのブロックを #pragma start1 および #pragma end1 で区切ります。これらの名前は、それぞれのオプションにおいて同じ順序でなければなりません。次のいずれかとなります。

-asm-begin "start1" -asm-end "end1"

または

-asm-begin "mark1,...markN,start1" -asm-end "mark1,...markN,end1"

次の例では、2 つの関数 foo_1 および foo_2 を除外するようマークします。

コード:

#pragma asm_begin_foo
int foo(void) { /* asm code to be ignored by Polyspace */ }
#pragma asm_end_foo

#pragma asm_begin_bar
void bar(void) { /* asm code to be ignored by Polyspace */ }
#pragma asm_end_bar

Polyspace コマンド:

• Bug Finder:

  polyspace-bug-finder -lang c -asm-begin "asm_begin_foo,asm_begin_bar"
            -asm-end "asm_end_foo,asm_end_bar"

• Code Prover:

  polyspace-code-prover -lang c -asm-begin "asm_begin_foo,asm_begin_bar"
           -asm-end "asm_end_foo,asm_end_bar"

• Bug Finder Server:

  polyspace-bug-finder-server -lang c -asm-begin "asm_begin_foo,asm_begin_bar"
            -asm-end "asm_end_foo,asm_end_bar"

• Code Prover Server:

  polyspace-code-prover-server -lang c -asm-begin "asm_begin_foo,asm_begin_bar"
           -asm-end "asm_end_foo,asm_end_bar"

asm_begin_foo と asm_begin_bar は、無視するアセンブリ ソース コード セクションの開始をマークします。 asm_end_foo と asm_end_bar はこれら各セクションの終了をマークします。

ヒント

IDE で Polyspace as You Code の拡張機能を使用する場合は、このオプションを解析オプション ファイルに入力します。オプション ファイルを参照してください。

参考

トピック

• Polyspace 解析オプションの指定