Merge pull request #747 from viperproject/ghost-pointer

Support for Ghost Pointers

src/main/antlr4/GobraLexer.g4

@@ -59,6 +59,7 @@ SET         : 'set'-> mode(NLSEMI);
 MSET        : 'mset'-> mode(NLSEMI);
 DICT        : 'dict'-> mode(NLSEMI);
 OPT         : 'option'-> mode(NLSEMI);
+GPOINTER    : 'gpointer'-> mode(NLSEMI);
 LEN         : 'len'-> mode(NLSEMI);
 NEW         : 'new'-> mode(NLSEMI);
 MAKE        : 'make'-> mode(NLSEMI);

src/main/antlr4/GobraParser.g4

@@ -141,7 +141,7 @@ seqUpdClause: expression ASSIGN expression;
 
 // Ghost Type Literals
 
-ghostTypeLit: sqType | ghostSliceType | domainType | adtType;
+ghostTypeLit: sqType | ghostSliceType | ghostPointerType | domainType | adtType;
 
 domainType: DOM L_CURLY (domainClause eos)* R_CURLY;
 
@@ -155,6 +155,8 @@ adtFieldDecl: identifierList? type_;
 
 ghostSliceType: GHOST L_BRACKET R_BRACKET elementType;
 
+ghostPointerType: GPOINTER L_BRACKET elementType R_BRACKET;
+
 sqType: (kind=(SEQ | SET | MSET | OPT) L_BRACKET type_ R_BRACKET)
     | kind=DICT L_BRACKET type_ R_BRACKET type_;
 

src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java

