X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2Fspecs%2Fabiword%2Fabi.model;h=1736391ff49dce1bdbab2180630e5e19cf63828a;hp=6e6a54e9663a99f0eb89d43549ca1c454327f288;hb=fcb08dbb9564da3732dd8b0cbf0088d0f9826541;hpb=7f291611f4c559aca2ef3a01f205287fca8f1e7a

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;