[kernel] avoid generating ill-formed asm contracts in presence of void ptrs

When a `void *` lval is referenced in an asm directive, use its conversion
as `char *` in the contract to obtain well-formed `assigns` clauses.

Fixes #609

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
 

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

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