diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index db32e083853b0f47d2e51061cde25d9e19676f46..f2aef10880a544801388ad2e04cbf0aab0dab5c5 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -3220,10 +3220,9 @@ let parseIntAux (str:string) = else if hasSuffix "U" then 1, [IUInt; IULong; IULongLong] else - 0, if octalhexbin || true (* !!! This is against the ISO but it - * is what GCC and MSVC do !!! *) + 0, if octalhexbin then [IInt; IUInt; ILong; IULong; ILongLong; IULongLong] - else [IInt; ILong; IUInt; ILongLong] + else [IInt; ILong; ILongLong] in (* Convert to integer. To prevent overflow we do the arithmetic * on Big_int and we take care of overflow. We work only with diff --git a/tests/rte/minus.c b/tests/rte/minus.c index 4cdcbe6b5f95f139dafd7e0c08efc9f349d7625e..e47777802f40ba58a7b1db9969c4be9056ee4ad9 100644 --- a/tests/rte/minus.c +++ b/tests/rte/minus.c @@ -14,7 +14,7 @@ int main() { sz = ((unsigned short) (65535 + 3)) + x; z = -0x80000000 -1; /* this is unsigned and equal to 0x7fffffff */ - z = -2147483648 - 1; /* this is unsigned and equal to 0x7fffffff */ + z = -2147483648U - 1; /* this is unsigned and equal to 0x7fffffff */ z = -2147483647 -1 -1; /* this is signed and overflows */ z = -((int)(-0x7fffffff -1)) -1; /* this is signed and overflows */ diff --git a/tests/rte/oracle/minus.0.res.oracle b/tests/rte/oracle/minus.0.res.oracle index 77df3b0b03d4a660022539fbccd38d12177d4e60..f9e50a4d885f9ecf4e83153dae254f5bdca3d9b6 100644 --- a/tests/rte/oracle/minus.0.res.oracle +++ b/tests/rte/oracle/minus.0.res.oracle @@ -44,7 +44,7 @@ int main(void) */ sz = (short)((int)((unsigned short)(65535 + 3)) + x); z = (int)(-0x80000000 - (unsigned int)1); - z = (int)(-2147483648 - (unsigned int)1); + z = (int)(-2147483648U - (unsigned int)1); /*@ assert rte: signed_overflow: -2147483648 ≤ (int)((int)(-2147483647) - 1) - 1; */ diff --git a/tests/rte/oracle/minus.1.res.oracle b/tests/rte/oracle/minus.1.res.oracle index 4680985ca143b0f3f99aa520590ed9663da49e40..0ffa1074191fb7338107ad35ea2849d371f8c8b5 100644 --- a/tests/rte/oracle/minus.1.res.oracle +++ b/tests/rte/oracle/minus.1.res.oracle @@ -48,9 +48,9 @@ int main(void) z = (int)(-0x80000000 - (unsigned int)1); /*@ assert rte: signed_downcast: - (unsigned int)((unsigned int)(-2147483648) - 1) ≤ 2147483647; + (unsigned int)((unsigned int)(-2147483648U) - 1) ≤ 2147483647; */ - z = (int)(-2147483648 - (unsigned int)1); + z = (int)(-2147483648U - (unsigned int)1); /*@ assert rte: signed_overflow: -2147483647 ≤ 2147483647; */ /*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-2147483647) - 1; */ /*@ assert rte: signed_overflow: (int)(-2147483647) - 1 ≤ 2147483647; */ diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle index aadc000d33d4ccd15c6d6c8d5d00427c21ff79cd..3cc52c6d29e9e2c7397e635d39563599327c5efc 100644 --- a/tests/syntax/oracle/very_large_integers.0.res.oracle +++ b/tests/syntax/oracle/very_large_integers.0.res.oracle @@ -1,6 +1,6 @@ [kernel] Parsing very_large_integers.c (with preprocessing) [kernel] very_large_integers.c:35: User Error: - integer constant too large in expression (unsigned long long)999999999999999999 + 9999999999999999999 + integer constant too large in expression 999999999999999999U + 9999999999999999999U [kernel] very_large_integers.c:36: User Error: bitfield width is not a valid integer constant [kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c index 02f67ae756044c9e232212160f82af45e9017f32..52e7e4433bd5c0a83f5b435fd18d3231a4e7a7c7 100644 --- a/tests/syntax/very_large_integers.c +++ b/tests/syntax/very_large_integers.c @@ -33,7 +33,7 @@ volatile int nondet; #ifdef BITFIELD struct st { - int bf:(999999999999999999+9999999999999999999); + int bf:(999999999999999999U+9999999999999999999U); }; #endif