暗黙的なデータ型の変換に関する 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