From 0367aa153420baf3ba9b4e36ad4dc3e21ba34285 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Mon, 17 May 2004 21:41:38 +0000
Subject: [PATCH] Fixed a variety of bugs...

---
 .../MCC/IR/RepairGenerator.java               | 21 ++++++++++++-------
 Repair/RepairCompiler/MCC/Runtime/classlist.h |  1 +
 .../MCC/specs/filesystem/test3.constraints    |  2 +-
 3 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 11c3ea2..a3b8efd 100755
--- 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 fab7ae2..1fbfcc7 100755
--- 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 39d4462..507a77f 100755
--- 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
-- 
2.34.1