Chalice: fix a bug for boogie print-out of a sequence class

3 files changed, 10 insertions, 4 deletions

diff --git a/Chalice/make.py b/Chalice/make.py
index e3ba1ab9..643832ef 100644
--- a/Chalice/make.py
+++ b/Chalice/make.py
@@ -1,11 +1,15 @@
+#! /bin/python

+

 import os

 import glob

 import sys

 import datetime

 

 bindir = "bin"

+if not os.path.exists(bindir):

+    os.makedirs(bindir)

     

-srcspecs = ["src\\*.scala"]

+srcspecs = ["src/*.scala"]

 srcfiles = [file for spec in srcspecs for file in glob.glob(spec)]

 

 buildstamp = "makestamp"

@@ -24,7 +28,7 @@ def printtime():
     print datetime.datetime.now().strftime("%H:%M:%S")

 

 printtime()

-cmd = "scalac -d bin -unchecked -deprecation " + " ".join(changedfiles) + " & if errorlevel 1 exit 1"

+cmd = "scalac -d bin -unchecked -deprecation " + " ".join(changedfiles) + " 2>&1"

 print cmd

 result = os.system(cmd)

 printtime()

diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index c353a5ba..f889609f 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -162,7 +162,9 @@ object Boogie {
    case nt@ NamedType(s) =>

      s

    case ClassType(cl) =>

-     if (cl.IsRef) "ref" else cl.id

+     if (cl.IsRef) "ref"

+     else if (cl.IsSeq) "Seq " + cl.parameters(0).id

+     else cl.id

    case IndexedType(id,t) =>

      id + " (" + PrintType(t) + ")"

  }

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 2f54b71f..d202f42f 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -11,7 +11,7 @@ import scala.util.parsing.input.Position
 

 object Chalice {

  def main(args: Array[String]): unit = {

-   var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"

+   var boogiePath = "C:\\Users\\t-kuayes\\Documents\\Boogie-2010-07-13\\Boogie.exe"

    // parse command-line arguments

    var inputName: String = null

    var printProgram = false