From 1430a80456f40922a4efc2af71b5863662a6e456 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Fri, 1 Mar 2024 17:12:08 +0100
Subject: [PATCH] [alias] add pathological example
tests/known_bugs/union_readback.c
The use of unions may lead to a crash in certain circumstances
---
src/plugins/alias/src/abstract_state.ml | 3 +++
.../alias/tests/known_bugs/union_readback.c | 19 +++++++++++++++++++
2 files changed, 22 insertions(+)
create mode 100644 src/plugins/alias/tests/known_bugs/union_readback.c
diff --git a/src/plugins/alias/src/abstract_state.ml b/src/plugins/alias/src/abstract_state.ml
index 25308698c08..811472106b7 100644
--- a/src/plugins/alias/src/abstract_state.ml
+++ b/src/plugins/alias/src/abstract_state.ml
@@ -173,6 +173,9 @@ module Readout = struct
let modify_lval lv = match E.label e with
| Field f -> let lhost, o = lv in lhost, Field (f, o)
| Pointer ->
+ (* TODO: This Cil.typeOfLval may crash with a fatal kernel
+ error for certain reconstructed lvals involving a union
+ type. See tests/known_bugs/union_readback.c *)
let ty = Cil.typeOfLval lv in
if Cil.isArrayType ty then
let lhost, o = lv in lhost, Index (Simplified.nul_exp, o)
diff --git a/src/plugins/alias/tests/known_bugs/union_readback.c b/src/plugins/alias/tests/known_bugs/union_readback.c
new file mode 100644
index 00000000000..893f065aa76
--- /dev/null
+++ b/src/plugins/alias/tests/known_bugs/union_readback.c
@@ -0,0 +1,19 @@
+// REPRODUCE: frama-c -alias -alias-verbose 2 union_readback.c
+// BEHAVIOUR: fatal kernel error [kernel] test.c:10: Failure:
+// typeOffset: Field r on a non-compound type 'char const **'
+// EXPECTED: no error
+// EXPLANATION:
+// This happens during the readback phase while reconstructing lvals.
+// The call [Cil.typeOfLval lv] on the reconstructed lval [lv] fails.
+// FIX: take into account typing information during reconstruction.
+
+typedef struct s {
+ union {
+ const char **v;
+ } r;
+} s;
+
+void f(const char** o) {
+ s flag;
+ flag.r.v = o;
+}
--
GitLab