diff --git a/share/libc/stdint.h b/share/libc/stdint.h
index 839a90e3dc1132e9b5b6a947ef2c27164faf0ec4..f7a7d365b28c922b777312e625a406f4bee4e1b5 100644
--- a/share/libc/stdint.h
+++ b/share/libc/stdint.h
@@ -163,16 +163,6 @@ typedef __UINTMAX_T uintmax_t;
#define WINT_MIN __FC_WINT_MIN
#define WINT_MAX __FC_WINT_MAX
-/* ISO C: 7.18.4 */
-#define INT8_C(c) c
-#define UINT8_C(c) c
-#define INT16_C(c) c
-#define UINT16_C(c) c
-#define INT32_C(c) (c ## L)
-#define UINT32_C(c) (c ## UL)
-#define INT64_C(c) (c ## LL)
-#define UINT64_C(c) (c ## ULL)
-
#define INTMAX_C(c) (c ## LL)
#define UINTMAX_C(c) (c ## ULL)
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index 9ca2d913b5b020f1358e914adf3c6bd1990eae39..f7734b1c823b5d490e128c092bac634658099fbb 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -68,6 +68,47 @@ let pp_of_kind =
"long long", "ll"
]
+let gen_precise_size_type fmt mach =
+ let open struct type ty = CHAR | SHORT | INT | LONG | LONGLONG end in
+ let all = [CHAR; SHORT; INT; LONG; LONGLONG] in
+ let size_of_ty t =
+ match t with
+ | CHAR -> 1
+ | SHORT -> mach.sizeof_short
+ | INT -> mach.sizeof_int
+ | LONG -> mach.sizeof_long
+ | LONGLONG -> mach.sizeof_longlong
+ in
+ let suffix_of_ty is_signed t =
+ let suff = try
+ List.assoc
+ (match t with
+ | CHAR -> "char"
+ | SHORT -> "short"
+ | INT -> "int"
+ | LONG -> "long"
+ | LONGLONG -> "long long") suff_of_kind
+ with Not_found -> Kernel.fatal "Undefined suffix type"
+ in
+ let suff = (if is_signed then "" else "U")^suff in
+ if suff = "" then "" else "## "^suff
+ in
+ let suffix is_signed n =
+ let t =
+ try
+ List.find (fun i -> size_of_ty i * 8 == n) all
+ with Not_found -> LONGLONG in
+ suffix_of_ty is_signed t
+ in
+ gen_define_string fmt "INT8_C(c)" ("(c"^(suffix true 8)^")");
+ gen_define_string fmt "INT16_C(c)" ("(c"^(suffix true 16)^")");
+ gen_define_string fmt "INT32_C(c)" ("(c"^(suffix true 32)^")");
+ gen_define_string fmt "INT64_C(c)" ("(c"^(suffix true 64)^")");
+ gen_define_string fmt "UINT8_C(c)" ("(c"^(suffix false 8)^")");
+ gen_define_string fmt "UINT16_C(c)" ("(c"^(suffix false 16)^")");
+ gen_define_string fmt "UINT32_C(c)" ("(c"^(suffix false 32)^")");
+ gen_define_string fmt "UINT64_C(c)" ("(c"^(suffix false 64)^")")
+
let max_val bitsize is_signed kind =
let suff = List.assoc kind suff_of_kind in
let suff = if is_signed then suff else "U" ^ suff in
@@ -249,6 +290,7 @@ let gen_all_defines fmt mach =
gen_char_unsigned_flag fmt mach;
gen_sizeof_std fmt mach;
gen_char_bit fmt mach;
+ gen_precise_size_type fmt mach;
gen_define_string fmt "__PTRDIFF_T" mach.ptrdiff_t;
gen_define_string fmt "__SIZE_T" mach.size_t;
gen_define_string fmt "__WCHAR_T" mach.wchar_t;
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index e2fedba13a469501a094a3d0a87af7e7a9b8da98..ae7a41fd5008aace906238f7035fda8352b7dab1 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6067,7 +6067,17 @@ and doExp local_env
else
abort_context "Unary ~ on a non-integral type"
- | Cabs.UNARY(Cabs.PLUS, e) -> doExp (no_paren_local_env local_env) asconst e what
+ | Cabs.UNARY(Cabs.PLUS, e) ->
+ let (r, se, e, t as v) = doExp (no_paren_local_env local_env) asconst e what in
+ if isIntegralType t then
+ let newt = integralPromotion t in
+ let e' = makeCastT ~e ~oldt:t ~newt in
+ finishExp r se e' newt
+ else
+ if isArithmeticType t then
+ v
+ else
+ abort_context "Unary + on a non-arithmetic type"
| Cabs.UNARY(Cabs.ADDROF, e) ->
(* some normalization is needed here to remove potential COMMA, QUESTION
diff --git a/tests/syntax/oracle/sizeof.0.res.oracle b/tests/syntax/oracle/sizeof.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..aa1ba789ca9fca267ec802decd82a0ed1c226e9d
--- /dev/null
+++ b/tests/syntax/oracle/sizeof.0.res.oracle
@@ -0,0 +1,17 @@
+[kernel] Parsing sizeof.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stdint.h"
+char c = (char)1;
+char a = (char)'a';
+int8_t i8 = (int8_t)125;
+uint8_t u8 = (uint8_t)230U;
+int16_t i16 = (int16_t)864;
+uint16_t u16 = (uint16_t)45213U;
+int32_t i32 = 864531;
+uint32_t u32 = 45213U;
+int64_t i64 = 753L;
+uint64_t u64 = 6453UL;
+int v = 645201;
+float f = (float)1.;
+double d = 1.;
+
diff --git a/tests/syntax/oracle/sizeof.1.res.oracle b/tests/syntax/oracle/sizeof.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..05c8abe3fa6d930520097aa9c3b94a8f07000f3e
--- /dev/null
+++ b/tests/syntax/oracle/sizeof.1.res.oracle
@@ -0,0 +1,17 @@
+[kernel] Parsing sizeof.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stdint.h"
+char c = (char)1;
+char a = (char)'a';
+int8_t i8 = (int8_t)125;
+uint8_t u8 = (uint8_t)230U;
+int16_t i16 = (int16_t)864;
+uint16_t u16 = (uint16_t)45213U;
+int32_t i32 = 864531;
+uint32_t u32 = 45213U;
+int64_t i64 = 753LL;
+uint64_t u64 = 6453ULL;
+int v = 645201;
+float f = (float)1.;
+double d = 1.;
+
diff --git a/tests/syntax/sizeof.c b/tests/syntax/sizeof.c
new file mode 100644
index 0000000000000000000000000000000000000000..a27bf94011e4a4341faf3a7e948d360ce70ec2d4
--- /dev/null
+++ b/tests/syntax/sizeof.c
@@ -0,0 +1,42 @@
+/* run.config
+ EXIT: 0
+ STDOPT: -machdep x86_64
+ STDOPT: -machdep x86_32
+*/
+char c = 1;
+_Static_assert(sizeof(-c) == sizeof(int), "Integer promotion with minus");
+_Static_assert(sizeof(+c) == sizeof(int), "Integer promotion with plus");
+_Static_assert(sizeof (c) == sizeof(char), "sizeof numeric char");
+char a = 'a';
+_Static_assert(sizeof(a) == sizeof(char), "sizeof char");
+_Static_assert(sizeof ('a') == sizeof(int), "sizeof literal char");
+
+#include "stdint.h"
+
+int8_t i8 = INT8_C(125);
+uint8_t u8 = UINT8_C(230);
+_Static_assert(sizeof +i8 == sizeof +INT8_C(50), "i8");
+_Static_assert(sizeof +u8 == sizeof +UINT8_C(140), "u8");
+
+int16_t i16 = INT16_C(864);
+uint16_t u16 = UINT16_C(45213);
+_Static_assert(sizeof +i16 == sizeof +INT16_C(645231), "i16");
+_Static_assert(sizeof +u16 == sizeof +UINT16_C(8475), "u16");
+
+int32_t i32 = INT32_C(864531);
+uint32_t u32 = UINT32_C(45213);
+_Static_assert(sizeof +i32 == sizeof +INT32_C(645231), "i32");
+_Static_assert(sizeof +u32 == sizeof +UINT32_C(8475), "u32");
+
+int64_t i64 = INT64_C(753);
+uint64_t u64 = UINT64_C(6453);
+_Static_assert(sizeof +i64 == sizeof +INT64_C(6531), "i64");
+_Static_assert(sizeof +u64 == sizeof +UINT64_C(64751), "u64");
+
+int v = 645201;
+_Static_assert(sizeof +v == sizeof(int), "Integer is promote to integer");
+
+float f = 1.;
+_Static_assert(sizeof +f == sizeof(float), "Float promotion");
+double d = 1.;
+_Static_assert(sizeof +d == sizeof(double), "Double promotion");