From f688c9ba14f57603a31e8662c5d60f3a4e85939a Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Thu, 6 May 2004 20:55:24 +0000
Subject: [PATCH] Checking in specs

---
 Repair/RepairCompiler/MCC/specs/linkedlists/ex.constraints  | 1 +
 Repair/RepairCompiler/MCC/specs/linkedlists/ex.model        | 5 +++++
 Repair/RepairCompiler/MCC/specs/linkedlists/ex.space        | 4 ++++
 Repair/RepairCompiler/MCC/specs/linkedlists/ex.struct       | 6 ++++++
 .../RepairCompiler/MCC/specs/linkedlists/link.constraints   | 5 +++++
 Repair/RepairCompiler/MCC/specs/linkedlists/link.model      | 6 ++++++
 Repair/RepairCompiler/MCC/specs/linkedlists/link.space      | 4 ++++
 Repair/RepairCompiler/MCC/specs/linkedlists/link.struct     | 6 ++++++
 8 files changed, 37 insertions(+)
 create mode 100755 Repair/RepairCompiler/MCC/specs/linkedlists/ex.constraints
 create mode 100755 Repair/RepairCompiler/MCC/specs/linkedlists/ex.model
 create mode 100755 Repair/RepairCompiler/MCC/specs/linkedlists/ex.space
 create mode 100755 Repair/RepairCompiler/MCC/specs/linkedlists/ex.struct
 create mode 100755 Repair/RepairCompiler/MCC/specs/linkedlists/link.constraints
 create mode 100755 Repair/RepairCompiler/MCC/specs/linkedlists/link.model
 create mode 100755 Repair/RepairCompiler/MCC/specs/linkedlists/link.space
 create mode 100755 Repair/RepairCompiler/MCC/specs/linkedlists/link.struct

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