From 24c5400211153137f7131c9c81651c0ebdcecf02 Mon Sep 17 00:00:00 2001
From: Dhruv Makwana <dc_mak@outlook.com>
Date: Mon, 30 Sep 2024 17:47:37 +0100
Subject: [PATCH] Re-add removed broken-crash test as broken-proof

https://github.com/rems-project/cerberus/pull/602 changed the behaviour
of this test
---
 .../broken/error-proof/00001_aliasing.c       | 48 +++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 src/example-archive/java_program_verification_challenges/broken/error-proof/00001_aliasing.c

diff --git a/src/example-archive/java_program_verification_challenges/broken/error-proof/00001_aliasing.c b/src/example-archive/java_program_verification_challenges/broken/error-proof/00001_aliasing.c
new file mode 100644
index 00000000..f5501f0e
--- /dev/null
+++ b/src/example-archive/java_program_verification_challenges/broken/error-proof/00001_aliasing.c
@@ -0,0 +1,48 @@
+// Tags: main, pointers, structs, alias, java, malloc
+
+//#include <stdio.h>
+#include <stdlib.h>
+
+// Struct corresponding to the Java class C
+typedef struct C {
+    struct C *a; // Pointer to same struct type to mimic object reference
+    int i;
+} C;
+
+/* Normal-behavior
+ * @ requires true;
+ * @ assignable a, i;
+ * @ ensures a == NULL && i == 1;
+ */
+C* createC() {
+    C* c = (C*) malloc(sizeof(C)); // Allocate memory for C
+    c->a = NULL; // Initialize as null
+    c->i = 1;    // Initialize i to 1
+    return c;
+}
+
+// Struct corresponding to the Java class Alias
+/* typedef struct Alias { */
+/*     // No direct fields needed */
+/* } Alias; */
+
+/* Normal-behavior
+ * @ requires true;
+ * @ assignable nothing;
+ * @ ensures result == 4;
+ */
+int m() {
+    C* c = createC(); // Similar to 'C c = new C();'
+    c->a = c;         // Alias to itself
+    c->i = 2;         // Change i to 2
+    int result = c->i + c->a->i; // Equivalent to 'return c.i + c.a.i;'
+    free(c); // Clean up allocated memory
+    return result;
+}
+
+int main() {
+    /* Alias alias; // Instantiate Alias */
+    int result = m(); // Call m and store result
+    //printf("Result: %d\n", result); // Print the result
+    return result;
+}