Correctly cast offsets to Cilfacade.ptrdiff_ikind () in memOutOfBounds

Author: michael-schwarz

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)

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;
+}