Fix pure classification of composite literals

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

@@ -44,11 +44,13 @@ trait UnderlyingType { this: TypeInfoImpl =>
           case value : PType => Some(value, this)
           case _ => None
         }
+        case st.AdtClause(_, typeDecl, _) => Some((typeDecl.right, this))
         case _ => None // type not defined
       }
       case PDot(_, id) => entity(id) match {
         case st.NamedType(decl, _, ctx) => inCtx(ctx, decl.right)
         case st.TypeAlias(decl, _, ctx) => inCtx(ctx, decl.right)
+        case st.AdtClause(_, typeDecl, _) => Some((typeDecl.right, this))
         case _ => None // type not defined
       }
       case t => Some((t, this))

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

@@ -466,8 +466,14 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case n: PIsComparable => asExpr(n.exp).forall(go)
 
       case PCompositeLit(typ, _) => typ match {
-        case _: PArrayType | _: PImplicitSizeArrayType => !strong
-        case _ => true
+        case _: PImplicitSizeArrayType => true
+        case t: PType => underlyingTypeP(t) match {
+          case Some(ut) => ut match {
+            case _: PSliceType | _: PMapType => false
+            case _ => true
+          }
+          case None => false
+        }
       }
 
       case POptionNone(_) => true

src/test/resources/regressions/features/arrays/array-length-simple2.gobra

@@ -6,7 +6,7 @@ package pkg
 const N = 42
 
 func foo() {
-	var a [N]int
-  assert len(a) == N
-  assert len(a) == 42
+    var a [N]int
+    assert len(a) == N
+    assert len(a) == 42
 }

src/test/resources/regressions/features/arrays/array-literal-simple1.gobra

@@ -60,3 +60,10 @@ func test10() {
   assert [4]int { 0, 1, 42, 8 }[2] == 42
   assert forall i int :: 0 <= i && i < 4 ==> ([4]int { 0, 2, 4, 6 })[i] == i + i
 }
+
+pure
+decreases
+func test11() [3]int {
+    // pure functions may contain array literals
+    return [3]int{}
+}

src/test/resources/regressions/features/maps/maps-fail1.gobra

@@ -30,3 +30,12 @@ func test4() {
 	//:: ExpectedOutput(type_error)
 	_ = map[int]int {1: 2, 1: 3}
 }
+
+// error: expected pure expression without permissions, but got map[int]int { }
+pure
+decreases
+func test5() map[int]int {
+    // pure functions may NOT contain map literals
+    //:: ExpectedOutput(type_error)
+    return map[int]int{}
+}

src/test/resources/regressions/features/slices/slice-type-fail1.gobra

@@ -7,4 +7,13 @@ package pkg
 //:: ExpectedOutput(type_error)
 requires s == t
 func foo(s []int, t []int) { 
+}
+
+// error: expected pure expression without permissions, but got []int { }
+pure
+decreases
+func f() []int {
+    // pure functions may NOT contain slice literals
+    //:: ExpectedOutput(type_error)
+    return []int{}
 }