From d2408bfcc6a196662432cfa9455db8275ba676ea Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 4 Oct 2022 12:48:14 +0300
Subject: [PATCH] Add runtime implementation for goblint.h (issue #814)

---
 dune-project                          |  1 +
 lib/.gitignore                        |  3 +++
 lib/goblint/runtime/dune              | 14 +++++++++++++
 lib/goblint/runtime/include/goblint.h |  2 --
 lib/goblint/runtime/src/dune          |  5 +++++
 lib/goblint/runtime/src/goblint.c     | 30 +++++++++++++++++++++++++++
 6 files changed, 53 insertions(+), 2 deletions(-)
 create mode 100644 lib/goblint/runtime/dune
 create mode 100644 lib/goblint/runtime/src/dune
 create mode 100644 lib/goblint/runtime/src/goblint.c

diff --git a/dune-project b/dune-project
index e538fab5a29..5a644076817 100644
--- a/dune-project
+++ b/dune-project
@@ -65,5 +65,6 @@
     (share lib_stub_src)
     (share lib_runtime_include)
     (share lib_runtime_src)
+    (share lib_runtime)
     (share conf))
 )
diff --git a/lib/.gitignore b/lib/.gitignore
index 73e1aae63bd..6ae5d417d70 100644
--- a/lib/.gitignore
+++ b/lib/.gitignore
@@ -1,2 +1,5 @@
 # override root goblint .gitignore
 !goblint
+
+*.a
+*.so
diff --git a/lib/goblint/runtime/dune b/lib/goblint/runtime/dune
new file mode 100644
index 00000000000..135aa1ba897
--- /dev/null
+++ b/lib/goblint/runtime/dune
@@ -0,0 +1,14 @@
+; dune build lib/goblint/runtime/libgoblint.a
+(copy_files
+ (mode (promote (until-clean)))
+ (files src/libgoblint.a))
+
+(copy_files
+ (mode (promote (until-clean)))
+ (files src/dllgoblint.so))
+
+(install
+ (section (site (goblint lib_runtime)))
+ (files
+  libgoblint.a
+  dllgoblint.so))
diff --git a/lib/goblint/runtime/include/goblint.h b/lib/goblint/runtime/include/goblint.h
index 01d2121f979..b0af41616e4 100644
--- a/lib/goblint/runtime/include/goblint.h
+++ b/lib/goblint/runtime/include/goblint.h
@@ -6,5 +6,3 @@ void __goblint_assume_join(/* pthread_t thread */); // undeclared argument to av
 
 void __goblint_split_begin(int exp);
 void __goblint_split_end(int exp);
-
-// TODO: provide identity runtime stubs for actual linking
diff --git a/lib/goblint/runtime/src/dune b/lib/goblint/runtime/src/dune
new file mode 100644
index 00000000000..0586704839d
--- /dev/null
+++ b/lib/goblint/runtime/src/dune
@@ -0,0 +1,5 @@
+(foreign_library
+ (archive_name goblint)
+ (language c)
+ (names goblint)
+ (include_dirs ../include))
diff --git a/lib/goblint/runtime/src/goblint.c b/lib/goblint/runtime/src/goblint.c
new file mode 100644
index 00000000000..bc176f93a6a
--- /dev/null
+++ b/lib/goblint/runtime/src/goblint.c
@@ -0,0 +1,30 @@
+#include "goblint.h"
+#include <pthread.h>
+
+// Empty implementations (instead of asserts) because annotating documentation promises no-op right now.
+
+void __goblint_check(int exp) {
+
+}
+
+void __goblint_assume(int exp) {
+
+}
+
+void __goblint_assert(int exp) {
+
+}
+
+
+void __goblint_assume_join(pthread_t thread) {
+
+}
+
+
+void __goblint_split_begin(int exp) {
+
+}
+
+void __goblint_split_end(int exp) {
+
+}
\ No newline at end of file