#pragma 命令に関する Code Prover の仮定

ほとんどの #pragma 命令は、検証に関連する情報をもたないため検証では無視されます。

ただし、以下のプラグマの動作は検証で考慮されます。

プラグマ検証への影響

#pragma asm および #pragma endasm

#asm および #endasm

これらのプラグマの間にある内容は検証で無視されます。

#pragma inline_asm func を使用する場合は、検証で関数 func にアセンブリ レベルの命令が含まれていることが考慮され、関数本体は無視されます。

#pragma hdrstopVisual C++® コンパイラの場合、検証ではこのプラグマを検出した時点でプリコンパイル済みヘッダーの処理が中止されます。
#pragma once検証では、現在のソース ファイルをコンパイルで 1 回だけ含めることができます。
#pragma pack(n), #pragma pack(push[,n]), #pragma pack(pop)

これらのプラグマで指定された境界の整列は検証で考慮されます。

引数が指定されていない #pragma pack は、#pragma pack(1) として扱われます。

詳細については、以下の例を参照してください。

#pragma inline global func または #pragma inline func検証では、関数 func がインライン関数として考慮されます。特に、既定で、Code Prover が生成した main は、他の関数で呼び出されることを前提として、これらの関数を直接呼び出しません。

_Pragma("inline=never") func

検証では、関数 func がインライン化されません。
#error message

この命令が検出されると検証は停止します。

詳細については、#error 命令に関連する Polyspace コンパイル エラーの修正を参照してください。

プラグマの詳細については、コンパイラのドキュメンテーションを参照してください。検証で前記のリストに記載された特定のプラグマが考慮されない場合、検証に適したコンパイラが指定されているかどうかを確認します。詳細については、コンパイラ (-compiler)を参照してください。

たとえば、このコードでは、命令 #pragma pack(n) で構造体に新しい整列境界を作成するように強制しています。これらの命令の動作は検証で考慮されるため、main 関数のユーザー アサーションチェックはグリーンになります。検証では以下のオプションを使用します。

#include <assert.h>

#pragma pack(2)

struct _s6 {
    char c;
    int i;
} s6;

#pragma pack() /* Restores default packing: pack(4) */

struct _sb {
    char c;
    int i;
} sb;

#pragma pack(1)

struct _s5 {
    char c;
    int i;
} s5;


int main(void) {
    assert(sizeof(s6) == 6);
    assert(sizeof(sb) == 8);
    assert(sizeof(s5) == 5);
    return 0;
}