diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 74ea3ab799eddce2ab73093eea341864183ba3c1..b7b7c48bf13716b8882c66befcfb348e5724efe0 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -79,6 +79,12 @@ let access_ptr_elts ~loc tlv =
   let range = Logic_const.trange ~loc (None, None) in
   let basetype = Cil.typeOfTermLval tlv in
   let base = Logic_const.term ~loc (TLval tlv) basetype in
+  let base, basetype =
+    if Logic_utils.isLogicVoidPointerType basetype then begin
+      let typ = Ctype Cil.charPtrType in
+      Logic_const.term ~loc (TCastE(Cil.charPtrType,base)) typ, typ
+    end else base, basetype
+  in
   let offset = Logic_const.term ~loc (TBinOp (PlusPI, base, range)) basetype in
   TMem offset, TNoOffset
 
diff --git a/tests/syntax/asm_with_contracts.i b/tests/syntax/asm_with_contracts.i
index 215f8be829c2fcb5a53895bc4dbe1ac9971ce0b5..4631049bab383dbb0bf87d8cc1aa9dad451f08e8 100644
--- a/tests/syntax/asm_with_contracts.i
+++ b/tests/syntax/asm_with_contracts.i
@@ -22,3 +22,10 @@ int f(int z) {
 
   return x;
 }
+
+static __inline void
+insw (unsigned short int __port, void *__addr, unsigned long int __count)
+{
+  __asm__ __volatile__ ("cld ; rep ; insw":"=D" (__addr), "=c" (__count)
+   :"d" (__port), "0" (__addr), "1" (__count));
+}
diff --git a/tests/syntax/oracle/asm_with_contracts.res.oracle b/tests/syntax/oracle/asm_with_contracts.res.oracle
index 915bed6e6f7a47e1bf4858a7377f09fdafd66425..de45604755bf733ffeb4e6885baede947f7b9fb3 100644
--- a/tests/syntax/oracle/asm_with_contracts.res.oracle
+++ b/tests/syntax/oracle/asm_with_contracts.res.oracle
@@ -25,4 +25,23 @@ int f(int z)
   return x;
 }
 
+__inline static void insw(unsigned short __port, void *__addr,
+                          unsigned long __count)
+{
+  /*@ assigns __addr, __count, *((char *)__addr + (..));
+      assigns __addr
+        \from __port, (indirect: __addr), __count, *((char *)__addr + (..));
+      assigns __count
+        \from __port, (indirect: __addr), __count, *((char *)__addr + (..));
+      assigns *((char *)__addr + (..))
+        \from __port, (indirect: __addr), __count, *((char *)__addr + (..));
+  */
+  __asm__ volatile (
+    "cld ; rep ; insw"
+    : "=D" (__addr), "=c" (__count)
+    : "d" (__port), "0" (__addr), "1" (__count)
+    );
+  return;
+}
+