Checking in specs

[repair.git] / Repair / RepairCompiler / MCC / specs / linkedlists / link.constraints

diff --git a/Repair/RepairCompiler/MCC/specs/linkedlists/link.constraints b/Repair/RepairCompiler/MCC/specs/linkedlists/link.constraints
new file mode 100755 (executable)
index 0000000..9e0c61b
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/linkedlists/link.constraints
@@ -0,0 +1,5 @@
+[], sizeof(Nodes) >= literal(1);
+[forall node in Nodes], sizeof(node.~nextnodes) <= literal(1);
+[forall n in Nodes], 
+       sizeof(n.nextnodes) = literal(0) or n.nextnodes.prevnodes = n;
+