Merge pull request #1685 from goblint/issue_1683

Correctly cast offsets to `Cilfacade.ptrdiff_ikind ()` in memOutOfBounds
goblint · Feb 18, 2025 · 99df9da · 99df9da
2 parents bcf8b72 + 2b7ab2b
commit 99df9da
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 1 deletion.
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
@@ -174,7 +174,7 @@ struct
         `Index (ID.top (), convert_offset ofs)
       | Index (exp, ofs) ->
         let i = match man.ask (Queries.EvalInt exp) with
-          | `Lifted x -> x
+          | `Lifted x -> ID.cast_to (Cilfacade.ptrdiff_ikind ()) x
           | _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
         in
         `Index (i, convert_offset ofs)

diff --git a/tests/regression/74-invalid_deref/33-enum-in-index.c b/tests/regression/74-invalid_deref/33-enum-in-index.c
@@ -0,0 +1,21 @@
+//PARAM: --set ana.activated[+] memOutOfBounds
+//NOCRASH (had invalid ikind exceptions earlier)
+#include <stdlib.h>
+
+typedef enum {
+    ITEM_PREV,
+    ITEM_NEXT
+} direction_t;
+
+struct s {
+    int head[2];
+};
+
+
+int main()
+{
+    struct s* item = malloc(sizeof(struct s));
+    direction_t link_field = ITEM_NEXT;
+    item->head[link_field] = 0;
+    return 0;
+}