reduces changeset, improves SymbExLogger unit tests to rely on subset behavior

Author: ArquintL

.gitignore

@@ -21,5 +21,5 @@ lib/
 silver
 src/test/resources/symbExLogTests/*.alog
 .DS_Store
-viper_tutorial_examples/
+viper_tutorial_examples
 .bsp/

src/main/resources/logback.xml

@@ -1,9 +1,3 @@
-<!-- This Source Code Form is subject to the terms of the Mozilla Public -->
-<!-- License, v. 2.0. If a copy of the MPL was not distributed with this -->
-<!-- file, You can obtain one at http://mozilla.org/MPL/2.0/. -->
-<!-- -->
-<!-- Copyright (c) 2011-2019 ETH Zurich. -->
-
 <!--
   ~ This Source Code Form is subject to the terms of the Mozilla Public
   ~ License, v. 2.0. If a copy of the MPL was not distributed with this

src/main/scala/Silicon.scala

@@ -9,7 +9,6 @@ package viper.silicon
 import java.nio.file.Paths
 import java.text.SimpleDateFormat
 import java.util.concurrent.{Callable, Executors, TimeUnit, TimeoutException}
-
 import scala.collection.immutable.ArraySeq
 import scala.util.{Left, Right}
 import ch.qos.logback.classic.{Level, Logger}

src/main/scala/rules/Brancher.scala

@@ -7,7 +7,6 @@
 package viper.silicon.rules
 
 import java.util.concurrent._
-
 import viper.silicon.common.concurrency._
 import viper.silicon.interfaces.{Unreachable, VerificationResult}
 import viper.silicon.logger.SymbExLogger

src/main/scala/verifier/DefaultMasterVerifier.scala

@@ -8,7 +8,6 @@ package viper.silicon.verifier
 
 import java.text.SimpleDateFormat
 import java.util.concurrent._
-
 import scala.annotation.unused
 import scala.collection.mutable
 import scala.util.Random

src/test/resources/symbExLogTests/testLogConfig.json

@@ -19,12 +19,7 @@ import viper.silver.frontend.{DefaultStates, Frontend}
 import viper.silver.reporter.NoopReporter
 
 class SymbExLoggerTests extends SilSuite {
-  /** directory containing test files */
   val testDirectories = Seq("symbExLogTests")
-  /**
-    * config file specifying what should be logged by the SymbExLogger.
-    * note that only a subset of records is collected to improve robustness of the tests */
-  val logConfigFile = "symbExLogTests/testLogConfig.json"
 
   override def frontend(verifier: Verifier, files: Seq[Path]): Frontend = {
     require(files.length == 1, "tests should consist of exactly one file")
@@ -71,8 +66,7 @@ class SymbExLoggerTests extends SilSuite {
     Seq(
       "--timeout", "300" /* seconds */,
       "--disableCaching", "--ideModeAdvanced",
-      "--numberOfParallelVerifiers", "1",
-      "--logConfig", getTestDirPath(logConfigFile).toString)
+      "--numberOfParallelVerifiers", "1")
 }
 
 class SiliconFrontendWithUnitTesting(path: Path) extends SiliconFrontend(NoopReporter) {