Merge branch 'fix/nigron/kernel/Plus-promotion' into 'master'

Plus Promotion

See merge request frama-c/frama-c!4296

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)
 

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;

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

tests/syntax/oracle/sizeof.0.res.oracle

+[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.;
+

tests/syntax/oracle/sizeof.1.res.oracle

+[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.;
+

tests/syntax/sizeof.c

+/* 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");