Fixed a variety of bugs...

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 11c3ea2b956087935b33247b346207097ca58f21..a3b8efdd219cc208aa33578151c3d9991efdc69f 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -741,7 +741,9 @@ public class RepairGenerator {
                /* Compute cost of each repair */
                VarDescriptor mincost=VarDescriptor.makeNew("mincost");
                VarDescriptor mincostindex=VarDescriptor.makeNew("mincostindex");
-               DNFConstraint dnfconst=constraint.dnfconstraint;
+               Vector dnfconst=new Vector();
+               dnfconst.addAll((Set)termination.conjunctionmap.get(constraint));
+
                if (dnfconst.size()<=1) {
                    cr.outputline("int "+mincostindex.getSafeSymbol()+"=0;");
                }
@@ -749,8 +751,8 @@ public class RepairGenerator {
                    cr.outputline("int "+mincostindex.getSafeSymbol()+";");
                    boolean first=true;
                    for(int j=0;j<dnfconst.size();j++) {
-                       Conjunction conj=dnfconst.get(j);
-                       GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
+                       GraphNode gn=(GraphNode)dnfconst.get(j);
+                       Conjunction conj=((TermNode)gn.getOwner()).getConjunction();
                        if (removed.contains(gn))
                            continue;
                        
@@ -788,8 +790,9 @@ public class RepairGenerator {
                }
                cr.outputline("switch("+mincostindex.getSafeSymbol()+") {");
                for(int j=0;j<dnfconst.size();j++) {
-                   Conjunction conj=dnfconst.get(j);
-                   GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
+                   GraphNode gn=(GraphNode)dnfconst.get(j);
+                   Conjunction conj=((TermNode)gn.getOwner()).getConjunction();
+
                    if (removed.contains(gn))
                        continue;
                    cr.outputline("case "+j+":");
@@ -1216,7 +1219,7 @@ public class RepairGenerator {
                    Rule r=(Rule)state.vRules.get(i);
                    if (r.getInclusion().getTargetDescriptors().contains(rd)) {
                        for(int j=0;j<mun.numUpdates();j++) {
-                           UpdateNode un=mun.getUpdate(i);
+                           UpdateNode un=mun.getUpdate(j);
                            if (un.getRule()==r) {
                                /* Update for rule rule r */
                                String name=(String)updatenames.get(un);
@@ -1237,7 +1240,7 @@ public class RepairGenerator {
                    Rule r=(Rule)state.vRules.get(i);
                    if (r.getInclusion().getTargetDescriptors().contains(sd)) {
                        for(int j=0;j<mun.numUpdates();j++) {
-                           UpdateNode un=mun.getUpdate(i);
+                           UpdateNode un=mun.getUpdate(j);
                            if (un.getRule()==r) {
                                /* Update for rule rule r */
                                String name=(String)updatenames.get(un);
@@ -1410,6 +1413,7 @@ public class RepairGenerator {
                        cr.outputline(methodcall+");");
                        cr.endblock();
                    }
+                   cr.outputline("delete "+newmodel.getSafeSymbol()+";");
                    cr.outputline("goto rebuild;");
                }
                cr.endblock();
@@ -1436,6 +1440,7 @@ public class RepairGenerator {
                    }
                    methodcall+=");";
                    cr.outputline(methodcall);
+                   cr.outputline("delete "+newmodel.getSafeSymbol()+";");
                    cr.outputline("goto rebuild;");
                }
            }
@@ -1551,6 +1556,7 @@ public class RepairGenerator {
                    }
                    methodcall+=");";
                    cr.outputline(methodcall);
+                   cr.outputline("delete "+newmodel.getSafeSymbol()+";");
                    cr.outputline("goto rebuild;");
                }
                cr.endblock();
@@ -1578,6 +1584,7 @@ public class RepairGenerator {
                    }
                    methodcall+=");";
                    cr.outputline(methodcall);
+                   cr.outputline("delete "+newmodel.getSafeSymbol()+";");
                    cr.outputline("goto rebuild;");
                }
            }

diff --git a/Repair/RepairCompiler/MCC/Runtime/classlist.h b/Repair/RepairCompiler/MCC/Runtime/classlist.h
index fab7ae2d559d1dafbbe286043688c47e5d4ccdce..1fbfcc7f719b4d507dd798e9c6cbc40068982c48 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Runtime/classlist.h
+++ b/Repair/RepairCompiler/MCC/Runtime/classlist.h
@@ -1,5 +1,6 @@
 #ifndef CLASSLIST_H
 #define CLASSLIST_H
+
 class typeobject;
 class typemap;
 class structuremap;

diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
index 39d44626db78a758c41f02151d1b4a589ab21b0a..507a77fafd1fab6afcff16a43133ed23b7328e8d 100755 (executable)
--- a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
+++ b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
@@ -39,7 +39,7 @@
 // C7
 // ??? for all files and directory blocks check that
 // only one inode references this block
-[forall b in FileDirectoryBlock],sizeof(b.~contents)=1;
+[forall b in FileDirectoryBlock],sizeof(b.~contents)=1; // should be <=
 
 // C10
 // verify that there is one inodetableblock