integration with checking code

diff --git a/Robust/src/IR/Flat/BuildCode.java b/Robust/src/IR/Flat/BuildCode.java
index 6f906751da426e574d13c17154af0b2abcbe68b4..8fe2873251e9c1cc86e2f8caa80523b5d8c3ca8f 100644 (file)
--- a/Robust/src/IR/Flat/BuildCode.java
+++ b/Robust/src/IR/Flat/BuildCode.java
@@ -941,7 +941,9 @@ public class BuildCode {
            output.println("if (doanalysis"+specname+"("+varname+")) {");
            output.println("free"+specname+"_state("+varname+");");
            output.println("} else {");
+           output.println("/* Bad invariant */");
            output.println("free"+specname+"_state("+varname+");");
+           output.println("abort_task();");
            output.println("}");
 
            output.println("}");

diff --git a/Robust/src/IR/Tree/BuildIR.java b/Robust/src/IR/Tree/BuildIR.java
index e3f5a4e53a0f62ad13d8515239283fde151e88b3..52becbd039f212d2bd34f826290f988c89675369 100644 (file)
--- a/Robust/src/IR/Tree/BuildIR.java
+++ b/Robust/src/IR/Tree/BuildIR.java
@@ -423,7 +423,7 @@ public class BuildIR {
        for(int i=0;i<anv.size();i++) {
            ParseNode cpn=anv.elementAt(i);
            ParseNode var=cpn.getChild("var");
-           ParseNode exp=cpn.getChild("exp");
+           ParseNode exp=cpn.getChild("exp").getFirstChild();
            varlist.add(var.getTerminal());
            arglist.add(parseExpression(exp));
        }

diff --git a/Robust/src/IR/Tree/ConstraintCheck.java b/Robust/src/IR/Tree/ConstraintCheck.java
index 983c225c9381f2d954fdf290596974ec411b828b..2af99398c530ec52d061fa97ac6250657df62b5b 100644 (file)
--- a/Robust/src/IR/Tree/ConstraintCheck.java
+++ b/Robust/src/IR/Tree/ConstraintCheck.java
@@ -35,7 +35,7 @@ public class ConstraintCheck {
     }
 
     public String getVar(int i) {
-       return (String) args.get(i);
+       return (String) vars.get(i);
     }
 
     public String printNode(int indent) {

diff --git a/Robust/src/Parse/java14.cup b/Robust/src/Parse/java14.cup
index ad2e6a92c197b52e059eaa882a41698b3a77a3c8..4a6877a4e6612a9fe334220daafa87e57a2a7599 100644 (file)
--- a/Robust/src/Parse/java14.cup
+++ b/Robust/src/Parse/java14.cup
@@ -1220,7 +1220,7 @@ class_instance_creation_expression ::=
        ;
 cons_argument_list_opt ::=
        {: RESULT=new ParseNode("empty"); :}
-       |       argument_list:args {: RESULT=args; :}
+       |       cons_argument_list:args {: RESULT=args; :}
        ;
 
 cons_argument_list ::=

diff --git a/Robust/src/Runtime/runtime.c b/Robust/src/Runtime/runtime.c
index 818138debe8501e7a47ff59eac8220bca5dfce5b..8126ca13f79bb5a60ef8e891d7fc823c2e476238 100644 (file)
--- a/Robust/src/Runtime/runtime.c
+++ b/Robust/src/Runtime/runtime.c
@@ -19,7 +19,7 @@ jmp_buf error_handler;
 #include "SimpleHash.h"
 #include "GenericHashtable.h"
 #ifdef CONSCHECK
-#include "initialize.h"
+#include "instrument.h"
 #endif
 
 struct Queue * activetasks;
@@ -304,3 +304,12 @@ void failednullptr() {
   longjmp(error_handler,3);
 #endif
 }
+
+void abort_task() {
+#ifndef TASK
+  printf("Aborting\n");
+  exit(-1);
+#else
+  longjmp(error_handler,4);
+#endif
+}

diff --git a/Robust/src/Runtime/runtime.h b/Robust/src/Runtime/runtime.h
index 307679cbc05e94313beebfe5a8233b73fc4c5c69..d02c7286d041eea3ef10e6e2d31c8af775adfeed 100644 (file)
--- a/Robust/src/Runtime/runtime.h
+++ b/Robust/src/Runtime/runtime.h
@@ -9,6 +9,7 @@ struct ___String___ * NewString(char *str,int length);
 
 void failedboundschk();
 void failednullptr();
+void abort_task();
 
 #ifdef TASK
 #include "SimpleHash.h"

diff --git a/Robust/src/buildscriptrepair b/Robust/src/buildscriptrepair
index 1caf13f24c0393b4f9d5488814e5059d73a9529e..69dd5dd91f71bd30a591a2095403a3b42addd829 100755 (executable)
--- a/Robust/src/buildscriptrepair
+++ b/Robust/src/buildscriptrepair
@@ -53,7 +53,8 @@ done
 
 #build and link everything
 
-cd $CURDIR gcc -I$ROBUSTROOT/Runtime -I. -I$BUILDDIR/specdir \
+cd $CURDIR 
+gcc -I$ROBUSTROOT/Runtime -I. -I$BUILDDIR/specdir \
 -IRuntime/include -I$BUILDDIR -O0 -DBOEHM_GC -DCONSCHECK \
 -LRuntime/lib/ -lgc -DTASK -g tmpbuilddirectory/methods.c \
 tmpbuilddirectory/taskdefs.c $ROBUSTROOT/Runtime/runtime.c \