Abiword specification

[repair.git] / Repair / RepairCompiler / MCC / specs / abiword / abi.constraints

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;