diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index a39379b17639f2b7b16fa30bc44001c212afbb3e..b6422e8030749d9da9814f232e4a68fa14bc868f 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4494,9 +4494,9 @@ let checkTypedefSize name typ =
          (not exact && size < intended_size)
       then
         Kernel.warning ~current:true
-          "bad type '%a' (%d bits) for typedef '%s';@ \
+          "bad type '%a' (%d bits) for typedef '%s' using machdep %s;@ \
            check for mismatch between -machdep flag and headers used"
-          Typ.pretty typ size name
+          Typ.pretty typ size name Cil.theMachine.theMachine.machdep_name
     with
     (* Not a standard integer type, ignore it. *)
       Not_found -> ()
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index 2f497c83aec2232083a53a68a6bc222679f164e7..feb925ad393094dc7e98d1d4112efe7de8af2af3 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -165,9 +165,10 @@ let prepare_builtin kf (name, builtin, cacheable, expected_typ) =
     Self.warning ~source ~once:true
       ~wkey:Self.wkey_builtins_override
       "The builtin %s will not be used for function %a of incompatible type.@ \
-       (got: %a)."
+       (got: %a. Machdep is %s)."
       name Kernel_function.pretty kf
       Printer.pp_typ (Kernel_function.get_type kf)
+      Cil.theMachine.theMachine.machdep_name
   else
     match find_builtin_specification kf with
     | None ->
diff --git a/tests/misc/oracle/stdint.0.res.oracle b/tests/misc/oracle/stdint.0.res.oracle
index 361bf0a731d25c48a5968997fe52adc755984705..09ab5559b6a1fc7f710aa034c89d37e44aa0c611 100644
--- a/tests/misc/oracle/stdint.0.res.oracle
+++ b/tests/misc/oracle/stdint.0.res.oracle
@@ -1,16 +1,16 @@
 [kernel] Parsing stdint.i (no preprocessing)
 [kernel] stdint.i:10: Warning: 
-  bad type 'int' (16 bits) for typedef 'int8_t';
+  bad type 'int' (16 bits) for typedef 'int8_t' using machdep machdep_x86_16;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:11: Warning: 
-  bad type 'unsigned char' (8 bits) for typedef 'uint_least64_t';
+  bad type 'unsigned char' (8 bits) for typedef 'uint_least64_t' using machdep machdep_x86_16;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:12: Warning: 
-  bad type 'short' (16 bits) for typedef 'int_fast32_t';
+  bad type 'short' (16 bits) for typedef 'int_fast32_t' using machdep machdep_x86_16;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:13: Warning: 
-  bad type 'char' (8 bits) for typedef 'intptr_t';
+  bad type 'char' (8 bits) for typedef 'intptr_t' using machdep machdep_x86_16;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:14: Warning: 
-  bad type 'unsigned short' (16 bits) for typedef 'uintmax_t';
+  bad type 'unsigned short' (16 bits) for typedef 'uintmax_t' using machdep machdep_x86_16;
   check for mismatch between -machdep flag and headers used
diff --git a/tests/misc/oracle/stdint.1.res.oracle b/tests/misc/oracle/stdint.1.res.oracle
index f293275aad7449242b56d10e4cc386e2970208e7..1bcb5d7a0942a3a28924e4678f5271d44dc3df45 100644
--- a/tests/misc/oracle/stdint.1.res.oracle
+++ b/tests/misc/oracle/stdint.1.res.oracle
@@ -1,16 +1,16 @@
 [kernel] Parsing stdint.i (no preprocessing)
 [kernel] stdint.i:10: Warning: 
-  bad type 'int' (32 bits) for typedef 'int8_t';
+  bad type 'int' (32 bits) for typedef 'int8_t' using machdep machdep_ppc_32;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:11: Warning: 
-  bad type 'unsigned char' (8 bits) for typedef 'uint_least64_t';
+  bad type 'unsigned char' (8 bits) for typedef 'uint_least64_t' using machdep machdep_ppc_32;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:12: Warning: 
-  bad type 'short' (16 bits) for typedef 'int_fast32_t';
+  bad type 'short' (16 bits) for typedef 'int_fast32_t' using machdep machdep_ppc_32;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:13: Warning: 
-  bad type 'char' (8 bits) for typedef 'intptr_t';
+  bad type 'char' (8 bits) for typedef 'intptr_t' using machdep machdep_ppc_32;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:14: Warning: 
-  bad type 'unsigned short' (16 bits) for typedef 'uintmax_t';
+  bad type 'unsigned short' (16 bits) for typedef 'uintmax_t' using machdep machdep_ppc_32;
   check for mismatch between -machdep flag and headers used
diff --git a/tests/misc/oracle/stdint.2.res.oracle b/tests/misc/oracle/stdint.2.res.oracle
index f293275aad7449242b56d10e4cc386e2970208e7..7079c2fcd815cc8fae3a25d4b682b71360475c24 100644
--- a/tests/misc/oracle/stdint.2.res.oracle
+++ b/tests/misc/oracle/stdint.2.res.oracle
@@ -1,16 +1,16 @@
 [kernel] Parsing stdint.i (no preprocessing)
 [kernel] stdint.i:10: Warning: 
-  bad type 'int' (32 bits) for typedef 'int8_t';
+  bad type 'int' (32 bits) for typedef 'int8_t' using machdep machdep_msvc_x86_64;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:11: Warning: 
-  bad type 'unsigned char' (8 bits) for typedef 'uint_least64_t';
+  bad type 'unsigned char' (8 bits) for typedef 'uint_least64_t' using machdep machdep_msvc_x86_64;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:12: Warning: 
-  bad type 'short' (16 bits) for typedef 'int_fast32_t';
+  bad type 'short' (16 bits) for typedef 'int_fast32_t' using machdep machdep_msvc_x86_64;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:13: Warning: 
-  bad type 'char' (8 bits) for typedef 'intptr_t';
+  bad type 'char' (8 bits) for typedef 'intptr_t' using machdep machdep_msvc_x86_64;
   check for mismatch between -machdep flag and headers used
 [kernel] stdint.i:14: Warning: 
-  bad type 'unsigned short' (16 bits) for typedef 'uintmax_t';
+  bad type 'unsigned short' (16 bits) for typedef 'uintmax_t' using machdep machdep_msvc_x86_64;
   check for mismatch between -machdep flag and headers used