Add runtime implementation for goblint.h (issue #814)

dune-project

@@ -65,5 +65,6 @@
     (share lib_stub_src)
     (share lib_runtime_include)
     (share lib_runtime_src)
+    (share lib_runtime)
     (share conf))
 )

lib/.gitignore

@@ -1,2 +1,5 @@
 # override root goblint .gitignore
 !goblint
+
+*.a
+*.so

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))

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

lib/goblint/runtime/src/dune

@@ -0,0 +1,5 @@
+(foreign_library
+ (archive_name goblint)
+ (language c)
+ (names goblint)
+ (include_dirs ../include))

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) {
+
+}