Code Prover Assumptions About Implicit Data Type Conversions

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.

Implicit Conversion When Operands Have Same Data Type

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;
}

If you hover on the operands in the binary operation c1 + c2, the tooltips show messages indicating the implicit conversion:

Conversion from int 8 to int 32

Implicit Conversion When Operands Have Different Data Types

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 the unsigned int value 0xFFFFFFFE or 4294967294. Therefore, the comparison with y fails and 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);
}

In both examples, if you hover on the operand x in the binary operation x <= y, the tooltip shows a message indicating the implicit conversion:

Conversion from int 32 to unsigned int 32