Repair/RepairCompiler/MCC/specs/abiword/abi.model

   1 //empty file
   2 [], !(fragments=null) => fragments in Fragments;
   3 [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;
   4 [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;
   5 [forall f in Frags], !(f.m_next=null) => f.m_next in Frags;
   6 [forall f in Frags], !(f.m_next=null) => <f,f.m_next> in Next;
   7 [forall f in Frags], !(f.m_prev=null) => <f,f.m_prev> in Prev;
   8 [forall f in Frags], (f.m_next=null) => f in Last;
   9 [forall f in Fragments], !(f.m_pLast=null) => <f,f.m_pLast> in PLast;
  10 [forall f in Fragments], !(f.m_pLast=null) => f.m_pLast in LFrag;