From 9261b71573b38f8b9e56d9121a9b1025325a13ec Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 7 Dec 2023 10:53:43 +0200
Subject: [PATCH] Extract library specificaton to goblint_library dune library

---
 src/dune                                       |  2 +-
 src/index.mld                                  |  3 +++
 src/{domains => util/library}/accessKind.ml    |  0
 src/util/library/dune                          | 18 ++++++++++++++++++
 src/util/library/library.mld                   | 14 ++++++++++++++
 src/{analyses => util/library}/libraryDesc.ml  |  0
 src/{analyses => util/library}/libraryDsl.ml   |  0
 src/{analyses => util/library}/libraryDsl.mli  |  0
 .../library}/libraryFunctions.ml               |  0
 .../library}/libraryFunctions.mli              |  0
 10 files changed, 36 insertions(+), 1 deletion(-)
 rename src/{domains => util/library}/accessKind.ml (100%)
 create mode 100644 src/util/library/dune
 create mode 100644 src/util/library/library.mld
 rename src/{analyses => util/library}/libraryDesc.ml (100%)
 rename src/{analyses => util/library}/libraryDsl.ml (100%)
 rename src/{analyses => util/library}/libraryDsl.mli (100%)
 rename src/{analyses => util/library}/libraryFunctions.ml (100%)
 rename src/{analyses => util/library}/libraryFunctions.mli (100%)

diff --git a/src/dune b/src/dune
index e40a58fcbd..8ad1b3aa4c 100644
--- a/src/dune
+++ b/src/dune
@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_incremental goblint_tracing
+  (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_library goblint_incremental goblint_tracing
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.
diff --git a/src/index.mld b/src/index.mld
index 755a736e6c..76b9d230dd 100644
--- a/src/index.mld
+++ b/src/index.mld
@@ -16,6 +16,9 @@ This {{!page-common}unwrapped library} contains various common modules extracted
 {2 Library goblint.domain}
 This {{!page-domain}unwrapped library} contains various domain modules extracted from {!Goblint_lib}.
 
+{2 Library goblint.library}
+This {{!page-library}unwrapped library} contains various library specification modules extracted from {!Goblint_lib}.
+
 {2 Library goblint.incremental}
 This {{!page-incremental}unwrapped library} contains various incremental modules extracted from {!Goblint_lib}.
 
diff --git a/src/domains/accessKind.ml b/src/util/library/accessKind.ml
similarity index 100%
rename from src/domains/accessKind.ml
rename to src/util/library/accessKind.ml
diff --git a/src/util/library/dune b/src/util/library/dune
new file mode 100644
index 0000000000..075c01c35d
--- /dev/null
+++ b/src/util/library/dune
@@ -0,0 +1,18 @@
+(include_subdirs no)
+
+(library
+ (name goblint_library)
+ (public_name goblint.library)
+ (wrapped false) ; TODO: wrap
+ (libraries
+   batteries.unthreaded
+   goblint_common
+   goblint_domain
+   goblint_config
+   goblint-cil)
+ (preprocess
+  (pps
+    ppx_deriving.std
+    ppx_deriving_hash)))
+
+(documentation)
diff --git a/src/util/library/library.mld b/src/util/library/library.mld
new file mode 100644
index 0000000000..f55db3f2ff
--- /dev/null
+++ b/src/util/library/library.mld
@@ -0,0 +1,14 @@
+{0 Library goblint.library}
+This library is unwrapped and provides the following top-level modules.
+For better context, see {!Goblint_lib} which also documents these modules.
+
+
+{1 Utilities}
+
+{2 Library specification}
+{!modules:
+AccessKind
+LibraryDesc
+LibraryDsl
+LibraryFunctions
+}
diff --git a/src/analyses/libraryDesc.ml b/src/util/library/libraryDesc.ml
similarity index 100%
rename from src/analyses/libraryDesc.ml
rename to src/util/library/libraryDesc.ml
diff --git a/src/analyses/libraryDsl.ml b/src/util/library/libraryDsl.ml
similarity index 100%
rename from src/analyses/libraryDsl.ml
rename to src/util/library/libraryDsl.ml
diff --git a/src/analyses/libraryDsl.mli b/src/util/library/libraryDsl.mli
similarity index 100%
rename from src/analyses/libraryDsl.mli
rename to src/util/library/libraryDsl.mli
diff --git a/src/analyses/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
similarity index 100%
rename from src/analyses/libraryFunctions.ml
rename to src/util/library/libraryFunctions.ml
diff --git a/src/analyses/libraryFunctions.mli b/src/util/library/libraryFunctions.mli
similarity index 100%
rename from src/analyses/libraryFunctions.mli
rename to src/util/library/libraryFunctions.mli