Convert array subscript on pointers to pointer arithmetic

clangml-transforms/for_memcad.ml

@@ -596,6 +596,11 @@ with type 'a Applicative.t = 'a Applicative.t = struct
       { record_decl with fields = name_anonymous_fields record_decl.fields },
     Free_monoid.zero
 
+  let is_pointer_type (ty : Clang.Type.t) =
+    match ty.desc with
+    | Pointer _ -> true
+    | _ -> false
+
   let hook :
     type a . a Refl.refl -> (a -> env -> a * accu) -> (a -> env -> a * accu) =
   fun refl super x env ->
@@ -624,9 +629,18 @@ with type 'a Applicative.t = 'a Applicative.t = struct
                 Visit.visit [%refl: Clang.Ast.expr] []
                   cond { env with in_condition = true } in
               Call { callee; args = [cond] }, cond_stmts
-          | UnaryExpr { kind = SizeOf; argument } ->
-              visit_unary_expr_size_of argument env
-          | _ -> super x env
+        | UnaryExpr { kind = SizeOf; argument } ->
+            visit_unary_expr_size_of argument env
+        | ArraySubscript { base; index }
+             when is_pointer_type (Clang.Type.of_node base) ->
+            let x' : Clang.Ast.expr_desc = UnaryOperator {
+              kind = Deref;
+              operand = { base with desc = BinaryOperator {
+                lhs = base;
+                kind = Add;
+                rhs = index; }}} in
+            super x' env
+        | _ -> super x env
         end
     | Clang.Ast.Refl_decl_desc ->
         begin match x with