some files

src/main/scala/viper/gobra/Gobra.scala

@@ -24,7 +24,7 @@ import viper.gobra.frontend.{Config, Desugar, PackageInfo, Parser, ScallopGobraC
 import viper.gobra.reporting._
 import viper.gobra.translator.Translator
 import viper.gobra.util.Violation.{KnownZ3BugException, LogicException, UglyErrorMessage}
-import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
+import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext, Sound}
 import viper.silicon.BuildInfo
 import viper.silver.{ast => vpr}
 
@@ -96,13 +96,17 @@ trait GoVerifier extends StrictLogging {
           warnings.foreach(w => logger.debug(w))
 
           result match {
-            case VerifierResult.Success => logger.info(s"$name found no errors")
+            case VerifierResult.Success =>
+              logger.info(s"$name found no errors")
+              Sound.playSuccess()
+
             case VerifierResult.Failure(errors) =>
               logger.error(s"$name has found ${errors.length} error(s) in package $pkgId")
               if (config.noStreamErrors) {
                 errors.foreach(err => logger.error(s"\t${err.formattedMessage}"))
               }
               allVerifierErrors = allVerifierErrors ++ errors
+              Sound.playFailure()
           }
         })(executor)
       try {

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

@@ -3198,6 +3198,19 @@ object Desugar extends LazyLogging {
       in.DefinedT(name, addrMod)
     }
 
+    def registerDesugaredDefinedType(t: in.DefinedT, ut: => in.Type): Unit = {
+      def register(addrMod: Addressability): Unit = {
+        if (!definedTypesSet.contains(t.name, addrMod)) {
+          definedTypesSet += ((t.name, addrMod))
+          definedTypes += (t.name, addrMod) -> ut.withAddressability(addrMod)
+        }
+      }
+      // [[underlyingType(in.Type)]] assumes that the RHS of a type declaration is in `definedTypes`
+      // if the corresponding type declaration was translated. This is necessary to avoid cycles in the translation.
+      register(Addressability.Exclusive)
+      register(Addressability.Shared)
+    }
+
     def registerInterface(t: Type.InterfaceT, dT: in.InterfaceT): Unit = {
 
       if (!registeredInterfaces.contains(dT.name) && info == t.context.getTypeInfo) {
@@ -3723,7 +3736,8 @@ object Desugar extends LazyLogging {
       case t: Type.AdtClauseT =>
         val adtName = nm.adt(t.declaredType)
         val definedName = nm.declaredType(t.declaredType)
-        val adt: in.AdtT = in.AdtT(adtName, definedName, addrMod)
+        val adt: in.AdtT = registerType(in.AdtT(adtName, definedName, addrMod))
+        registerDesugaredDefinedType(adt.definedType, adt)
         val fields: Vector[in.Field] = t.fields.map{ case (key: String, typ: Type) =>
           in.Field(nm.adtField(key, t.typeDecl), typeD(typ, Addressability.mathDataStructureElement)(src), true)(src)
         }

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

@@ -111,6 +111,7 @@ trait Implements { this: TypeInfoImpl =>
         case ut: Type.OptionT => go(ut.elem)
         case ut: Type.AdtT =>
           ut.clauses.forall(_.fields.forall(f => go(f._2)))
+        case _: Type.DomainT => true
         case ut: GhostCollectionType => go(ut.elem)
         case _: Type.InterfaceT => true
         case _ => false

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

@@ -30,7 +30,12 @@ trait GhostIdTyping { this: TypeInfoImpl =>
     })
     case c: AdtDestructor => wellDefAndType(c.decl.typ)
     case _: AdtDiscriminator => LocalMessages(noMessages)
-    case _: MatchVariable => LocalMessages(noMessages) // TODO
+    case MatchVariable(_, p, context) => p match {
+      case PMatchAdt(clause, _) =>
+        unsafeMessage(!context.symbType(clause).isInstanceOf[AdtClauseT])
+      case _: PExpression => LocalMessages(noMessages)
+      case _ => unsafeMessage(true)
+    }
     case _: BuiltInFPredicate | _: BuiltInMPredicate => LocalMessages(noMessages)
   }
 

src/main/scala/viper/gobra/util/Sound.scala

@@ -0,0 +1,68 @@
+package viper.gobra.util
+
+import javax.sound.sampled.{AudioFormat, AudioSystem}
+
+object Sound {
+
+  val SAMPLE_RATE: Float = 8000f
+
+  private class AudioPlayer {
+
+    private val sdl = {
+      val af = new AudioFormat(SAMPLE_RATE, 8, 1, true, false)
+      val res = AudioSystem.getSourceDataLine(af)
+      res.open(af)
+      res.start()
+      res
+    }
+
+    def play(hz: Int, msecs: Int, vol: Double = 1.0): Unit = {
+      val bytes = compile(hz, msecs, vol)
+      output(bytes)
+    }
+
+    private def compile(hz: Int, msecs: Int, vol: Double): Array[Byte] = {
+      val buf = Array.ofDim[Byte](msecs * 8)
+      for (i <- buf.indices) {
+        val angle = i / (SAMPLE_RATE / hz) * 2.0 * Math.PI
+        buf(i) = (Math.sin(angle) * 127.0 * vol).toByte
+      }
+      buf
+    }
+
+    private def output(bytes: Array[Byte]): Unit = {
+      for (off <- bytes.indices) {
+        sdl.write(bytes, off, 1)
+      }
+    }
+
+    def close(): Unit = {
+      sdl.drain()
+      sdl.stop()
+      sdl.close()
+    }
+  }
+
+  def playSong(song: Vector[Int]): Unit = {
+    try {
+      val player = new AudioPlayer
+      for (hz <- song) {
+        player.play(hz,100)
+        Thread.sleep(100)
+      }
+      player.close()
+    } catch {
+      case _: Throwable =>
+    }
+  }
+
+  def playSuccess(): Unit = {
+    // playSong(Vector(400,200,800,1200,2000,1200,200,800,1200,2000,1200,5000))
+    playSong(Vector(2000, 1200, 5000))
+  }
+
+  def playFailure(): Unit = {
+    // playSong(Vector(400,200,800,1200,2000,1200,200,800,1200,2000,1200,5000))
+    playSong(Vector(400, 400, 400))
+  }
+}