Change to the spec...missed a consistency property. Adding timing option.

diff --git a/Repair/RepairCompiler/MCC/CLI.java b/Repair/RepairCompiler/MCC/CLI.java
index 28ecc2973c0ff7bf06b2a02693e60ec2521e1c4e..febfd744040537deb30a6f6c48d240b85989b389 100755 (executable)
--- 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 70e9749e07185d574c16f2314ff071cf58981bb4..04ad0bad552606b1f42f608d689d717009a34272 100755 (executable)
--- 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 a6586bc6de6cf77ca44bd9d6f62ffea7730e85c8..5d64040d50073b70b3df9c25d92beefb511a3ed7 100755 (executable)
--- 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 5ea646d0a14c1c9b9e0189f46a0ebc54734b9187..ea1448203d263533a7d86710fb270b87a66e64c7 100755 (executable)
--- 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 6e6a54e9663a99f0eb89d43549ca1c454327f288..1736391ff49dce1bdbab2180630e5e19cf63828a 100755 (executable)
--- 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 1a71eb18bd97127da7b8114f1be0e5f7fe293cfa..191451110a369359f34ea9a3e50b60a2200fbe7d 100755 (executable)
--- 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