add case for ghost slice

viperproject · May 20, 2024 · 4883590 · 4883590
1 parent 0da53fa
commit 4883590
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala
@@ -689,7 +689,7 @@ case class PImplicitSizeArrayType(elem: PType) extends PLiteralType
 
 case class PSliceType(elem: PType) extends PTypeLit with PLiteralType
 
-case class PVariadicType(elem: PType) extends PTypeLit with PLiteralType
+case class PVariadicType(elem: PType) extends PTypeLit
 
 case class PMapType(key: PType, elem: PType) extends PTypeLit with PLiteralType
 

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala
@@ -469,7 +469,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
         case _: PImplicitSizeArrayType => true
         case t: PType => underlyingTypeP(t) match {
           case Some(ut) => ut match {
-            case _: PSliceType | _: PMapType => false
+            case _: PSliceType | _: PGhostSliceType | _: PMapType => false
             case _ => true
           }
           case None => false