From: bdemsky <bdemsky>
Date: Thu, 6 May 2004 20:55:24 +0000 (+0000)
Subject: Checking in specs
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=commitdiff_plain;h=f688c9ba14f57603a31e8662c5d60f3a4e85939a

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