From 5dbb6b33993d2af908af3d06f83e47c9c20f5d58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 21 May 2024 09:48:43 +0200 Subject: [PATCH] implement feedback from PR review --- .../typing/ghost/GhostExprTyping.scala | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) 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 index 83eb186f4..ec0652dec 100644 --- 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 @@ -468,10 +468,22 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => case PCompositeLit(typ, _) => typ match { case _: PImplicitSizeArrayType => true case t: PType => underlyingTypeP(t) match { - case Some(ut) => ut match { - case _: PSliceType | _: PGhostSliceType | _: PMapType => false - case _ => true + case Some(ut: PType with PLiteralType) => ut match { + case g: PGhostLiteralType => g match { + case _: PGhostSliceType => false + case _: PAdtType | _: PDomainType | _: PMathematicalMapType | + _: PMultisetType | _: POptionType | _: PSequenceType | _: PSetType => true + } + case _: PArrayType | _: PStructType => true + case _: PMapType | _: PSliceType => false + case d@(_: PDot | _: PNamedOperand) => + // underlyingTypeP should never return any of these types + violation(s"Unexpected underlying type $d") } + case Some(d) => + // the type system should already have rejected composite literals whose underlying type is not a valid + // literal type. + violation(s"Unexpected underlying type $d") case None => false } }