Chalice: Fixed a bug that prevented Chalice from correctly dealing with Boogie options containing white space characters

1 files changed, 12 insertions, 1 deletions

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 1b53a187..e639ddbb 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -48,6 +48,11 @@ object Chalice {
     var gen = false;

     var showFullStackTrace = false

 

+		println("----------------")

+		args foreach println

+		println("----------------")

+		// exit(0)

+		

     // closures should be idempotent

     val options = Map(

      "-print" -> {() => printProgram = true},

@@ -87,7 +92,13 @@ object Chalice {
          else percentageSupport = in

        } catch { case _ => CommandLineError("-percentageSupport takes integer argument", help); }

      }

-     else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // other arguments starting with "-" or "/" are sent to Boogie.exe

+     else if (a.startsWith("-") || a.startsWith("/"))

+			boogieArgs += ('"' + a + '"' + " ")

+				// other arguments starting with "-" or "/" are sent to Boogie.exe

+				/* [MHS] Quote whole argument to not confuse Boogie with arguments that

+				 * contain spaces, e.g. if Chalice is invoked as

+				 *   chalice -z3exe:"C:\Program Files\z3\z3.exe" program.chalice

+				 */

      else inputs += a

     }