Merge pull request #1142 from utwente-fmt/cast-fixes

Fix for #1141

src/col/vct/col/typerules/CoercionUtils.scala

@@ -66,6 +66,7 @@ case object CoercionUtils {
       case (TNull(), JavaTClass(target, _)) => CoerceNullJavaClass(target)
       case (TNull(), TAnyClass()) => CoerceNullAnyClass()
       case (TNull(), TPointer(target)) => CoerceNullPointer(target)
+      case (TNull(), CTPointer(target)) => CoerceNullPointer(target)
       case (TNull(), TEnum(target)) => CoerceNullEnum(target)
 
       case (CTArray(_, innerType), TArray(element)) if element == innerType =>

src/rewrite/vct/rewrite/lang/LangCToCol.scala

@@ -308,6 +308,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz
       }
       NewPointerArray(rw.dispatch(t1), size)(ArrayMallocFailed(inv))(c.o)
     case CCast(CInvocation(CLocal("__vercors_malloc"), _, _, _), _) => throw UnsupportedMalloc(c)
+    case CCast(n@Null(), t) if t.asPointer.isDefined => rw.dispatch(n)
     case _ => throw UnsupportedCast(c)
   }
 

test/main/vct/test/integration/examples/CSpec.scala

@@ -369,4 +369,23 @@ class CSpec extends VercorsSpec {
         assert(sum[2] == 2);
     }
     """
+
+    vercors should verify using silicon in "Casting null to pointers" c
+    """
+    #include <stdlib.h>
+
+    struct nested {
+      struct nested *inner;  
+    };
+
+    void main() {
+      int *ip = NULL;                              
+      double *dp = NULL;                           
+      struct nested *np = NULL;                    
+      np = (struct nested*) NULL;               
+      np = (struct nested*) malloc(sizeof(struct nested));
+      np->inner = NULL;
+      np->inner = (struct nested*) NULL;         
+    }
+    """
 }