Merge pull request #603 from viperproject/fix-adt-postconditions

Fix ADT postcondition bug

Author: marcoeilers

src/main/scala/viper/silver/parser/Translator.scala

@@ -9,6 +9,7 @@ package viper.silver.parser
 import viper.silver.FastMessaging
 import viper.silver.ast.utility._
 import viper.silver.ast.{SourcePosition, _}
+import viper.silver.plugin.standard.adt.{Adt, AdtType}
 
 import scala.language.implicitConversions
 
@@ -582,12 +583,16 @@ case class Translator(program: PProgram) {
       MapType(ttyp(keyType), ttyp(valueType))
     case PDomainType(name, args) =>
       members.get(name.name) match {
-        case Some(d) =>
-          val domain = d.asInstanceOf[Domain]
+        case Some(domain: Domain) =>
           val typVarMapping = domain.typVars zip (args map ttyp)
           DomainType(domain, typVarMapping /*.filter {
             case (tv, tt) => tv!=tt //!tt.isInstanceOf[TypeVar]
           }*/.toMap)
+        case Some(adt: Adt) =>
+          val typVarMapping = adt.typVars zip (args map ttyp)
+          AdtType(adt, typVarMapping.toMap)
+        case Some(other) =>
+          sys.error(s"Did not expect member ${other}")
         case None =>
           assert(args.isEmpty)
           TypeVar(name.name) // not a domain, i.e. it must be a type variable

src/test/resources/adt/postconditions.vpr

@@ -0,0 +1,23 @@
+adt Wrap {
+  WrappedInt(
+    data: Int
+  )
+}
+
+function wrap(
+  data: Int
+): Wrap
+  ensures result.data == data
+
+function wrapNot(
+  data: Int
+): Wrap
+  ensures result.data != data
+
+method wrapTest() {
+  var x: Wrap := wrap(1)
+  assert(x.data == 1)
+  var y: Wrap := wrapNot(1)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert(y.data == 1)
+}