Abiword specification

diff --git a/Repair/RepairCompiler/MCC/specs/abiword/abi.constraints b/Repair/RepairCompiler/MCC/specs/abiword/abi.constraints
new file mode 100755 (executable)
index 0000000..5ea646d
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/abiword/abi.constraints
@@ -0,0 +1,7 @@
+[], sizeof(firstblock)=1;
+[], sizeof(Fragments)=1;
+[], sizeof(secondblock)=1;
+[forall f in Frags], (!(sizeof(f.Next)=1)) or ((f.Next.Prev=f) and sizeof(f.Next.Prev)=1);
+[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;

diff --git a/Repair/RepairCompiler/MCC/specs/abiword/abi.model b/Repair/RepairCompiler/MCC/specs/abiword/abi.model
new file mode 100755 (executable)
index 0000000..6e6a54e
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/abiword/abi.model
@@ -0,0 +1,10 @@
+//empty file
+[], !(fragments=null) => fragments in Fragments;
+[forall f in Fragments], ((!(f.m_pFirst=null)) and (f.m_pFirst.m_type=2)) and cast(pf_Frag_Strux,f.m_pFirst).m_struxType=0 => cast(pf_Frag_Strux_Section,f.m_pFirst) in firstblock;
+[forall f in firstblock], ((!(f.m_next=null)) and (f.m_next.m_type=2)) and cast(pf_Frag_Strux,f.m_next).m_struxType=1 => cast(pf_Frag_Strux_Block,f.m_next) in secondblock;
+[forall f in Frags], !(f.m_next=null) => f.m_next in Frags;
+[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 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

diff --git a/Repair/RepairCompiler/MCC/specs/abiword/abi.space b/Repair/RepairCompiler/MCC/specs/abiword/abi.space
new file mode 100755 (executable)
index 0000000..1a71eb1
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/abiword/abi.space
@@ -0,0 +1,9 @@
+set Fragments(pf_Fragments);
+set Frags(pf_Frag): firstblock | secondblock | Last;
+set Last(pf_Frag);
+set firstblock(pf_Frag_Strux_Section);
+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

diff --git a/Repair/RepairCompiler/MCC/specs/abiword/abi.struct b/Repair/RepairCompiler/MCC/specs/abiword/abi.struct
new file mode 100755 (executable)
index 0000000..59f90c2
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/abiword/abi.struct
@@ -0,0 +1,71 @@
+structure UT_Vector { 
+   void * m_pEntries;
+   int m_iCount;
+   int m_iSpace;
+   int m_iCutoffDouble;
+   int m_iPostCutoffIncrement;
+}
+
+structure pf_Fragments { 
+   pf_Frag * m_pFirst;
+   pf_Frag * m_pLast;
+   UT_Vector m_vecFrags;
+   byte m_bAreFragsClean;
+   reserved byte[3];
+   pf_Frag * m_pCache;
+}
+
+structure pf_Frag { 
+   void * _vptr_pf_Frag;
+   int m_type;
+   int m_length;
+   pf_Frag * m_next;
+   pf_Frag * m_prev;
+   fd_Field * m_pField;
+   pt_PieceTable * m_pPieceTable;
+   int m_docPos;
+}
+
+structure pf_Frag_Strux subclass of pf_Frag { 
+   void * _vptr_pf_Frag;
+   int m_type;
+   int m_length;
+   pf_Frag * m_next;
+   pf_Frag * m_prev;
+   fd_Field * m_pField;
+   pt_PieceTable * m_pPieceTable;
+   int m_docPos;
+   int m_struxType;
+   int m_indexAP;
+   UT_Vector m_vecFmtHandle;
+}
+
+structure pf_Frag_Strux_Block subclass of pf_Frag_Strux { 
+   void * _vptr_pf_Frag;
+   int m_type;
+   int m_length;
+   pf_Frag * m_next;
+   pf_Frag * m_prev;
+   fd_Field * m_pField;
+   pt_PieceTable * m_pPieceTable;
+   int m_docPos;
+   int m_struxType;
+   int m_indexAP;
+   UT_Vector m_vecFmtHandle;
+}
+
+structure pf_Frag_Strux_Section subclass of pf_Frag_Strux { 
+   void * _vptr_pf_Frag;
+   int m_type;
+   int m_length;
+   pf_Frag * m_next;
+   pf_Frag * m_prev;
+   fd_Field * m_pField;
+   pt_PieceTable * m_pPieceTable;
+   int m_docPos;
+   int m_struxType;
+   int m_indexAP;
+   UT_Vector m_vecFmtHandle;
+}
+
+pf_Fragments * fragments;
\ No newline at end of file

diff --git a/Repair/RepairCompiler/MCC/specs/abiword/importantstructs b/Repair/RepairCompiler/MCC/specs/abiword/importantstructs
new file mode 100755 (executable)
index 0000000..f44ed2d
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/abiword/importantstructs
@@ -0,0 +1,3 @@
+pf_Frag_Strux_Section
+pf_Frag_Strux_Block
+pf_Fragments