If an operation involves two operands, the verification assumes that before the operation takes place, the operands can undergo implicit data type conversion. Whether this conversion happens depends on the original data types of the operands.
Following are the conversion rules that apply if the operands
in a binary operation have the same data type. Both operands can be
converted to int or unsigned int type
before the operation is performed. This conversion is called integer
promotion. The conversion rules are based on the ANSI® C99 Standard.
char and signed short variables
are converted to int variables.
unsigned short variables are converted
to int variables only if an int variable
can represent all possible values
of an unsigned short variable.
For targets where the size of int is the same as size of
short, unsigned short variables
are converted to unsigned int variables. For more information on data type sizes, see
Target processor type (-target).
Types such as int, long and long
long remain unchanged.
Following are some of the conversion rules that apply when the operands have different data types. The rules are based on the ANSI C99 Standard.
If both operands are signed or unsigned,
the operand with a lower-ranked data type is converted to the data
type of the operand with the higher-ranked type. The rank increases
in the order char, short, int, long,
and long long.
If one operand is unsigned and
the other signed, and the unsigned operand
data type has a rank higher or the same as the signed operand
data type, the signed operand is converted to the unsigned operand
type.
For instance, if one operand has data type int and
the other has type unsigned int, the int operand
is converted to unsigned int.
This example shows implicit conversions when the operands in a binary operation have the same data type. If you run verification on the examples, you can use tooltips on the Source pane to see the conversions.
In the first addition, i1 and i2 are
not converted before the addition. Their sum can have values outside
the range of an int type because i1 and i2 have
full-range values. Therefore, the Overflow check
on the first addition is orange.
In the second addition, c1 and c2 are
promoted to int before the addition. The addition
does not overflow because an int variable can represent
all values that result from the sum
of two char variables. The Overflow check
on the second addition is green. However, when the sum is assigned
to a char variable, an overflow occurs during the
conversion from int back to char.
An orange Overflow check appears on the = operation.
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;
}The following examples show implicit conversions that happen when the operands in a binary operation have different data types. If you run verification on the examples, you can use tooltips on the Source pane to see the conversions.
In this example, before the <= operation, x is
implicitly converted to unsigned int. Therefore,
the User
assertion check is red.
#include <assert.h>
int func(void) {
int x = -2;
unsigned int y = 5;
assert(x <= y);
}In this example, in the first assert statement, x is
implicitly converted to unsigned int before the
operation x <= y. Because of this conversion,
in the second assert statement, x is
greater than or equal to zero. The User assertion check
on the second assert statement is green.
int input(void);
void func(void) {
unsigned int y = 7;
int x = input();
assert ( x >= -7 && x <= y );
assert ( x >=0 && x <= 7);
}