From bce39b45977de9ffa51f7ff165987eb5f410f79e Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 13 Sep 2024 12:20:03 +0300
Subject: [PATCH] Add paper example

---
 .../debt-24-demo/paper-example/example.c      | 38 +++++++++++++++++++
 .../debt-24-demo/paper-example/goblint.json   | 22 +++++++++++
 .../debt-24-demo/paper-example/gobpie.json    |  6 +++
 3 files changed, 66 insertions(+)
 create mode 100644 adb_examples/debt-24-demo/paper-example/example.c
 create mode 100644 adb_examples/debt-24-demo/paper-example/goblint.json
 create mode 100644 adb_examples/debt-24-demo/paper-example/gobpie.json

diff --git a/adb_examples/debt-24-demo/paper-example/example.c b/adb_examples/debt-24-demo/paper-example/example.c
new file mode 100644
index 0000000..6e0bd49
--- /dev/null
+++ b/adb_examples/debt-24-demo/paper-example/example.c
@@ -0,0 +1,38 @@
+#include <stdio.h>
+#include <pthread.h>
+
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+typedef enum { PUBLISH, CACHE } ThreadAction;
+int global;
+
+int f(ThreadAction action) {
+    int cache = 0;
+    switch (action) {
+        case CACHE:
+            printf("Store in local cache!\n");
+            cache = 42;
+            break; // remove for flawed version
+        case PUBLISH:
+            printf("Publish work!\n");
+            global = 42;
+    }
+}
+
+void *t(void *arg) {
+    if (pthread_mutex_lock(&mutex)) {
+        f(CACHE);
+    } else {
+        f(PUBLISH);
+        pthread_mutex_unlock(&mutex);
+    }
+}
+
+
+int main() {
+    pthread_t t1, t2;
+    pthread_create(&t1, NULL, t, NULL);
+    pthread_create(&t2, NULL, t, NULL);
+    pthread_join(t1, NULL);
+    pthread_join(t2, NULL);
+    return 0;
+}
diff --git a/adb_examples/debt-24-demo/paper-example/goblint.json b/adb_examples/debt-24-demo/paper-example/goblint.json
new file mode 100644
index 0000000..5c67c82
--- /dev/null
+++ b/adb_examples/debt-24-demo/paper-example/goblint.json
@@ -0,0 +1,22 @@
+{
+  "files": [
+    "example.c"
+  ],
+  "ana": {
+    "int": {
+      "def_exc" : false,
+      "interval": true
+    }
+  },
+  "sem": {
+    "lock": {
+      "fail": true
+    }
+  },
+  "warn": {
+    "imprecise": false,
+    "deadcode": false,
+    "info": false
+  },
+  "allglobs": true
+}
diff --git a/adb_examples/debt-24-demo/paper-example/gobpie.json b/adb_examples/debt-24-demo/paper-example/gobpie.json
new file mode 100644
index 0000000..0283899
--- /dev/null
+++ b/adb_examples/debt-24-demo/paper-example/gobpie.json
@@ -0,0 +1,6 @@
+{
+    "goblintConf" : "goblint.json",
+    "abstractDebugging": true,
+    "showCfg": true,
+    "incrementalAnalysis": false
+}