From fcb08dbb9564da3732dd8b0cbf0088d0f9826541 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Mon, 16 Aug 2004 20:54:16 +0000
Subject: [PATCH] Change to the spec...missed a consistency property.  Adding
 timing option.

---
 Repair/RepairCompiler/MCC/CLI.java                     |  5 ++++-
 Repair/RepairCompiler/MCC/Compiler.java                |  1 +
 Repair/RepairCompiler/MCC/IR/RepairGenerator.java      | 10 ++++++++++
 .../RepairCompiler/MCC/specs/abiword/abi.constraints   |  1 +
 Repair/RepairCompiler/MCC/specs/abiword/abi.model      |  3 ++-
 Repair/RepairCompiler/MCC/specs/abiword/abi.space      |  3 ++-
 6 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/CLI.java b/Repair/RepairCompiler/MCC/CLI.java
index 28ecc29..febfd74 100755
--- a/Repair/RepairCompiler/MCC/CLI.java
+++ b/Repair/RepairCompiler/MCC/CLI.java
@@ -11,7 +11,7 @@ import MCC.IR.DebugItem;
  * files.
  *
  * @author  le01, 6.035 Staff (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.11 2004/08/13 19:22:23 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.12 2004/08/16 20:53:53 bdemsky Exp $</tt>
  */
 public class CLI {
     /**
@@ -106,6 +106,7 @@ public class CLI {
 	    System.out.println("-aggressivesearch");
 	    System.out.println("-prunequantifiernodes");
 	    System.out.println("-cplusplus");
+	    System.out.println("-time");
 	    System.exit(-1);
 	}
 
@@ -123,6 +124,8 @@ public class CLI {
 		i+=3;
 	    } else if (args[i].equals("-debug")) {
                 Compiler.GENERATEDEBUGHOOKS=true;
+	    } else if (args[i].equals("-time")) {
+                Compiler.TIME=true;
 	    } else if (args[i].equals("-instrument")) {
                 Compiler.GENERATEINSTRUMENT=true;
 	    } else if (args[i].equals("-aggressivesearch")) {
diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index 70e9749..04ad0ba 100755
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -25,6 +25,7 @@ public class Compiler {
     public static boolean GENERATEDEBUGPRINT=false;
     public static boolean GENERATEINSTRUMENT=false;
     public static boolean ALLOCATECPLUSPLUS=false;
+    public static boolean TIME=false;
     
     public static Vector debuggraphs=new Vector();
 
diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index a6586bc..5d64040 100755
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -497,6 +497,11 @@ public class RepairGenerator {
 	crhead.outputline("void doanalysis();");
 	craux.outputline("void "+name +"_state::doanalysis()");
   	craux.startblock();
+	if (Compiler.TIME) {
+	    craux.outputline("struct timeval _begin_time,_end_time;");
+	    craux.outputline("gettimeofday(&_begin_time,NULL);");
+	}
+
 	if (Compiler.GENERATEINSTRUMENT) {
 	    craux.outputline("updatecount=0;");
 	    craux.outputline("rebuildcount=0;");
@@ -521,6 +526,11 @@ public class RepairGenerator {
     private void generate_teardown() {
 	CodeWriter cr = new StandardCodeWriter(outputaux);        
 	cr.endblock();
+	if (Compiler.TIME) {
+	    cr.outputline("gettimeofday(&_end_time,NULL);");
+	    cr.outputline("printf(\"time=%ld uS\\n\",(_end_time.tv_sec-_begin_time.tv_sec)*1000000+_end_time.tv_usec-_begin_time.tv_usec)");
+	}
+
 	if (Compiler.GENERATEINSTRUMENT) {
 	    cr.outputline("printf(\"updatecount=%d\\n\",updatecount);");
 	    cr.outputline("printf(\"rebuildcount=%d\\n\",rebuildcount);");
diff --git a/Repair/RepairCompiler/MCC/specs/abiword/abi.constraints b/Repair/RepairCompiler/MCC/specs/abiword/abi.constraints
index 5ea646d..ea14482 100755
--- a/Repair/RepairCompiler/MCC/specs/abiword/abi.constraints
+++ b/Repair/RepairCompiler/MCC/specs/abiword/abi.constraints
@@ -5,3 +5,4 @@
 [forall f in Frags], (sizeof(f.~Next)<=1);
 [forall f in firstblock], sizeof(f.~Next)=0;
 [forall l in Last, forall f in Fragments], f.PLast=l and sizeof(f.PLast)=1;
+[forall f in Frags], f.Length>=1;
\ No newline at end of file
diff --git a/Repair/RepairCompiler/MCC/specs/abiword/abi.model b/Repair/RepairCompiler/MCC/specs/abiword/abi.model
index 6e6a54e..1736391 100755
--- a/Repair/RepairCompiler/MCC/specs/abiword/abi.model
+++ b/Repair/RepairCompiler/MCC/specs/abiword/abi.model
@@ -6,5 +6,6 @@
 [forall f in Frags], !(f.m_next=null) => <f,f.m_next> in Next;
 [forall f in Frags], !(f.m_prev=null) => <f,f.m_prev> in Prev;
 [forall f in Frags], (f.m_next=null) => f in Last;
+[forall f in Frags], true => <f,f.m_length> in Length;
 [forall f in Fragments], !(f.m_pLast=null) => <f,f.m_pLast> in PLast;
-[forall f in Fragments], !(f.m_pLast=null) => f.m_pLast in LFrag;
\ No newline at end of file
+[forall f in Fragments], !(f.m_pLast=null) => f.m_pLast in LFrag;
diff --git a/Repair/RepairCompiler/MCC/specs/abiword/abi.space b/Repair/RepairCompiler/MCC/specs/abiword/abi.space
index 1a71eb1..1914511 100755
--- a/Repair/RepairCompiler/MCC/specs/abiword/abi.space
+++ b/Repair/RepairCompiler/MCC/specs/abiword/abi.space
@@ -6,4 +6,5 @@ set secondblock(pf_Frag_Strux_Block);
 Next: Frags -> Frags;
 Prev: Frags -> Frags;
 set LFrag(pf_Frag);
-PLast: Fragments -> LFrag;
\ No newline at end of file
+PLast: Fragments -> LFrag;
+Length: Frags -> int;
\ No newline at end of file
-- 
2.34.1