Merge pull request #588 from viperproject/remove-quotes

Remove quotes around Z3 arguments

silicon.bat

@@ -4,7 +4,7 @@ set CURR_DIR=%cd%
 set BASE_DIR=%~dp0
 
 :: switch to repository root to check for classpath file and possibly call sbt.
-cd %BASE_DIR%
+cd "%BASE_DIR%"
 
 :: Only call sbt if the classpath file is missing.
 if not exist silicon_classpath.txt (
@@ -22,12 +22,8 @@ if not exist silicon_classpath.txt (
 for /f "delims=" %%x in (silicon_classpath.txt) do set CP=%%x
 
 :: switch back to original directory
-cd %CURR_DIR%
+cd "%CURR_DIR%"
 
-set JAVA_EXE=java
-set JVM_OPTS=-Dlogback.configurationFile="%BASE_DIR%\src\main\resources\logback.xml" -Xss16m -Dfile.encoding=UTF-8
-set SILICON_MAIN=viper.silicon.SiliconRunner
-set FWD_ARGS= %*
-set CMD=%JAVA_EXE% %JVM_OPTS% -cp "%CP%" %SILICON_MAIN% %FWD_ARGS%
+set JVM_OPTS=-Xss16m -Dlogback.configurationFile="%BASE_DIR%\src\main\resources\logback.xml" -Dfile.encoding=UTF-8
 
-call %CMD%
+call java %JVM_OPTS% -cp "%CP%" viper.silicon.SiliconRunner %*

src/main/scala/Config.scala

@@ -54,10 +54,9 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   private val smtlibOptionsConverter: ValueConverter[Map[String, String]] = new ValueConverter[Map[String, String]] {
     def parse(s: List[(String, List[String])]): Either[String, Option[Map[String, String]]] = s match {
-      case (_, str :: Nil) :: Nil if str.head == '"' && str.last == '"' =>
+      case (_, str :: Nil) :: Nil =>
         val config = toMap(
-          str.substring(1, str.length - 1) /* Drop leading and trailing quotation mark */
-             .split(' ') /* Separate individual key=value pairs */
+          str.split(' ') /* Separate individual key=value pairs */
              .map(_.trim)
              .filter(_.nonEmpty)
              .map(_.split('=')) /* Split key=value pairs */
@@ -367,15 +366,15 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   val z3Args: ScallopOption[String] = opt[String]("z3Args",
     descr = (  "Command-line arguments which should be forwarded to Z3. "
-             + "The expected format is \"<opt> <opt> ... <opt>\", including the quotation marks."),
+             + "The expected format is \"<opt> <opt> ... <opt>\", excluding the quotation marks."),
     default = None,
     noshort = true
-  )(forwardArgumentsConverter)
+  )
 
   val z3ConfigArgs: ScallopOption[Map[String, String]] = opt[Map[String, String]]("z3ConfigArgs",
     descr = (  "Configuration options which should be forwarded to Z3. "
              + "The expected format is \"<key>=<val> <key>=<val> ... <key>=<val>\", "
-             + "including the quotation marks. "
+             + "excluding the quotation marks. "
              + "The configuration options given here will override those from Silicon's Z3 preamble."),
     default = Some(Map()),
     noshort = true