From 3e2ff29feab43fbd5d4e88699b4e126c76ee56f5 Mon Sep 17 00:00:00 2001
From: Dhruv Makwana <dc_mak@outlook.com>
Date: Tue, 13 Aug 2024 16:00:13 +0100
Subject: [PATCH] Re-add pointer dec tests

---
 .../broken/error-proof/00073.err1.c           | 20 +++++++++++
 .../c-testsuite/working/00032.c               | 35 +++++++++++++++++++
 .../broken/error-proof/pointer_dec3.c         |  9 +++++
 .../simple-examples/working/pointer_dec1.c    |  5 +++
 .../simple-examples/working/pointer_dec2.c    |  7 ++++
 5 files changed, 76 insertions(+)
 create mode 100644 src/example-archive/c-testsuite/broken/error-proof/00073.err1.c
 create mode 100644 src/example-archive/c-testsuite/working/00032.c
 create mode 100644 src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c
 create mode 100644 src/example-archive/simple-examples/working/pointer_dec1.c
 create mode 100644 src/example-archive/simple-examples/working/pointer_dec2.c

diff --git a/src/example-archive/c-testsuite/broken/error-proof/00073.err1.c b/src/example-archive/c-testsuite/broken/error-proof/00073.err1.c
new file mode 100644
index 00000000..f32b1df7
--- /dev/null
+++ b/src/example-archive/c-testsuite/broken/error-proof/00073.err1.c
@@ -0,0 +1,20 @@
+/*
+cn: internal error, uncaught exception:
+    Failure("todo")
+*/
+// Cause: `-=` assignment operator 
+
+int
+main()
+{
+	int arr[2];
+	int *p;
+	
+	p = &arr[1];
+	p -= 1;
+	*p = 123;
+	
+	if(arr[0] != 123)
+		return 1;
+	return 0;
+}
diff --git a/src/example-archive/c-testsuite/working/00032.c b/src/example-archive/c-testsuite/working/00032.c
new file mode 100644
index 00000000..61fe917c
--- /dev/null
+++ b/src/example-archive/c-testsuite/working/00032.c
@@ -0,0 +1,35 @@
+// Crash: caused by pointer decrement 
+
+int
+main()
+/*@ ensures return == 0i32; @*/
+{
+	int arr[2];
+	int *p;
+
+	/*@ extract Block<int>, 0u64; @*/
+	arr[0] = 2;
+	/*@ extract Block<int>, 1u64; @*/
+	arr[1] = 3;
+	p = &arr[0];
+	if(*(p++) != 2)
+		return 1;
+	if(*(p++) != 3)
+		return 2;
+	
+	p = &arr[1];
+	if(*(p--) != 3)
+		return 1;
+	if(*(p--) != 2)
+		return 2;
+		
+	p = &arr[0];
+	if(*(++p) != 3)
+		return 1;
+	
+	p = &arr[1];
+	if(*(--p) != 2) // <-- cause of the crash  
+		return 1;
+
+	return 0;
+}
diff --git a/src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c b/src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c
new file mode 100644
index 00000000..1b59c111
--- /dev/null
+++ b/src/example-archive/simple-examples/broken/error-proof/pointer_dec3.c
@@ -0,0 +1,9 @@
+// Crash 
+
+void
+pointerdec_crash_3()
+{
+  int arr[2];
+  int *p = &arr[1];
+  *(--p); 
+}
diff --git a/src/example-archive/simple-examples/working/pointer_dec1.c b/src/example-archive/simple-examples/working/pointer_dec1.c
new file mode 100644
index 00000000..a5d208da
--- /dev/null
+++ b/src/example-archive/simple-examples/working/pointer_dec1.c
@@ -0,0 +1,5 @@
+int a;
+void b() {
+  int *c = &a;
+  c -= 1;
+}
diff --git a/src/example-archive/simple-examples/working/pointer_dec2.c b/src/example-archive/simple-examples/working/pointer_dec2.c
new file mode 100644
index 00000000..542a2108
--- /dev/null
+++ b/src/example-archive/simple-examples/working/pointer_dec2.c
@@ -0,0 +1,7 @@
+// Derived from src/example-archive/c-testsuite/broken/error-proof/00032.err1.c
+
+int a;
+void b() {
+  int *c = &a;
+  --c;
+}