@@ -1,4 +1,4 @@
-// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
+// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 
@@ -362,6 +362,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitGhostSliceType(GobraParser.GhostSliceTypeContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitGhostPointerType(GobraParser.GhostPointerTypeContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *

src/main/java/viper/gobra/frontend/GobraParserVisitor.java

@@ -1,4 +1,4 @@
-// Generated from /Users/joao/code/gobra/src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
+// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.13.1
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 
@@ -314,6 +314,12 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitGhostSliceType(GobraParser.GhostSliceTypeContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#ghostPointerType}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitGhostPointerType(GobraParser.GhostPointerTypeContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#sqType}.
 	 * @param ctx the parse tree

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -731,13 +731,19 @@ case class PEmbeddedDecl(typ: PEmbeddedType, id: PIdnDef) extends PActualStructC
   require(id.name == typ.name)
 }
 
-sealed trait PMethodRecvType extends PActualType { // TODO: will have to be removed for packages
+sealed trait PMethodRecvType extends PType { // TODO: will have to be removed for packages
   def typ: PNamedOperand
 }
 
-case class PMethodReceiveName(typ: PNamedOperand) extends PMethodRecvType
+case class PMethodReceiveName(typ: PNamedOperand) extends PMethodRecvType with PActualType
 
-case class PMethodReceivePointer(typ: PNamedOperand) extends PMethodRecvType
+trait PMethodReceivePointer extends PMethodRecvType {
+  def typ: PNamedOperand
+}
+
+case class PMethodReceiveActualPointer(typ: PNamedOperand) extends PMethodReceivePointer with PActualType
+
+case class PMethodReceiveGhostPointer(typ: PNamedOperand) extends PMethodReceivePointer with PGhostType
 
 // TODO: Named type is not allowed to be an interface
 
@@ -1250,6 +1256,9 @@ case class PMathematicalMapType(keys: PType, values: PType) extends PGhostLitera
 /** The type of option types. */
 case class POptionType(elem : PType) extends PGhostLiteralType
 
+/** The type of ghost pointers */
+case class PGhostPointerType(elem: PType) extends PGhostLiteralType
+
 /** The type of ADT types */
 case class PAdtType(clauses: Vector[PAdtClause]) extends PGhostLiteralType with PUnorderedScope
 

src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala

@@ -642,7 +642,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
           ssep(pspec map showInterfaceClause, line)
       )
     case PMethodReceiveName(t) => showType(t)
-    case PMethodReceivePointer(t) => "*" <> showType(t)
+    case PMethodReceiveActualPointer(t) => "*" <> showType(t)
   }
 
   def showGhostType(typ : PGhostType) : Doc = typ match {
@@ -651,12 +651,14 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case PMultisetType(elem) => "mset" <> brackets(showType(elem))
     case PMathematicalMapType(keys, values) => "dict" <> brackets(showType(keys)) <> showType(values)
     case POptionType(elem) => "option" <> brackets(showType(elem))
+    case PGhostPointerType(elem) => "gpointer" <> brackets(showType(elem))
     case PGhostSliceType(elem) => "ghost" <+> brackets(emptyDoc) <> showType(elem)
     case PDomainType(funcs, axioms) =>
       "domain" <+> block(
         ssep((funcs ++ axioms) map showMisc, line)
       )
     case PAdtType(clauses) => "adt" <> block(ssep(clauses map showMisc, line))
+    case PMethodReceiveGhostPointer(t) => "gpointer" <> brackets(showType(t))
   }
 
   def showStructClause(c: PStructClause): Doc = c match {

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -2992,7 +2992,7 @@ object Desugar extends LazyLogging {
         case PIntLit(v, base)  => single(in.IntLit(v, base = base))
         case PBoolLit(b) => single(in.BoolLit(b))
         case PStringLit(s) => single(in.StringLit(s))
-        case nil: PNilLit => single(in.NilLit(typeD(info.nilType(nil).getOrElse(Type.PointerT(Type.BooleanT)), Addressability.literal)(src))) // if no type is found, then use *bool
+        case nil: PNilLit => single(in.NilLit(typeD(info.nilType(nil).getOrElse(Type.ActualPointerT(Type.BooleanT)), Addressability.literal)(src))) // if no type is found, then use *bool
         case f: PFunctionLit => registerFunctionLit(ctx, info)(f)
         case c: PCompositeLit => compositeLitD(ctx, info)(c)
         case _ => ???
@@ -3017,7 +3017,9 @@ object Desugar extends LazyLogging {
       // Both will have type Pointer(typeOf(v))
       val src: Meta = meta(v, info)
       val refAlias = nm.refAlias(idName(v, info), info.scope(v), info)
-      val param = in.Parameter.In(refAlias, typeD(PointerT(info.typ(v)), Addressability.inParameter)(src))(src)
+      // If `v` is a ghost variable, we consider `param` a ghost pointer. 
+      // However, we can use ActualPointer here since there is a single internal pointer type only.
+      val param = in.Parameter.In(refAlias, typeD(ActualPointerT(info.typ(v)), Addressability.inParameter)(src))(src)
       val localVar = in.LocalVar(nm.alias(refAlias, info.scope(v), info), param.typ)(src)
       (param, localVar)
     }
@@ -3767,7 +3769,7 @@ object Desugar extends LazyLogging {
         in.MapT(keysD, valuesD, addrMod)
       case Type.GhostSliceT(elem) => in.SliceT(typeD(elem, Addressability.sliceElement)(src), addrMod)
       case Type.OptionT(elem) => in.OptionT(typeD(elem, Addressability.mathDataStructureElement)(src), addrMod)
-      case PointerT(elem) => registerType(in.PointerT(typeD(elem, Addressability.pointerBase)(src), addrMod))
+      case Type.PointerT(elem) => registerType(in.PointerT(typeD(elem, Addressability.pointerBase)(src), addrMod))
       case Type.ChannelT(elem, _) => in.ChannelT(typeD(elem, Addressability.channelElement)(src), addrMod)
       case Type.SequenceT(elem) => in.SequenceT(typeD(elem, Addressability.mathDataStructureElement)(src), addrMod)
       case Type.SetT(elem) => in.SetT(typeD(elem, Addressability.mathDataStructureElement)(src), addrMod)
@@ -4931,7 +4933,7 @@ object Desugar extends LazyLogging {
       topLevelName(s"$METHODSPEC_PREFIX${interface(t)}")(n, context)
     def method  (n: String, t: PMethodRecvType, context: ExternalTypeInfo): String = t match {
       case PMethodReceiveName(typ)    => topLevelName(s"$METHOD_PREFIX${typ.name}")(n, context)
-      case PMethodReceivePointer(typ) => topLevelName(s"P$METHOD_PREFIX${typ.name}")(n, context)
+      case r: PMethodReceivePointer => topLevelName(s"P$METHOD_PREFIX${r.typ.name}")(n, context)
     }
     private def stringifyType(typ: in.Type): String = Names.serializeType(typ)
     def builtInMember(tag: BuiltInMemberTag, dependantTypes: Vector[in.Type]): String = {

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -503,6 +503,17 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     PGhostSliceType(typ).at(ctx)
   }
 
+  /**
+    * {@inheritDoc }
+    *
+    * <p>The default implementation returns the result of calling
+    * {@link #   visitChildren} on {@code ctx}.</p>
+    */
+  override def visitGhostPointerType(ctx: GhostPointerTypeContext): PGhostPointerType = {
+    val typ = visitNode[PType](ctx.elementType().type_())
+    PGhostPointerType(typ).at(ctx)
+  }
+
   /**
     * {@inheritDoc  }
     *
@@ -914,7 +925,8 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
   override def visitReceiver(ctx: ReceiverContext): PReceiver = {
     val recvType = visitNode[PType](ctx.type_()) match {
       case t : PNamedOperand => PMethodReceiveName(t).at(t)
-      case PDeref(t : PNamedOperand) => PMethodReceivePointer(t).at(t)
+      case PDeref(t: PNamedOperand) => PMethodReceiveActualPointer(t).at(t)
+      case PGhostPointerType(t: PNamedOperand) => PMethodReceiveGhostPointer(t).at(t)
       case f => fail(ctx.type_(), s"Expected declared type or pointer to declared type but got: $f.")
     }
 

src/main/scala/viper/gobra/frontend/info/base/Type.scala

@@ -74,7 +74,17 @@ object Type {
 
   case class MapT(key: Type, elem: Type) extends PrettyType(s"map[$key]$elem")
 
-  case class PointerT(elem: Type) extends PrettyType(s"*$elem")
+  sealed trait PointerT {
+    val elem: Type
+  }
+
+  object PointerT {
+    def unapply(arg: PointerT): Option[Type] = Some(arg.elem)
+  }
+
+  case class ActualPointerT(elem: Type) extends PrettyType(s"*$elem") with PointerT
+
+  case class GhostPointerT(elem: Type) extends PrettyType(s"gpointer[$elem]") with PointerT with GhostType
 
   case class ChannelT(elem: Type, mod: ChannelModus) extends PrettyType(s"$mod $elem")
 

src/main/scala/viper/gobra/frontend/info/implementation/property/Convertibility.scala

@@ -6,7 +6,7 @@
 
 package viper.gobra.frontend.info.implementation.property
 
-import viper.gobra.frontend.info.base.Type.{DeclaredT, Float32T, Float64T, IntT, PermissionT, PointerT, Single, SliceT, StringT, Type}
+import viper.gobra.frontend.info.base.Type.{ActualPointerT, DeclaredT, Float32T, Float64T, GhostPointerT, IntT, PermissionT, Single, SliceT, StringT, Type}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
 trait Convertibility extends BaseProperty { this: TypeInfoImpl =>
@@ -29,7 +29,9 @@ trait Convertibility extends BaseProperty { this: TypeInfoImpl =>
       case (left, right) => (underlyingType(left), underlyingType(right)) match {
         case (l, r) if identicalTypes(l, r) => true
         case (IntT(_), IntT(_)) => true
-        case (PointerT(l), PointerT(r)) if identicalTypes(underlyingType(l), underlyingType(r)) &&
+        case (ActualPointerT(l), ActualPointerT(r)) if identicalTypes(underlyingType(l), underlyingType(r)) &&
+          !(left.isInstanceOf[DeclaredT] && right.isInstanceOf[DeclaredT]) => true
+        case (GhostPointerT(l), GhostPointerT(r)) if identicalTypes(underlyingType(l), underlyingType(r)) &&
           !(left.isInstanceOf[DeclaredT] && right.isInstanceOf[DeclaredT]) => true
         case _ => false
       }

src/main/scala/viper/gobra/frontend/info/implementation/property/TypeIdentity.scala

@@ -51,7 +51,8 @@ trait TypeIdentity extends BaseProperty { this: TypeInfoImpl =>
         lm.keySet.forall(k => rm.get(k).exists(m => identicalTypes(memberType(m), memberType(lm(k))))) &&
           rm.keySet.forall(k => lm.get(k).exists(m => identicalTypes(memberType(m), memberType(rm(k)))))
 
-      case (PointerT(l), PointerT(r)) => identicalTypes(l, r)
+      case (ActualPointerT(l), ActualPointerT(r)) => identicalTypes(l, r)
+      case (GhostPointerT(l), GhostPointerT(r)) => identicalTypes(l, r)
 
       case (SortT, SortT) => true
 

src/main/scala/viper/gobra/frontend/info/implementation/property/TypeMerging.scala

@@ -7,7 +7,7 @@
 package viper.gobra.frontend.info.implementation.property
 
 import viper.gobra.ast.internal.{Float32T, Float64T}
-import viper.gobra.frontend.info.base.Type.{ArrayT, AssertionT, BooleanT, ChannelT, GhostSliceT, IntT, InternalTupleT, MapT, MultisetT, PermissionT, PointerT, SequenceT, SetT, Single, SliceT, Type}
+import viper.gobra.frontend.info.base.Type.{ActualPointerT, ArrayT, AssertionT, BooleanT, ChannelT, GhostPointerT, GhostSliceT, IntT, InternalTupleT, MapT, MultisetT, PermissionT, SequenceT, SetT, Single, SliceT, Type}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
 trait TypeMerging extends BaseProperty { this: TypeInfoImpl =>
@@ -45,7 +45,8 @@ trait TypeMerging extends BaseProperty { this: TypeInfoImpl =>
             k <- typeMerge(k1, k2)
             v <- typeMerge(v1, v2)
           } yield MapT(k, v)
-          case (PointerT(l), PointerT(r)) => typeMerge(l, r) map PointerT
+          case (ActualPointerT(l), ActualPointerT(r)) => typeMerge(l, r) map ActualPointerT
+          case (GhostPointerT(l), GhostPointerT(r)) => typeMerge(l, r) map GhostPointerT
           case (ChannelT(l, mod1), ChannelT(r, mod2)) if mod1 == mod2 => typeMerge(l, r) map (ChannelT(_, mod1))
           case _ => None
         }

src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala

@@ -247,7 +247,8 @@ trait MemberResolution { this: TypeInfoImpl =>
     attr[Type, AdvancedMemberSet[TypeMember]] {
       case t: InterfaceT => interfaceMethodSet(t)
       case pt@PointerT(t) => receiverSet(pt) union receiverSet(t).ref
-      case t => receiverSet(t) union receiverSet(PointerT(t)).deref
+      // we do not add `receiverSet(GhostPointerT(t)).deref` since this would result in implicitly assuming that the receiver points to the ghost heap, which is not guaranteed:
+      case t => receiverSet(t) union receiverSet(ActualPointerT(t)).deref
     }
 
   val nonAddressableMethodSet: Type => AdvancedMemberSet[TypeMember] =
@@ -265,7 +266,8 @@ trait MemberResolution { this: TypeInfoImpl =>
       case Single(t) =>
         pastPromotions(pastPromotionsMethodSuffix)(t) union (t match {
           case pt@ PointerT(st) => receiverSet(pt) union receiverSet(st).ref
-          case _ => receiverSet(t) union receiverSet(PointerT(t)).deref
+          // we do not add `receiverSet(GhostPointerT(t)).deref` since this would result in implicitly assuming that the receiver points to the ghost heap, which is not guaranteed:
+          case _ => receiverSet(t) union receiverSet(ActualPointerT(t)).deref
         })
       case _ => AdvancedMemberSet.empty
     }

src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala

@@ -144,7 +144,7 @@ trait NameResolution {
       case _ => violation("PIdnUnk always has a parent")
     }
 
-  private[resolution] lazy val isGhostDef: PNode => Boolean = isEnclosingExplicitGhost
+  private[resolution] lazy val isGhostDef: PNode => Boolean = isEnclosingGhost
 
   private[resolution] def serialize(id: PIdnNode): String = id.name
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

@@ -10,7 +10,7 @@ import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, check, error, noM
 import viper.gobra.ast.frontend.{AstPattern => ap, _}
 import viper.gobra.frontend.info.base.{SymbolTable => st}
 import viper.gobra.frontend.info.base.SymbolTable.{AdtDestructor, AdtDiscriminator, GlobalVariable, SingleConstant}
-import viper.gobra.frontend.info.base.Type._
+import viper.gobra.frontend.info.base.Type.{PointerT, _}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.util.TypeBounds.{BoundedIntegerKind, UnboundedInteger}
 import viper.gobra.util.{Constants, TypeBounds, Violation}
@@ -390,7 +390,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
             error(cap, "sequence slice expressions do not allow specifying a capacity", capT.isDefined)
         }
 
-        case (PointerT(ArrayT(l, _)), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) =>
+        case (ActualPointerT(ArrayT(l, _)), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) =>  // without ghost slices, slicing a ghost pointer is not allowed.
           val (lowOpt, highOpt, capOpt) = (low map intConstantEval, high map intConstantEval, cap map intConstantEval)
           error(n, s"index $low is out of bounds", !lowOpt.forall(_.forall(i => i >= 0 && i < l))) ++
             error(n, s"index $high is out of bounds", !highOpt.forall(_.forall(i => i >= 0 && i < l))) ++
@@ -707,7 +707,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
       val baseType = exprType(base)
       (underlyingType(baseType), low map exprType, high map exprType, cap map exprType) match {
         case (ArrayT(_, elem), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) if addressable(base) => SliceT(elem)
-        case (PointerT(ArrayT(_, elem)), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) => SliceT(elem)
+        case (ActualPointerT(ArrayT(_, elem)), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) => SliceT(elem)
         case (SequenceT(_), None | Some(IntT(_)), None | Some(IntT(_)), None) => baseType
         case (SliceT(_), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) => baseType
         case (GhostSliceT(_), None | Some(IntT(_)), None | Some(IntT(_)), None | Some(IntT(_))) => baseType
@@ -725,7 +725,9 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case t => violation(s"expected receive-permitting channel but got $t")
     }
 
-    case PReference(exp) if effAddressable(exp) => PointerT(exprType(exp))
+    case PReference(exp) if effAddressable(exp) =>
+      // we do not care whether the reference itself is in a ghost context or not but whether `exp` is ghost
+      if (isGhostLocation(exp)) GhostPointerT(exprType(exp)) else ActualPointerT(exprType(exp))
 
     case n: PAnd => // is boolean if left and right argument are boolean, otherwise is an assertion
       val lt = exprType(n.left)
@@ -750,7 +752,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
 
     case b: PBlankIdentifier => getBlankIdType(b)
 
-    case PNew(typ) => PointerT(typeSymbType(typ))
+    case n: PNew => if (isEnclosingGhost(n)) GhostPointerT(typeSymbType(n.typ)) else ActualPointerT(typeSymbType(n.typ))
 
     case PMake(typ, _) => typeSymbType(typ)
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/MiscTyping.scala

@@ -68,7 +68,7 @@ trait MiscTyping extends BaseTyping { this: TypeInfoImpl =>
     case PClosureDecl(args, res, _, _)  => FunctionT(args.map(typ), miscType(res))
 
     case PEmbeddedName(t) => typeSymbType(t)
-    case PEmbeddedPointer(t) => PointerT(typeSymbType(t))
+    case PEmbeddedPointer(t) => ActualPointerT(typeSymbType(t))
 
     case l: PLiteralValue => expectedMiscType(l)
     case l: PKeyedElement => miscType(l.exp)

src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala

@@ -130,7 +130,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
 
     case PMethodReceiveName(t) => typeSymbType(t)
 
-    case PMethodReceivePointer(t) => PointerT(typeSymbType(t))
+    case PMethodReceiveActualPointer(t) => ActualPointerT(typeSymbType(t))
 
     case PFunctionType(args, r) => FunctionT(args map miscType, miscType(r))
 
@@ -145,7 +145,8 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
 
     case n: PDeref =>
       resolve(n) match {
-        case Some(p: ap.PointerType) => PointerT(typeSymbType(p.base))
+        // since we have special syntax for ghost pointer types, `*T` always resolves to an actual pointer type
+        case Some(p: ap.PointerType) => ActualPointerT(typeSymbType(p.base))
         case _ => violation(s"expected type, but got $n")
       }
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostTypeTyping.scala

@@ -21,7 +21,9 @@ trait GhostTypeTyping extends BaseTyping { this : TypeInfoImpl =>
     case PMultisetType(elem) => isType(elem).out
     case PMathematicalMapType(key, value) => isType(key).out ++ isType(value).out
     case POptionType(elem) => isType(elem).out
+    case PGhostPointerType(elem) => isType(elem).out
     case n: PGhostSliceType => isType(n.elem).out
+    case PMethodReceiveGhostPointer(t) => isType(t).out
 
     case _: PDomainType => noMessages
     case n: PAdtType => n match {
@@ -39,7 +41,9 @@ trait GhostTypeTyping extends BaseTyping { this : TypeInfoImpl =>
     case PMultisetType(elem) => MultisetT(typeSymbType(elem))
     case PMathematicalMapType(keys, values) => MathMapT(typeSymbType(keys), typeSymbType(values))
     case POptionType(elem) => OptionT(typeSymbType(elem))
+    case PGhostPointerType(elem) => GhostPointerT(typeSymbType(elem))
     case PGhostSliceType(elem) => GhostSliceT(typeSymbType(elem))
+    case PMethodReceiveGhostPointer(t) => GhostPointerT(typeSymbType(t))
     case t: PDomainType => DomainT(t, this)
     case a: PAdtType => adtSymbType(a)
   }