diff --git a/src/plugins/alias/src/abstract_state.ml b/src/plugins/alias/src/abstract_state.ml index 25308698c088c279f5526b761cebb1e968ac2c5d..811472106b7d39b2beda10b1b99439bf20ab0e65 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 0000000000000000000000000000000000000000..893f065aa76fded518256696d02e0d076b94efd6 --- /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; +}