Use size_t instead of sint for offsetof

Author: moratorium08

lib/compile.ml

@@ -802,7 +802,7 @@ module C_vars = struct
         return (IT (SizeOf scty, Memory.size_sbt, loc))
       | CNExpr_offsetof (tag, member) ->
         let@ _ = lookup_struct loc tag env in
-        return (IT (OffsetOf (tag, member), Memory.sint_sbt, loc))
+        return (IT (OffsetOf (tag, member), Memory.size_sbt, loc))
       | CNExpr_array_shift (base, ty_annot, index) ->
         let@ base = self base in
         let@ ct = infer_scty ~pred_loc:loc ~ptr:base `Array_shift ty_annot in

lib/wellTyped.ml

@@ -865,9 +865,9 @@ module WIT = struct
         let@ _ty = get_struct_member_type loc tag member in
         let@ decl = get_struct_decl loc tag in
         let o = Option.get (Memory.member_offset decl member) in
-        let rs = Option.get (BT.is_bits_bt Memory.sint_bt) in
+        let rs = Option.get (BT.is_bits_bt Memory.size_bt) in
         let@ () = ensure_z_fits_bits_type loc rs (Z.of_int o) in
-        return (IT (OffsetOf (tag, member), Memory.sint_bt, loc))
+        return (IT (OffsetOf (tag, member), Memory.size_bt, loc))
       | Aligned t ->
         let@ t_t = check loc (Loc ()) t.t in
         let@ t_align = check loc Memory.uintptr_bt t.align in

tests/cn/offsetof_type.c

@@ -0,0 +1,11 @@
+struct s
+{
+    int x;
+    int y;
+};
+
+int main()
+{
+    // C standard defines offsetof to have a size_t type, which we map to u64
+    /*@ assert (offsetof(s, y) == 4u64); @*/
+}

tests/cn/offsetof_type.c.coq

@@ -0,0 +1,6 @@
+return code: 0
+[1/1] tests/cn/offsetof_type.c:
+  CN verify:    SUCCESS
+  Coq compile:  SUCCESS
+
+All 1 tests passed!

tests/cn/offsetof_type.c.verify

@@ -0,0 +1,2 @@
+return code: 0
+[1/1]: main -- pass