暗黙的なデータ型の変換に関する Code Prover の仮定

演算にオペランドが 2 つある場合、検証では演算の実行前にオペランドの暗黙的なデータ型の変換が実行される可能性があると仮定されます。この変換が実行されるかどうかは、オペランドの元のデータ型によって異なります。

二項演算のオペランドのデータ型が同じ場合に適用される変換ルールを次に示します。演算の実行前に、両方のオペランドを int 型または unsigned int 型に変換できます。この変換は整数プロモーションと呼ばれます。変換ルールは ANSI^® C99 規格に基づきます。

char と signed short の変数は int の変数に変換されます。
unsigned short の変数は、int の変数で unsigned short の変数に対するすべての可能な値を表せる場合に限り、int の変数に変換されます。
int のサイズが short のサイズと同じターゲットの場合、unsigned short の変数は unsigned int の変数に変換されます。データ型のサイズの詳細は、ターゲットプロセッサタイプ (-target)を参照してください。
int、long、long long などの型は変更されません。

オペランドのデータ型が異なる場合に適用される変換ルールの一部を次に示します。ルールは ANSI C99 規格に基づきます。

両方のオペランドが signed または unsigned の場合、データ型のランクが低いオペランドがランクが高いオペランドのデータ型に変換されます。ランクは、char、short、int、long、long long の順に高くなります。
一方のオペランドが unsigned でもう一方が signed であり、unsigned のオペランドのデータ型のランクが signed のオペランドのデータ型よりも高いかそれと同じ場合、signed のオペランドが unsigned のオペランドの型に変換されます。
たとえば、一方のオペランドのデータ型が int で、もう一方の型が unsigned int の場合、int のオペランドが unsigned int に変換されます。

オペランドのデータ型が同じ場合の暗黙的な変換

この例では、二項演算のオペランドのデータ型が同じ場合の暗黙的な変換を示します。この例について検証を実行すると、[ソース] ペインのツールヒントを使用して変換を確認できます。

1 つ目の加算では、i1 と i2 が加算前に変換されていません。i1 と i2 が全範囲の値を取るため、これらの合計は int の範囲外の値になる可能性があります。したがって、1 つ目の加算に対する [オーバーフロー] チェックはオレンジになります。

2 つ目の加算では、c1 と c2 が加算前に int にプロモートされています。2 つの char の変数を合計して得られるすべての値を int の変数で表すことができるため、この加算はオーバーフローしません。2 つ目の加算に対する [オーバーフロー] チェックはグリーンになります。ただし、合計を char の変数に代入した場合、int から char に変換を戻すときにオーバーフローが発生します。= 演算に対して [オーバーフロー] のオレンジチェックが表示されます。

extern char input_char(void);
extern int input_int(void);

void main(void) {
    char c1 = input_char();
    char c2 = input_char();
    int i1 = input_int();
    int i2 = input_int();
  
    i1 = i1 + i2;
    c1 = c1 + c2;
}

二項演算 c1 + c2 のオペランドにカーソルを合わせると、ツールヒントに暗黙的な変換であることを示すメッセージが表示されます。

Conversion from int 8 to int 32

オペランドのデータ型が異なる場合の暗黙的な変換

以下の例では、二項演算のオペランドのデータ型が異なる場合に実行される暗黙的な変換を示します。この例について検証を実行すると、[ソース] ペインのツールヒントを使用して変換を確認できます。

この例では、<= 演算の前に、x が unsigned int 値 0xFFFFFFFE または 4294967294 に暗黙的に変換されています。したがって、y は失敗し、ユーザーアサーションチェックはレッドになります。

#include <assert.h>
int func(void) {
    int x = -2;
    unsigned int y = 5;
    assert(x <= y);
}

この例では、1 つ目の assert ステートメントで、演算 x <= y の前に x が unsigned int に暗黙的に変換されます。この変換により、2 つ目の assert ステートメントで x がゼロ以上になります。2 つ目の assert ステートメントに対するユーザーアサーションチェックはグリーンになります。

int input(void);

void func(void) {
    unsigned int y = 7;
    int x = input();
    assert ( x >= -7 && x <= y );
    assert ( x >=0 && x <= 7);
}

どちらの例でも、二項演算 x <= y のオペランド x にカーソルを合わせると、ツールヒントに暗黙的な変換であることを示すメッセージが表示されます。

Conversion from int 32 to unsigned int 32