summaryrefslogtreecommitdiff
path: root/Chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice')
-rw-r--r--Chalice/src/Chalice.scala25
1 files changed, 22 insertions, 3 deletions
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 8e95a725..410e482c 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -118,15 +118,34 @@ object Chalice {
val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl"
writeFile(bplFilename, bplText);
// run Boogie.exe on out.bpl
- val boogie = Runtime.getRuntime().exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename);
- val input = new BufferedReader(new InputStreamReader(boogie.getInputStream()));
+ val boogie = Runtime.getRuntime.exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename);
+ // terminate boogie if interrupted
+ Runtime.getRuntime.addShutdownHook(new Thread(new Runnable() {
+ def run {
+ boogie.destroy
+ }
+ }))
+ // the process blocks until we exhaust input and error streams
+ new Thread(new Runnable() {
+ def run {
+ val err = new BufferedReader(new InputStreamReader(boogie.getErrorStream));
+ var line = err.readLine;
+ while(line!=null) {Console.err.println(line); Console.err.flush}
+ }
+ }).start;
+ val input = new BufferedReader(new InputStreamReader(boogie.getInputStream));
var line = input.readLine();
var previous_line = null: String;
while(line!=null){
- println(line);
+ Console.out.println(line);
+ Console.out.flush;
previous_line = line;
line = input.readLine();
}
+ boogie.waitFor;
+ input.close;
+
+ // generate code
if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack
val converter = new ChaliceToCSharp();
println("Code generated in out.cs.");