From 3b78bec24e594756f65bab181e7425af95e564c7 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 21 Mar 2023 10:03:39 +0100
Subject: [PATCH] [machdep] more info in incompatibility messages
---
src/kernel_internals/typing/cabs2cil.ml | 4 ++--
src/plugins/eva/domains/cvalue/builtins.ml | 3 ++-
tests/misc/oracle/stdint.0.res.oracle | 10 +++++-----
tests/misc/oracle/stdint.1.res.oracle | 10 +++++-----
tests/misc/oracle/stdint.2.res.oracle | 10 +++++-----
5 files changed, 19 insertions(+), 18 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index a39379b1763..b6422e80307 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 2f497c83aec..feb925ad393 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 361bf0a731d..09ab5559b6a 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 f293275aad7..1bcb5d7a094 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 f293275aad7..7079c2fcd81 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
--
GitLab