Checking in specs

diff --git a/Repair/RepairCompiler/MCC/specs/linkedlists/ex.constraints b/Repair/RepairCompiler/MCC/specs/linkedlists/ex.constraints
new file mode 100755 (executable)
index 0000000..42e959e
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/linkedlists/ex.constraints
@@ -0,0 +1 @@
+[], sizeof(Nodes) >= 1;

diff --git a/Repair/RepairCompiler/MCC/specs/linkedlists/ex.model b/Repair/RepairCompiler/MCC/specs/linkedlists/ex.model
new file mode 100755 (executable)
index 0000000..2528d0e
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/linkedlists/ex.model
@@ -0,0 +1,5 @@
+[], !(head=0) => head in Nodes;
+[forall node in Nodes], !(node.next=0) => node.next in Nodes;
+[forall node in Nodes], !(node.next=0) => <node, node.next> in nextnodes;
+
+

diff --git a/Repair/RepairCompiler/MCC/specs/linkedlists/ex.space b/Repair/RepairCompiler/MCC/specs/linkedlists/ex.space
new file mode 100755 (executable)
index 0000000..ac17965
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/linkedlists/ex.space
@@ -0,0 +1,4 @@
+set Nodes(Node);
+nextnodes : Nodes -> Nodes (1->1);
+prevnodes : Nodes -> Nodes (1->1);
+  

diff --git a/Repair/RepairCompiler/MCC/specs/linkedlists/ex.struct b/Repair/RepairCompiler/MCC/specs/linkedlists/ex.struct
new file mode 100755 (executable)
index 0000000..f8782dc
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/linkedlists/ex.struct
@@ -0,0 +1,6 @@
+Node* head;
+structure Node {
+     int data;
+     Node *next;
+     Node *prev;
+}

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;
+

diff --git a/Repair/RepairCompiler/MCC/specs/linkedlists/link.model b/Repair/RepairCompiler/MCC/specs/linkedlists/link.model
new file mode 100755 (executable)
index 0000000..1953ef2
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/linkedlists/link.model
@@ -0,0 +1,6 @@
+[], literal(true) => head in Nodes;
+[forall node in Nodes], !(node.next=literal(0)) => node.next in Nodes;
+[forall node in Nodes], !(node.next=literal(0)) => <node, node.next> in nextnodes;
+[forall node in Nodes], !(node.prev=literal(0)) => <node, node.prev> in prevnodes;
+
+

diff --git a/Repair/RepairCompiler/MCC/specs/linkedlists/link.space b/Repair/RepairCompiler/MCC/specs/linkedlists/link.space
new file mode 100755 (executable)
index 0000000..ac17965
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/linkedlists/link.space
@@ -0,0 +1,4 @@
+set Nodes(Node);
+nextnodes : Nodes -> Nodes (1->1);
+prevnodes : Nodes -> Nodes (1->1);
+  

diff --git a/Repair/RepairCompiler/MCC/specs/linkedlists/link.struct b/Repair/RepairCompiler/MCC/specs/linkedlists/link.struct
new file mode 100755 (executable)
index 0000000..f8782dc
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/specs/linkedlists/link.struct
@@ -0,0 +1,6 @@
+Node* head;
+structure Node {
+     int data;
+     Node *next;
+     Node *prev;
+}