From a840e412a7eedcd3cd6a2c8b3166e80acb4b8f2b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 4 Oct 2023 16:40:37 +0300
Subject: [PATCH 01/10] Extract most library extensions to std dune library

---
 src/dune                         | 19 ++++++++++---------
 src/goblint_lib.ml               | 17 +++--------------
 src/util/std/dune                | 17 +++++++++++++++++
 src/util/{ => std}/gobFpath.ml   |  0
 src/util/{ => std}/gobGc.ml      |  0
 src/util/{ => std}/gobHashtbl.ml |  0
 src/util/{ => std}/gobList.ml    |  0
 src/util/{ => std}/gobOption.ml  |  0
 src/util/{ => std}/gobPretty.ml  |  0
 src/util/{ => std}/gobRef.ml     |  0
 src/util/{ => std}/gobResult.ml  |  0
 src/util/{ => std}/gobSys.ml     |  0
 src/util/{ => std}/gobUnix.ml    |  0
 src/util/{ => std}/gobYaml.ml    |  0
 src/util/{ => std}/gobYojson.ml  |  0
 src/util/{ => std}/gobZ.ml       |  0
 src/util/std/goblint_std.ml      | 24 ++++++++++++++++++++++++
 17 files changed, 54 insertions(+), 23 deletions(-)
 create mode 100644 src/util/std/dune
 rename src/util/{ => std}/gobFpath.ml (100%)
 rename src/util/{ => std}/gobGc.ml (100%)
 rename src/util/{ => std}/gobHashtbl.ml (100%)
 rename src/util/{ => std}/gobList.ml (100%)
 rename src/util/{ => std}/gobOption.ml (100%)
 rename src/util/{ => std}/gobPretty.ml (100%)
 rename src/util/{ => std}/gobRef.ml (100%)
 rename src/util/{ => std}/gobResult.ml (100%)
 rename src/util/{ => std}/gobSys.ml (100%)
 rename src/util/{ => std}/gobUnix.ml (100%)
 rename src/util/{ => std}/gobYaml.ml (100%)
 rename src/util/{ => std}/gobYojson.ml (100%)
 rename src/util/{ => std}/gobZ.ml (100%)
 create mode 100644 src/util/std/goblint_std.ml

diff --git a/src/dune b/src/dune
index 85944375ea..a8cda818b1 100644
--- a/src/dune
+++ b/src/dune
@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint mainspec 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
+  (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
     ; 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.
@@ -56,6 +56,7 @@
       (-> violationZ3.no-z3.ml)
     )
   )
+  (flags :standard -open Goblint_std)
   (foreign_stubs (language c) (names stubs))
   (ocamlopt_flags :standard -no-float-const-prop)
   (preprocess
@@ -77,33 +78,33 @@
   (public_names goblint -)
   (modes byte native) ; https://dune.readthedocs.io/en/stable/dune-files.html#linking-modes
   (modules goblint mainspec)
-  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune)
+  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
-  (flags :standard -linkall)
+  (flags :standard -linkall -open Goblint_std)
 )
 
 (executable
   (name privPrecCompare)
   (modules privPrecCompare)
-  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune)
+  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
-  (flags :standard -linkall)
+  (flags :standard -linkall -open Goblint_std)
 )
 
 (executable
   (name apronPrecCompare)
   (modules apronPrecCompare)
-  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune)
+  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
-  (flags :standard -linkall)
+  (flags :standard -linkall -open Goblint_std)
 )
 
 (executable
   (name messagesCompare)
   (modules messagesCompare)
-  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune)
+  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
-  (flags :standard -linkall)
+  (flags :standard -linkall -open Goblint_std)
 )
 
 (rule
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 6e700485dd..816a69faff 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -469,29 +469,18 @@ module ConfigVersion = ConfigVersion
 
 (** {1 Library extensions}
 
-    OCaml library extensions which are completely independent of Goblint. *)
+    OCaml library extensions which are completely independent of Goblint.
+
+    See {!Goblint_std}. *)
 
 (** {2 Standard library}
 
     OCaml standard library extensions which are not provided by {!Batteries}. *)
 
 module GobFormat = GobFormat
-module GobGc = GobGc
-module GobHashtbl = GobHashtbl
-module GobList = GobList
-module GobRef = GobRef
-module GobResult = GobResult
-module GobOption = GobOption
-module GobSys = GobSys
-module GobUnix = GobUnix
 
 (** {2 Other libraries}
 
     External library extensions. *)
 
-module GobFpath = GobFpath
-module GobPretty = GobPretty
-module GobYaml = GobYaml
-module GobYojson = GobYojson
-module GobZ = GobZ
 module MyCheck = MyCheck
diff --git a/src/util/std/dune b/src/util/std/dune
new file mode 100644
index 0000000000..c85710a8d6
--- /dev/null
+++ b/src/util/std/dune
@@ -0,0 +1,17 @@
+(include_subdirs no)
+
+(library
+ (name goblint_std)
+ (public_name goblint.std)
+ (libraries
+   batteries
+   zarith
+   goblint-cil
+   fpath
+   yojson
+   yaml)
+ (preprocess
+  (pps
+   ppx_deriving.std
+   ppx_deriving_hash
+   ppx_deriving_yojson)))
diff --git a/src/util/gobFpath.ml b/src/util/std/gobFpath.ml
similarity index 100%
rename from src/util/gobFpath.ml
rename to src/util/std/gobFpath.ml
diff --git a/src/util/gobGc.ml b/src/util/std/gobGc.ml
similarity index 100%
rename from src/util/gobGc.ml
rename to src/util/std/gobGc.ml
diff --git a/src/util/gobHashtbl.ml b/src/util/std/gobHashtbl.ml
similarity index 100%
rename from src/util/gobHashtbl.ml
rename to src/util/std/gobHashtbl.ml
diff --git a/src/util/gobList.ml b/src/util/std/gobList.ml
similarity index 100%
rename from src/util/gobList.ml
rename to src/util/std/gobList.ml
diff --git a/src/util/gobOption.ml b/src/util/std/gobOption.ml
similarity index 100%
rename from src/util/gobOption.ml
rename to src/util/std/gobOption.ml
diff --git a/src/util/gobPretty.ml b/src/util/std/gobPretty.ml
similarity index 100%
rename from src/util/gobPretty.ml
rename to src/util/std/gobPretty.ml
diff --git a/src/util/gobRef.ml b/src/util/std/gobRef.ml
similarity index 100%
rename from src/util/gobRef.ml
rename to src/util/std/gobRef.ml
diff --git a/src/util/gobResult.ml b/src/util/std/gobResult.ml
similarity index 100%
rename from src/util/gobResult.ml
rename to src/util/std/gobResult.ml
diff --git a/src/util/gobSys.ml b/src/util/std/gobSys.ml
similarity index 100%
rename from src/util/gobSys.ml
rename to src/util/std/gobSys.ml
diff --git a/src/util/gobUnix.ml b/src/util/std/gobUnix.ml
similarity index 100%
rename from src/util/gobUnix.ml
rename to src/util/std/gobUnix.ml
diff --git a/src/util/gobYaml.ml b/src/util/std/gobYaml.ml
similarity index 100%
rename from src/util/gobYaml.ml
rename to src/util/std/gobYaml.ml
diff --git a/src/util/gobYojson.ml b/src/util/std/gobYojson.ml
similarity index 100%
rename from src/util/gobYojson.ml
rename to src/util/std/gobYojson.ml
diff --git a/src/util/gobZ.ml b/src/util/std/gobZ.ml
similarity index 100%
rename from src/util/gobZ.ml
rename to src/util/std/gobZ.ml
diff --git a/src/util/std/goblint_std.ml b/src/util/std/goblint_std.ml
new file mode 100644
index 0000000000..e716d1df5b
--- /dev/null
+++ b/src/util/std/goblint_std.ml
@@ -0,0 +1,24 @@
+(** OCaml library extensions which are completely independent of Goblint. *)
+
+(** {1 Standard library}
+
+    OCaml standard library extensions which are not provided by {!Batteries}. *)
+
+module GobGc = GobGc
+module GobHashtbl = GobHashtbl
+module GobList = GobList
+module GobRef = GobRef
+module GobResult = GobResult
+module GobOption = GobOption
+module GobSys = GobSys
+module GobUnix = GobUnix
+
+(** {1 Other libraries}
+
+    External library extensions. *)
+
+module GobFpath = GobFpath
+module GobPretty = GobPretty
+module GobYaml = GobYaml
+module GobYojson = GobYojson
+module GobZ = GobZ

From 7b76751a6cc2100f7c303c481fe28c0b7a4737a4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 Oct 2023 12:37:54 +0300
Subject: [PATCH 02/10] Move config modules to build_info dune library

---
 src/build-info/.gitignore                     |  1 +
 ...blint_build_info.ml => dune_build_info.ml} |  0
 ...blint_build_info.ml => dune_build_info.ml} |  0
 src/build-info/dune                           | 20 ++++++++++-
 ...int_build_info.mli => dune_build_info.mli} |  0
 src/build-info/goblint_build_info.ml          | 34 +++++++++++++++++++
 src/dune                                      | 16 ---------
 src/framework/control.ml                      |  2 +-
 src/goblint_lib.ml                            | 15 --------
 src/maingoblint.ml                            |  6 ++--
 src/util/sarif.ml                             |  2 +-
 src/util/tracing.ml                           |  2 +-
 src/version.ml                                | 16 ---------
 src/witness/witness.ml                        |  2 +-
 src/witness/yamlWitness.ml                    |  2 +-
 15 files changed, 62 insertions(+), 56 deletions(-)
 create mode 100644 src/build-info/.gitignore
 rename src/build-info/build_info_dune/{goblint_build_info.ml => dune_build_info.ml} (100%)
 rename src/build-info/build_info_js/{goblint_build_info.ml => dune_build_info.ml} (100%)
 rename src/build-info/{goblint_build_info.mli => dune_build_info.mli} (100%)
 create mode 100644 src/build-info/goblint_build_info.ml
 delete mode 100644 src/version.ml

diff --git a/src/build-info/.gitignore b/src/build-info/.gitignore
new file mode 100644
index 0000000000..8afff91d71
--- /dev/null
+++ b/src/build-info/.gitignore
@@ -0,0 +1 @@
+config*.ml
diff --git a/src/build-info/build_info_dune/goblint_build_info.ml b/src/build-info/build_info_dune/dune_build_info.ml
similarity index 100%
rename from src/build-info/build_info_dune/goblint_build_info.ml
rename to src/build-info/build_info_dune/dune_build_info.ml
diff --git a/src/build-info/build_info_js/goblint_build_info.ml b/src/build-info/build_info_js/dune_build_info.ml
similarity index 100%
rename from src/build-info/build_info_js/goblint_build_info.ml
rename to src/build-info/build_info_js/dune_build_info.ml
diff --git a/src/build-info/dune b/src/build-info/dune
index 89ae841778..c1de250263 100644
--- a/src/build-info/dune
+++ b/src/build-info/dune
@@ -8,4 +8,22 @@
 (library
   (name goblint_build_info)
   (public_name goblint.build-info)
-  (virtual_modules goblint_build_info))
+  (libraries batteries.unthreaded)
+  (virtual_modules dune_build_info))
+
+(rule
+  (target configVersion.ml)
+  (mode (promote (until-clean) (only configVersion.ml))) ; replace existing file in source tree, even if releasing (only overrides)
+  (deps (universe)) ; do not cache, always regenerate
+  (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = \"%s\"'")))))
+
+(rule
+  (target configProfile.ml)
+  (mode (promote (until-clean) (only configProfile.ml))) ; replace existing file in source tree, even if releasing (only overrides)
+  (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet profile = \"%{profile}\"")))
+
+(rule
+  (target configOcaml.ml)
+  (mode (promote (until-clean) (only configOcaml.ml))) ; replace existing file in source tree, even if releasing (only overrides)
+  (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet flambda = \"%{ocaml-config:flambda}\"")))
+
diff --git a/src/build-info/goblint_build_info.mli b/src/build-info/dune_build_info.mli
similarity index 100%
rename from src/build-info/goblint_build_info.mli
rename to src/build-info/dune_build_info.mli
diff --git a/src/build-info/goblint_build_info.ml b/src/build-info/goblint_build_info.ml
new file mode 100644
index 0000000000..cf5165d51c
--- /dev/null
+++ b/src/build-info/goblint_build_info.ml
@@ -0,0 +1,34 @@
+(** Goblint build info. *)
+
+(** OCaml compiler flambda status. *)
+let ocaml_flambda = ConfigOcaml.flambda
+
+(** Dune profile. *)
+let dune_profile = ConfigProfile.profile
+
+(** Goblint version from git. *)
+let git_version = ConfigVersion.version
+
+(** Goblint version from release archive. *)
+let release_version = "%%VERSION_NUM%%"
+
+(** Goblint git commit from release archive. *)
+let release_commit = "%%VCS_COMMIT_ID%%"
+
+(** Goblint version. *)
+let version =
+  let commit = ConfigVersion.version in
+  if BatString.starts_with release_version "%" then
+    commit
+  else (
+    let commit =
+      if commit = "n/a" then (* released archive has no .git *)
+        release_commit
+      else
+        commit
+    in
+    Format.sprintf "%s (%s)" release_version commit
+  )
+
+(** Statically linked libraries with versions. *)
+let statically_linked_libraries = Dune_build_info.statically_linked_libraries
diff --git a/src/dune b/src/dune
index a8cda818b1..5fdf58a5b2 100644
--- a/src/dune
+++ b/src/dune
@@ -107,22 +107,6 @@
   (flags :standard -linkall -open Goblint_std)
 )
 
-(rule
-  (target configVersion.ml)
-  (mode (promote (until-clean) (only configVersion.ml))) ; replace existing file in source tree, even if releasing (only overrides)
-  (deps (universe)) ; do not cache, always regenerate
-  (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = \"%s\"'")))))
-
-(rule
-  (target configProfile.ml)
-  (mode (promote (until-clean) (only configProfile.ml))) ; replace existing file in source tree, even if releasing (only overrides)
-  (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet profile = \"%{profile}\"")))
-
-(rule
-  (target configOcaml.ml)
-  (mode (promote (until-clean) (only configOcaml.ml))) ; replace existing file in source tree, even if releasing (only overrides)
-  (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet flambda = \"%{ocaml-config:flambda}\"")))
-
 (rule
   (alias runtest)
   (deps ../goblint ../scripts/update_suite.rb ../Makefile ../make.sh (source_tree ../tests/regression) (source_tree ../includes) (source_tree ../linux-headers))
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 5cefc1a7de..9baa2dd1ca 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -529,7 +529,7 @@ struct
             GobConfig.write_file config;
             let module Meta = struct
                 type t = { command : string; version: string; timestamp : float; localtime : string } [@@deriving to_yojson]
-                let json = to_yojson { command = GobSys.command_line; version = Version.goblint; timestamp = Unix.time (); localtime = GobUnix.localtime () }
+                let json = to_yojson { command = GobSys.command_line; version = Goblint_build_info.version; timestamp = Unix.time (); localtime = GobUnix.localtime () }
               end
             in
             (* Yojson.Safe.to_file meta Meta.json; *)
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 816a69faff..e009ecf86b 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -452,21 +452,6 @@ module PrivPrecCompareUtil = PrivPrecCompareUtil
 module RelationPrecCompareUtil = RelationPrecCompareUtil
 module ApronPrecCompareUtil = ApronPrecCompareUtil
 
-(** {2 Build info} *)
-
-(** OCaml compiler info. *)
-module ConfigOcaml = ConfigOcaml
-
-(** Dune profile info. *)
-module ConfigProfile = ConfigProfile
-
-(** Goblint version info. *)
-module Version = Version
-
-(** Goblint git version info. *)
-module ConfigVersion = ConfigVersion
-
-
 (** {1 Library extensions}
 
     OCaml library extensions which are completely independent of Goblint.
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 7808cbcd3f..98363233a2 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -9,11 +9,11 @@ let writeconffile = ref None
 
 (** Print version and bail. *)
 let print_version ch =
-  printf "Goblint version: %s\n" Version.goblint;
+  printf "Goblint version: %s\n" Goblint_build_info.version;
   printf "Cil version:     %s\n" Cil.cilVersion;
-  printf "Dune profile:    %s\n" ConfigProfile.profile;
+  printf "Dune profile:    %s\n" Goblint_build_info.dune_profile;
   printf "OCaml version:   %s\n" Sys.ocaml_version;
-  printf "OCaml flambda:   %s\n" ConfigOcaml.flambda;
+  printf "OCaml flambda:   %s\n" Goblint_build_info.ocaml_flambda;
   if get_bool "dbg.verbose" then (
     printf "Library versions:\n";
     List.iter (fun (name, version) ->
diff --git a/src/util/sarif.ml b/src/util/sarif.ml
index 4374da46d7..7620384cc4 100644
--- a/src/util/sarif.ml
+++ b/src/util/sarif.ml
@@ -26,7 +26,7 @@ let goblintTool: Tool.t = {
     fullName = "Goblint static analyser";
     informationUri = "https://goblint.in.tum.de/home";
     organization = "TUM - i2 and UTartu - SWS";
-    version = Version.goblint;
+    version = Goblint_build_info.version;
     rules = List.map transformToReportingDescriptor (List.map (fun rule -> rule.name) rules)
   };
 }
diff --git a/src/util/tracing.ml b/src/util/tracing.ml
index f9dff2c2cf..ad8892c396 100644
--- a/src/util/tracing.ml
+++ b/src/util/tracing.ml
@@ -10,7 +10,7 @@ open Pretty
 module Strs = Set.Make (String)
 
 
-let tracing = ConfigProfile.profile = "trace"
+let tracing = Goblint_build_info.dune_profile = "trace"
 
 let current_loc = ref locUnknown
 let next_loc    = ref locUnknown
diff --git a/src/version.ml b/src/version.ml
deleted file mode 100644
index cbe2874608..0000000000
--- a/src/version.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-let release = "%%VERSION_NUM%%"
-let release_commit = "%%VCS_COMMIT_ID%%"
-
-let goblint =
-  let commit = ConfigVersion.version in
-  if BatString.starts_with release "%" then
-    commit
-  else (
-    let commit =
-      if commit = "n/a" then (* released archive has no .git *)
-        release_commit
-      else
-        commit
-    in
-    Format.sprintf "%s (%s)" release commit
-  )
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 0e237716fd..fb1604f03e 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -118,7 +118,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
       | Result.Unknown -> "unknown_witness"
     );
   GML.write_metadata g "sourcecodelang" "C";
-  GML.write_metadata g "producer" (Printf.sprintf "Goblint (%s)" Version.goblint);
+  GML.write_metadata g "producer" (Printf.sprintf "Goblint (%s)" Goblint_build_info.version);
   GML.write_metadata g "specification" (Svcomp.Specification.to_string Task.specification);
   let programfile = (Node.location (N.cfgnode main_entry)).file in
   GML.write_metadata g "programfile" programfile;
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index c7106a57b5..72ff21f6bd 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -17,7 +17,7 @@ struct
   (* let yaml_conf: Yaml.value = Json_repr.convert (module Json_repr.Yojson) (module Json_repr.Ezjsonm) (!GobConfig.json_conf) in *)
   let producer: Producer.t = {
     name = "Goblint";
-    version = Version.goblint;
+    version = Goblint_build_info.version;
     command_line = Some GobSys.command_line;
   }
 

From d723fdef0bf9e17625c141ed44a0e9d271e0609d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 Oct 2023 15:48:41 +0300
Subject: [PATCH 03/10] Extract widely used modules to common dune library

---
 src/{util => common}/afterConfig.ml        |  0
 src/{framework => common}/analysisState.ml |  0
 src/{cdomains => common}/basetype.ml       |  0
 src/{util => common}/cilType.ml            |  0
 src/{util => common}/cilfacade.ml          |  0
 src/{util => common}/cilfacade0.ml         |  0
 src/{framework => common}/controlSpecC.ml  |  0
 src/{framework => common}/controlSpecC.mli |  0
 src/common/dune                            | 28 ++++++++++++++++++++++
 src/{framework => common}/edge.ml          |  0
 src/{util => common}/gobConfig.ml          |  0
 src/{util => common}/gobFormat.ml          |  0
 src/{util => common}/jsonSchema.ml         |  0
 src/{domains => common}/lattice.ml         |  0
 src/{util => common}/lazyEval.ml           |  0
 src/{util => common}/messageCategory.ml    |  0
 src/{util => common}/messageUtil.ml        |  0
 src/{util => common}/messages.ml           |  0
 src/{framework => common}/myCFG.ml         |  0
 src/{domains => common}/myCheck.ml         |  0
 src/{framework => common}/node.ml          |  0
 src/{framework => common}/node0.ml         |  0
 src/{util => common}/options.ml            |  0
 src/{util => common}/options.schema.json   |  0
 src/{domains => common}/printable.ml       |  0
 src/{util => common}/resettableLazy.ml     |  0
 src/{util => common}/resettableLazy.mli    |  0
 src/{util => common}/richVarinfo.ml        |  0
 src/{util => common}/richVarinfo.mli       |  0
 src/{util => common}/timing.ml             |  0
 src/{util => common}/tracing.ml            |  0
 src/{incremental => common}/updateCil0.ml  |  0
 src/{util => common}/xmlUtil.ml            |  0
 src/dune                                   |  3 +--
 34 files changed, 29 insertions(+), 2 deletions(-)
 rename src/{util => common}/afterConfig.ml (100%)
 rename src/{framework => common}/analysisState.ml (100%)
 rename src/{cdomains => common}/basetype.ml (100%)
 rename src/{util => common}/cilType.ml (100%)
 rename src/{util => common}/cilfacade.ml (100%)
 rename src/{util => common}/cilfacade0.ml (100%)
 rename src/{framework => common}/controlSpecC.ml (100%)
 rename src/{framework => common}/controlSpecC.mli (100%)
 create mode 100644 src/common/dune
 rename src/{framework => common}/edge.ml (100%)
 rename src/{util => common}/gobConfig.ml (100%)
 rename src/{util => common}/gobFormat.ml (100%)
 rename src/{util => common}/jsonSchema.ml (100%)
 rename src/{domains => common}/lattice.ml (100%)
 rename src/{util => common}/lazyEval.ml (100%)
 rename src/{util => common}/messageCategory.ml (100%)
 rename src/{util => common}/messageUtil.ml (100%)
 rename src/{util => common}/messages.ml (100%)
 rename src/{framework => common}/myCFG.ml (100%)
 rename src/{domains => common}/myCheck.ml (100%)
 rename src/{framework => common}/node.ml (100%)
 rename src/{framework => common}/node0.ml (100%)
 rename src/{util => common}/options.ml (100%)
 rename src/{util => common}/options.schema.json (100%)
 rename src/{domains => common}/printable.ml (100%)
 rename src/{util => common}/resettableLazy.ml (100%)
 rename src/{util => common}/resettableLazy.mli (100%)
 rename src/{util => common}/richVarinfo.ml (100%)
 rename src/{util => common}/richVarinfo.mli (100%)
 rename src/{util => common}/timing.ml (100%)
 rename src/{util => common}/tracing.ml (100%)
 rename src/{incremental => common}/updateCil0.ml (100%)
 rename src/{util => common}/xmlUtil.ml (100%)

diff --git a/src/util/afterConfig.ml b/src/common/afterConfig.ml
similarity index 100%
rename from src/util/afterConfig.ml
rename to src/common/afterConfig.ml
diff --git a/src/framework/analysisState.ml b/src/common/analysisState.ml
similarity index 100%
rename from src/framework/analysisState.ml
rename to src/common/analysisState.ml
diff --git a/src/cdomains/basetype.ml b/src/common/basetype.ml
similarity index 100%
rename from src/cdomains/basetype.ml
rename to src/common/basetype.ml
diff --git a/src/util/cilType.ml b/src/common/cilType.ml
similarity index 100%
rename from src/util/cilType.ml
rename to src/common/cilType.ml
diff --git a/src/util/cilfacade.ml b/src/common/cilfacade.ml
similarity index 100%
rename from src/util/cilfacade.ml
rename to src/common/cilfacade.ml
diff --git a/src/util/cilfacade0.ml b/src/common/cilfacade0.ml
similarity index 100%
rename from src/util/cilfacade0.ml
rename to src/common/cilfacade0.ml
diff --git a/src/framework/controlSpecC.ml b/src/common/controlSpecC.ml
similarity index 100%
rename from src/framework/controlSpecC.ml
rename to src/common/controlSpecC.ml
diff --git a/src/framework/controlSpecC.mli b/src/common/controlSpecC.mli
similarity index 100%
rename from src/framework/controlSpecC.mli
rename to src/common/controlSpecC.mli
diff --git a/src/common/dune b/src/common/dune
new file mode 100644
index 0000000000..03a93a3030
--- /dev/null
+++ b/src/common/dune
@@ -0,0 +1,28 @@
+(include_subdirs no)
+
+(library
+ (name goblint_common)
+ (public_name goblint.common)
+ (wrapped false) ; TODO: wrap
+ (libraries
+   batteries
+   zarith
+   goblint_std
+   goblint-cil
+   fpath
+   yojson
+   json-data-encoding
+   cpu
+   goblint_timing
+   goblint_build_info
+   goblint.sites
+   qcheck-core.runner)
+ (flags :standard -open Goblint_std)
+ (preprocess
+  (pps
+    ppx_deriving.std
+    ppx_deriving_hash
+    ppx_deriving_yojson
+    ppx_blob))
+ (preprocessor_deps (file options.schema.json)))
+
diff --git a/src/framework/edge.ml b/src/common/edge.ml
similarity index 100%
rename from src/framework/edge.ml
rename to src/common/edge.ml
diff --git a/src/util/gobConfig.ml b/src/common/gobConfig.ml
similarity index 100%
rename from src/util/gobConfig.ml
rename to src/common/gobConfig.ml
diff --git a/src/util/gobFormat.ml b/src/common/gobFormat.ml
similarity index 100%
rename from src/util/gobFormat.ml
rename to src/common/gobFormat.ml
diff --git a/src/util/jsonSchema.ml b/src/common/jsonSchema.ml
similarity index 100%
rename from src/util/jsonSchema.ml
rename to src/common/jsonSchema.ml
diff --git a/src/domains/lattice.ml b/src/common/lattice.ml
similarity index 100%
rename from src/domains/lattice.ml
rename to src/common/lattice.ml
diff --git a/src/util/lazyEval.ml b/src/common/lazyEval.ml
similarity index 100%
rename from src/util/lazyEval.ml
rename to src/common/lazyEval.ml
diff --git a/src/util/messageCategory.ml b/src/common/messageCategory.ml
similarity index 100%
rename from src/util/messageCategory.ml
rename to src/common/messageCategory.ml
diff --git a/src/util/messageUtil.ml b/src/common/messageUtil.ml
similarity index 100%
rename from src/util/messageUtil.ml
rename to src/common/messageUtil.ml
diff --git a/src/util/messages.ml b/src/common/messages.ml
similarity index 100%
rename from src/util/messages.ml
rename to src/common/messages.ml
diff --git a/src/framework/myCFG.ml b/src/common/myCFG.ml
similarity index 100%
rename from src/framework/myCFG.ml
rename to src/common/myCFG.ml
diff --git a/src/domains/myCheck.ml b/src/common/myCheck.ml
similarity index 100%
rename from src/domains/myCheck.ml
rename to src/common/myCheck.ml
diff --git a/src/framework/node.ml b/src/common/node.ml
similarity index 100%
rename from src/framework/node.ml
rename to src/common/node.ml
diff --git a/src/framework/node0.ml b/src/common/node0.ml
similarity index 100%
rename from src/framework/node0.ml
rename to src/common/node0.ml
diff --git a/src/util/options.ml b/src/common/options.ml
similarity index 100%
rename from src/util/options.ml
rename to src/common/options.ml
diff --git a/src/util/options.schema.json b/src/common/options.schema.json
similarity index 100%
rename from src/util/options.schema.json
rename to src/common/options.schema.json
diff --git a/src/domains/printable.ml b/src/common/printable.ml
similarity index 100%
rename from src/domains/printable.ml
rename to src/common/printable.ml
diff --git a/src/util/resettableLazy.ml b/src/common/resettableLazy.ml
similarity index 100%
rename from src/util/resettableLazy.ml
rename to src/common/resettableLazy.ml
diff --git a/src/util/resettableLazy.mli b/src/common/resettableLazy.mli
similarity index 100%
rename from src/util/resettableLazy.mli
rename to src/common/resettableLazy.mli
diff --git a/src/util/richVarinfo.ml b/src/common/richVarinfo.ml
similarity index 100%
rename from src/util/richVarinfo.ml
rename to src/common/richVarinfo.ml
diff --git a/src/util/richVarinfo.mli b/src/common/richVarinfo.mli
similarity index 100%
rename from src/util/richVarinfo.mli
rename to src/common/richVarinfo.mli
diff --git a/src/util/timing.ml b/src/common/timing.ml
similarity index 100%
rename from src/util/timing.ml
rename to src/common/timing.ml
diff --git a/src/util/tracing.ml b/src/common/tracing.ml
similarity index 100%
rename from src/util/tracing.ml
rename to src/common/tracing.ml
diff --git a/src/incremental/updateCil0.ml b/src/common/updateCil0.ml
similarity index 100%
rename from src/incremental/updateCil0.ml
rename to src/common/updateCil0.ml
diff --git a/src/util/xmlUtil.ml b/src/common/xmlUtil.ml
similarity index 100%
rename from src/util/xmlUtil.ml
rename to src/common/xmlUtil.ml
diff --git a/src/dune b/src/dune
index 5fdf58a5b2..df19f85340 100644
--- a/src/dune
+++ b/src/dune
@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint mainspec 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
+  (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_common
     ; 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.
@@ -61,7 +61,6 @@
   (ocamlopt_flags :standard -no-float-const-prop)
   (preprocess
     (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson ppx_blob))
-  (preprocessor_deps (file util/options.schema.json))
   (instrumentation (backend bisect_ppx))
 )
 

From 6fd299852648e1dde28eeb0b70e5684b9f471dab Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 16:09:39 +0300
Subject: [PATCH 04/10] Fix references to options.schema.json

---
 .github/workflows/options.yml  | 6 +++---
 .readthedocs.yaml              | 2 +-
 docs/user-guide/configuring.md | 2 +-
 src/common/options.ml          | 2 +-
 src/goblint_lib.ml             | 2 +-
 5 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
index b5f690a700..84906d4949 100644
--- a/.github/workflows/options.yml
+++ b/.github/workflows/options.yml
@@ -26,10 +26,10 @@ jobs:
         run: npm install -g ajv-cli
 
       - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
-        run: ajv migrate -s src/util/options.schema.json
+        run: ajv migrate -s src/common/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/util/options.schema.json -d "conf/**/*.json"
+        run: ajv validate -s src/common/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
-        run: ajv validate -s src/util/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/common/options.schema.json -d "tests/incremental/*/*.json"
diff --git a/.readthedocs.yaml b/.readthedocs.yaml
index c9b41df49d..4827b825ef 100644
--- a/.readthedocs.yaml
+++ b/.readthedocs.yaml
@@ -20,4 +20,4 @@ build:
       - pip install json-schema-for-humans
     post_build:
       - mkdir _readthedocs/html/jsfh/
-      - generate-schema-doc --config-file jsfh.yml src/util/options.schema.json _readthedocs/html/jsfh/
+      - generate-schema-doc --config-file jsfh.yml src/common/options.schema.json _readthedocs/html/jsfh/
diff --git a/docs/user-guide/configuring.md b/docs/user-guide/configuring.md
index 82e92f6fe7..348e15dac4 100644
--- a/docs/user-guide/configuring.md
+++ b/docs/user-guide/configuring.md
@@ -24,7 +24,7 @@ In `.vscode/settings.json` add the following:
                 "/conf/*.json",
                 "/tests/incremental/*/*.json"
             ],
-            "url": "/src/util/options.schema.json"
+            "url": "/src/common/options.schema.json"
         }
     ]
 }
diff --git a/src/common/options.ml b/src/common/options.ml
index d352c86465..c9bd41038f 100644
--- a/src/common/options.ml
+++ b/src/common/options.ml
@@ -1,4 +1,4 @@
-(** [src/util/options.schema.json] low-level access. *)
+(** [src/common/options.schema.json] low-level access. *)
 
 open Json_schema
 
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index e009ecf86b..a108058291 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -49,7 +49,7 @@ module VarQuery = VarQuery
 (** {2 Configuration}
 
     Runtime configuration is represented as JSON.
-    Options are specified and documented by the JSON schema [src/util/options.schema.json]. *)
+    Options are specified and documented by the JSON schema [src/common/options.schema.json]. *)
 
 module GobConfig = GobConfig
 module AfterConfig = AfterConfig

From 809f84b905a4b85f6e56d7fc74a5d252dfe90a5e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 16:12:52 +0300
Subject: [PATCH 05/10] Update Gobview for goblint.common

---
 gobview | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gobview b/gobview
index b373d06174..41be36b548 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit b373d06174667537b671f3122daf4ebd4b195aea
+Subproject commit 41be36b54837b24e6de83740c34e810d3d1afdfb

From 3281c74399a6f4b9c16a64ca11e041897ff36d9a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 11 Oct 2023 17:54:59 +0300
Subject: [PATCH 06/10] Temporarily reintroduce old unqualified directory
 structure inside common library

---
 .github/workflows/options.yml               | 6 +++---
 .readthedocs.yaml                           | 2 +-
 docs/user-guide/configuring.md              | 2 +-
 src/common/{ => cdomains}/basetype.ml       | 0
 src/common/{ => domains}/lattice.ml         | 0
 src/common/{ => domains}/myCheck.ml         | 0
 src/common/{ => domains}/printable.ml       | 0
 src/common/dune                             | 4 ++--
 src/common/{ => framework}/analysisState.ml | 0
 src/common/{ => framework}/controlSpecC.ml  | 0
 src/common/{ => framework}/controlSpecC.mli | 0
 src/common/{ => framework}/edge.ml          | 0
 src/common/{ => framework}/myCFG.ml         | 0
 src/common/{ => framework}/node.ml          | 0
 src/common/{ => framework}/node0.ml         | 0
 src/common/{ => incremental}/updateCil0.ml  | 0
 src/common/{ => util}/afterConfig.ml        | 0
 src/common/{ => util}/cilType.ml            | 0
 src/common/{ => util}/cilfacade.ml          | 0
 src/common/{ => util}/cilfacade0.ml         | 0
 src/common/{ => util}/gobConfig.ml          | 0
 src/common/{ => util}/gobFormat.ml          | 0
 src/common/{ => util}/jsonSchema.ml         | 0
 src/common/{ => util}/lazyEval.ml           | 0
 src/common/{ => util}/messageCategory.ml    | 0
 src/common/{ => util}/messageUtil.ml        | 0
 src/common/{ => util}/messages.ml           | 0
 src/common/{ => util}/options.ml            | 2 +-
 src/common/{ => util}/options.schema.json   | 0
 src/common/{ => util}/resettableLazy.ml     | 0
 src/common/{ => util}/resettableLazy.mli    | 0
 src/common/{ => util}/richVarinfo.ml        | 0
 src/common/{ => util}/richVarinfo.mli       | 0
 src/common/{ => util}/timing.ml             | 0
 src/common/{ => util}/tracing.ml            | 0
 src/common/{ => util}/xmlUtil.ml            | 0
 src/goblint_lib.ml                          | 2 +-
 37 files changed, 9 insertions(+), 9 deletions(-)
 rename src/common/{ => cdomains}/basetype.ml (100%)
 rename src/common/{ => domains}/lattice.ml (100%)
 rename src/common/{ => domains}/myCheck.ml (100%)
 rename src/common/{ => domains}/printable.ml (100%)
 rename src/common/{ => framework}/analysisState.ml (100%)
 rename src/common/{ => framework}/controlSpecC.ml (100%)
 rename src/common/{ => framework}/controlSpecC.mli (100%)
 rename src/common/{ => framework}/edge.ml (100%)
 rename src/common/{ => framework}/myCFG.ml (100%)
 rename src/common/{ => framework}/node.ml (100%)
 rename src/common/{ => framework}/node0.ml (100%)
 rename src/common/{ => incremental}/updateCil0.ml (100%)
 rename src/common/{ => util}/afterConfig.ml (100%)
 rename src/common/{ => util}/cilType.ml (100%)
 rename src/common/{ => util}/cilfacade.ml (100%)
 rename src/common/{ => util}/cilfacade0.ml (100%)
 rename src/common/{ => util}/gobConfig.ml (100%)
 rename src/common/{ => util}/gobFormat.ml (100%)
 rename src/common/{ => util}/jsonSchema.ml (100%)
 rename src/common/{ => util}/lazyEval.ml (100%)
 rename src/common/{ => util}/messageCategory.ml (100%)
 rename src/common/{ => util}/messageUtil.ml (100%)
 rename src/common/{ => util}/messages.ml (100%)
 rename src/common/{ => util}/options.ml (98%)
 rename src/common/{ => util}/options.schema.json (100%)
 rename src/common/{ => util}/resettableLazy.ml (100%)
 rename src/common/{ => util}/resettableLazy.mli (100%)
 rename src/common/{ => util}/richVarinfo.ml (100%)
 rename src/common/{ => util}/richVarinfo.mli (100%)
 rename src/common/{ => util}/timing.ml (100%)
 rename src/common/{ => util}/tracing.ml (100%)
 rename src/common/{ => util}/xmlUtil.ml (100%)

diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
index 84906d4949..40652791fa 100644
--- a/.github/workflows/options.yml
+++ b/.github/workflows/options.yml
@@ -26,10 +26,10 @@ jobs:
         run: npm install -g ajv-cli
 
       - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
-        run: ajv migrate -s src/common/options.schema.json
+        run: ajv migrate -s src/common/util/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/common/options.schema.json -d "conf/**/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
-        run: ajv validate -s src/common/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json"
diff --git a/.readthedocs.yaml b/.readthedocs.yaml
index 4827b825ef..08044d195c 100644
--- a/.readthedocs.yaml
+++ b/.readthedocs.yaml
@@ -20,4 +20,4 @@ build:
       - pip install json-schema-for-humans
     post_build:
       - mkdir _readthedocs/html/jsfh/
-      - generate-schema-doc --config-file jsfh.yml src/common/options.schema.json _readthedocs/html/jsfh/
+      - generate-schema-doc --config-file jsfh.yml src/common/util/options.schema.json _readthedocs/html/jsfh/
diff --git a/docs/user-guide/configuring.md b/docs/user-guide/configuring.md
index 348e15dac4..9a32a14a4c 100644
--- a/docs/user-guide/configuring.md
+++ b/docs/user-guide/configuring.md
@@ -24,7 +24,7 @@ In `.vscode/settings.json` add the following:
                 "/conf/*.json",
                 "/tests/incremental/*/*.json"
             ],
-            "url": "/src/common/options.schema.json"
+            "url": "/src/common/util/options.schema.json"
         }
     ]
 }
diff --git a/src/common/basetype.ml b/src/common/cdomains/basetype.ml
similarity index 100%
rename from src/common/basetype.ml
rename to src/common/cdomains/basetype.ml
diff --git a/src/common/lattice.ml b/src/common/domains/lattice.ml
similarity index 100%
rename from src/common/lattice.ml
rename to src/common/domains/lattice.ml
diff --git a/src/common/myCheck.ml b/src/common/domains/myCheck.ml
similarity index 100%
rename from src/common/myCheck.ml
rename to src/common/domains/myCheck.ml
diff --git a/src/common/printable.ml b/src/common/domains/printable.ml
similarity index 100%
rename from src/common/printable.ml
rename to src/common/domains/printable.ml
diff --git a/src/common/dune b/src/common/dune
index 03a93a3030..b937ecdd02 100644
--- a/src/common/dune
+++ b/src/common/dune
@@ -1,4 +1,4 @@
-(include_subdirs no)
+(include_subdirs unqualified)
 
 (library
  (name goblint_common)
@@ -24,5 +24,5 @@
     ppx_deriving_hash
     ppx_deriving_yojson
     ppx_blob))
- (preprocessor_deps (file options.schema.json)))
+ (preprocessor_deps (file util/options.schema.json)))
 
diff --git a/src/common/analysisState.ml b/src/common/framework/analysisState.ml
similarity index 100%
rename from src/common/analysisState.ml
rename to src/common/framework/analysisState.ml
diff --git a/src/common/controlSpecC.ml b/src/common/framework/controlSpecC.ml
similarity index 100%
rename from src/common/controlSpecC.ml
rename to src/common/framework/controlSpecC.ml
diff --git a/src/common/controlSpecC.mli b/src/common/framework/controlSpecC.mli
similarity index 100%
rename from src/common/controlSpecC.mli
rename to src/common/framework/controlSpecC.mli
diff --git a/src/common/edge.ml b/src/common/framework/edge.ml
similarity index 100%
rename from src/common/edge.ml
rename to src/common/framework/edge.ml
diff --git a/src/common/myCFG.ml b/src/common/framework/myCFG.ml
similarity index 100%
rename from src/common/myCFG.ml
rename to src/common/framework/myCFG.ml
diff --git a/src/common/node.ml b/src/common/framework/node.ml
similarity index 100%
rename from src/common/node.ml
rename to src/common/framework/node.ml
diff --git a/src/common/node0.ml b/src/common/framework/node0.ml
similarity index 100%
rename from src/common/node0.ml
rename to src/common/framework/node0.ml
diff --git a/src/common/updateCil0.ml b/src/common/incremental/updateCil0.ml
similarity index 100%
rename from src/common/updateCil0.ml
rename to src/common/incremental/updateCil0.ml
diff --git a/src/common/afterConfig.ml b/src/common/util/afterConfig.ml
similarity index 100%
rename from src/common/afterConfig.ml
rename to src/common/util/afterConfig.ml
diff --git a/src/common/cilType.ml b/src/common/util/cilType.ml
similarity index 100%
rename from src/common/cilType.ml
rename to src/common/util/cilType.ml
diff --git a/src/common/cilfacade.ml b/src/common/util/cilfacade.ml
similarity index 100%
rename from src/common/cilfacade.ml
rename to src/common/util/cilfacade.ml
diff --git a/src/common/cilfacade0.ml b/src/common/util/cilfacade0.ml
similarity index 100%
rename from src/common/cilfacade0.ml
rename to src/common/util/cilfacade0.ml
diff --git a/src/common/gobConfig.ml b/src/common/util/gobConfig.ml
similarity index 100%
rename from src/common/gobConfig.ml
rename to src/common/util/gobConfig.ml
diff --git a/src/common/gobFormat.ml b/src/common/util/gobFormat.ml
similarity index 100%
rename from src/common/gobFormat.ml
rename to src/common/util/gobFormat.ml
diff --git a/src/common/jsonSchema.ml b/src/common/util/jsonSchema.ml
similarity index 100%
rename from src/common/jsonSchema.ml
rename to src/common/util/jsonSchema.ml
diff --git a/src/common/lazyEval.ml b/src/common/util/lazyEval.ml
similarity index 100%
rename from src/common/lazyEval.ml
rename to src/common/util/lazyEval.ml
diff --git a/src/common/messageCategory.ml b/src/common/util/messageCategory.ml
similarity index 100%
rename from src/common/messageCategory.ml
rename to src/common/util/messageCategory.ml
diff --git a/src/common/messageUtil.ml b/src/common/util/messageUtil.ml
similarity index 100%
rename from src/common/messageUtil.ml
rename to src/common/util/messageUtil.ml
diff --git a/src/common/messages.ml b/src/common/util/messages.ml
similarity index 100%
rename from src/common/messages.ml
rename to src/common/util/messages.ml
diff --git a/src/common/options.ml b/src/common/util/options.ml
similarity index 98%
rename from src/common/options.ml
rename to src/common/util/options.ml
index c9bd41038f..3046f70809 100644
--- a/src/common/options.ml
+++ b/src/common/util/options.ml
@@ -1,4 +1,4 @@
-(** [src/common/options.schema.json] low-level access. *)
+(** [src/common/util/options.schema.json] low-level access. *)
 
 open Json_schema
 
diff --git a/src/common/options.schema.json b/src/common/util/options.schema.json
similarity index 100%
rename from src/common/options.schema.json
rename to src/common/util/options.schema.json
diff --git a/src/common/resettableLazy.ml b/src/common/util/resettableLazy.ml
similarity index 100%
rename from src/common/resettableLazy.ml
rename to src/common/util/resettableLazy.ml
diff --git a/src/common/resettableLazy.mli b/src/common/util/resettableLazy.mli
similarity index 100%
rename from src/common/resettableLazy.mli
rename to src/common/util/resettableLazy.mli
diff --git a/src/common/richVarinfo.ml b/src/common/util/richVarinfo.ml
similarity index 100%
rename from src/common/richVarinfo.ml
rename to src/common/util/richVarinfo.ml
diff --git a/src/common/richVarinfo.mli b/src/common/util/richVarinfo.mli
similarity index 100%
rename from src/common/richVarinfo.mli
rename to src/common/util/richVarinfo.mli
diff --git a/src/common/timing.ml b/src/common/util/timing.ml
similarity index 100%
rename from src/common/timing.ml
rename to src/common/util/timing.ml
diff --git a/src/common/tracing.ml b/src/common/util/tracing.ml
similarity index 100%
rename from src/common/tracing.ml
rename to src/common/util/tracing.ml
diff --git a/src/common/xmlUtil.ml b/src/common/util/xmlUtil.ml
similarity index 100%
rename from src/common/xmlUtil.ml
rename to src/common/util/xmlUtil.ml
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index a108058291..0b3829f11c 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -49,7 +49,7 @@ module VarQuery = VarQuery
 (** {2 Configuration}
 
     Runtime configuration is represented as JSON.
-    Options are specified and documented by the JSON schema [src/common/options.schema.json]. *)
+    Options are specified and documented by the JSON schema [src/common/util/options.schema.json]. *)
 
 module GobConfig = GobConfig
 module AfterConfig = AfterConfig

From 956efd86e8f63aa75bc54808649354c4f7659e8b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 Oct 2023 10:39:24 +0300
Subject: [PATCH 07/10] Fix indentation in moved common library files

---
 src/common/domains/lattice.ml      | 16 ++++++++--------
 src/common/util/lazyEval.ml        | 14 +++++++-------
 src/common/util/messageCategory.ml |  4 ++--
 3 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/common/domains/lattice.ml b/src/common/domains/lattice.ml
index 4cdaa8fb9f..79455aea62 100644
--- a/src/common/domains/lattice.ml
+++ b/src/common/domains/lattice.ml
@@ -4,12 +4,12 @@
 module Pretty = GoblintCil.Pretty
 
 (* module type Rel =
-sig
-  type t
-  type relation = Less | Equal | Greater | Uncomparable
-  val rel : t -> t -> relation
-  val in_rel : t -> relation -> t -> bool
-end *)
+   sig
+     type t
+     type relation = Less | Equal | Greater | Uncomparable
+     val rel : t -> t -> relation
+     val in_rel : t -> relation -> t -> bool
+   end *)
 
 (* partial order: elements might not be comparable and no bot/top -> join etc. might fail with exception Uncomparable *)
 exception Uncomparable
@@ -324,14 +324,14 @@ struct
     match (x,y) with
     | (`Lifted x, `Lifted y) ->
       (try `Lifted (Base.widen x y)
-      with Uncomparable -> `Top)
+       with Uncomparable -> `Top)
     | _ -> y
 
   let narrow x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) ->
       (try `Lifted (Base.narrow x y)
-      with Uncomparable -> `Bot)
+       with Uncomparable -> `Bot)
     | _ -> x
 end
 
diff --git a/src/common/util/lazyEval.ml b/src/common/util/lazyEval.ml
index e49a5f4693..9007cdd089 100644
--- a/src/common/util/lazyEval.ml
+++ b/src/common/util/lazyEval.ml
@@ -5,10 +5,10 @@
    Node -> CilType -> Printable -> Goblintutil -> GobConfig -> Tracing -> Node *)
 
 module Make (M : sig
-  type t
-  type result
-  val eval : t -> result
-end) : sig
+    type t
+    type result
+    val eval : t -> result
+  end) : sig
   type t
   val make : M.t -> t
   val force : t -> M.result
@@ -20,8 +20,8 @@ end = struct
   let force l =
     match l.value with
     | `Closure arg ->
-        let v = M.eval arg in
-        l.value <- `Computed v;
-        v
+      let v = M.eval arg in
+      l.value <- `Computed v;
+      v
     | `Computed v -> v
 end
diff --git a/src/common/util/messageCategory.ml b/src/common/util/messageCategory.ml
index 1bb31d6d5b..c70b8faf5f 100644
--- a/src/common/util/messageCategory.ml
+++ b/src/common/util/messageCategory.ml
@@ -260,8 +260,8 @@ let categoryName = function
 
   | Behavior x -> behaviorName x
   | Integer x -> (match x with
-    | Overflow -> "Overflow";
-    | DivByZero -> "DivByZero")
+      | Overflow -> "Overflow";
+      | DivByZero -> "DivByZero")
   | Float -> "Float"
 
 

From 59462c3e2614d79f63a4b8376b2304050f24f6d6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 Oct 2023 10:52:20 +0300
Subject: [PATCH 08/10] Use batteries.unthreaded everywhere to avoid Gobview
 exception

---
 gobview           | 2 +-
 src/common/dune   | 2 +-
 src/util/std/dune | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/gobview b/gobview
index 41be36b548..42b07f8253 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 41be36b54837b24e6de83740c34e810d3d1afdfb
+Subproject commit 42b07f825316052ec030370daf0d00ebe28ec092
diff --git a/src/common/dune b/src/common/dune
index b937ecdd02..c9ed9f9db2 100644
--- a/src/common/dune
+++ b/src/common/dune
@@ -5,7 +5,7 @@
  (public_name goblint.common)
  (wrapped false) ; TODO: wrap
  (libraries
-   batteries
+   batteries.unthreaded
    zarith
    goblint_std
    goblint-cil
diff --git a/src/util/std/dune b/src/util/std/dune
index c85710a8d6..c6961a1725 100644
--- a/src/util/std/dune
+++ b/src/util/std/dune
@@ -4,7 +4,7 @@
  (name goblint_std)
  (public_name goblint.std)
  (libraries
-   batteries
+   batteries.unthreaded
    zarith
    goblint-cil
    fpath

From a0b376bfa6c587e293172c6d86aa2a1085ddb5c3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 Oct 2023 11:40:03 +0300
Subject: [PATCH 09/10] Add odoc page for package

---
 src/common/common.mld | 74 +++++++++++++++++++++++++++++++++++++++++++
 src/common/dune       |  1 +
 src/dune              |  2 ++
 src/goblint_lib.ml    |  1 +
 src/index.mld         | 51 +++++++++++++++++++++++++++++
 5 files changed, 129 insertions(+)
 create mode 100644 src/common/common.mld
 create mode 100644 src/index.mld

diff --git a/src/common/common.mld b/src/common/common.mld
new file mode 100644
index 0000000000..662c789572
--- /dev/null
+++ b/src/common/common.mld
@@ -0,0 +1,74 @@
+{0 Library goblint.common}
+This library is unwrapped and provides the following top-level modules.
+For better context, see {!Goblint_lib} which also documents these modules.
+
+
+{1 Framework}
+
+{2 CFG}
+{!modules:
+Node
+Edge
+MyCFG
+}
+
+{2 Specification}
+{!modules:
+AnalysisState
+ControlSpecC
+}
+
+{2 Configuration}
+{!modules:
+GobConfig
+AfterConfig
+JsonSchema
+Options
+}
+
+
+{1 Domains}
+{!modules:
+Printable
+Lattice
+}
+
+{2 Analysis-specific}
+
+{3 Other}
+{!modules:Basetype}
+
+
+{1 I/O}
+{!modules:
+Messages
+Tracing
+}
+
+
+{1 Utilities}
+{!modules:Timing}
+
+{2 General}
+{!modules:
+LazyEval
+ResettableLazy
+MessageUtil
+XmlUtil
+}
+
+{2 CIL}
+{!modules:
+CilType
+Cilfacade
+RichVarinfo
+}
+
+
+{1 Library extensions}
+
+{2 Standard library}
+{!modules:GobFormat}
+
+{2 Other libraries}
+{!modules:MyCheck}
diff --git a/src/common/dune b/src/common/dune
index c9ed9f9db2..c8f1564782 100644
--- a/src/common/dune
+++ b/src/common/dune
@@ -26,3 +26,4 @@
     ppx_blob))
  (preprocessor_deps (file util/options.schema.json)))
 
+(documentation)
diff --git a/src/dune b/src/dune
index df19f85340..acd5348acb 100644
--- a/src/dune
+++ b/src/dune
@@ -125,3 +125,5 @@
     (flags (:standard -warn-error -A -w -unused-var-strict -w -unused-functor-parameter -w +9)) ; https://dune.readthedocs.io/en/stable/faq.html#how-to-make-warnings-non-fatal
   )
 )
+
+(documentation)
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 0b3829f11c..dadeb2cda1 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -1,3 +1,4 @@
+(** Main library. *)
 
 (** {1 Framework} *)
 
diff --git a/src/index.mld b/src/index.mld
new file mode 100644
index 0000000000..2afbbc97ae
--- /dev/null
+++ b/src/index.mld
@@ -0,0 +1,51 @@
+{0 goblint index}
+
+{1 Goblint}
+The following libraries make up Goblint's main codebase.
+
+{2 Library goblint.lib}
+{!modules:Goblint_lib}
+This library currently contains the majority of Goblint and is in the process of being split into smaller libraries.
+
+{2 Library goblint.common}
+This {{!page-common}unwrapped library} contains various common modules extracted from {!Goblint_lib}.
+
+
+{1 Library extensions}
+The following libraries provide extensions to other OCaml libraries.
+
+{2 Library goblint.std}
+{!modules:Goblint_std}
+
+
+{1 Package utilities}
+The following libraries provide [goblint] package metadata for executables.
+
+{2 Library goblint.build-info}
+{!modules:Goblint_build_info}
+This library is virtual and has the following implementations
+- goblint.build-info.dune for native executables,
+- goblint.build-info.js for js_of_ocaml executables.
+
+{2 Library goblint.sites}
+{!modules:Goblint_sites}
+This library is virtual and has the following implementations
+- goblint.sites.dune for native executables,
+- goblint.sites.js for js_of_ocaml executables.
+
+
+{1 Independent utilities}
+The following libraries provide utilities which are completely independent of Goblint.
+
+{2 Library goblint.backtrace}
+{!modules:Goblint_backtrace}
+
+{2 Library goblint.timing}
+{!modules:Goblint_timing}
+
+
+{1 Vendored}
+The following libraries are vendored in Goblint.
+
+{2 Library goblint.zarith.mlgmpidl}
+{!modules:Z_mlgmpidl}

From 47cce4f58634308a4326683ab8031499eab2e9e0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 Oct 2023 11:41:24 +0300
Subject: [PATCH 10/10] Use goblint library documentation page in Readthedocs

---
 mkdocs.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mkdocs.yml b/mkdocs.yml
index 558c381e66..428e28078d 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -30,7 +30,7 @@ nav:
     - 👶 Your first analysis: developer-guide/firstanalysis.md
     - 🏫 Extending library: developer-guide/extending-library.md
     - 📢 Messaging: developer-guide/messaging.md
-    - 🗃️ API reference: https://goblint.github.io/analyzer/
+    - 🗃️ API reference: https://goblint.github.io/analyzer/goblint/
     - 🚨 Testing: developer-guide/testing.md
     - 🪲 Debugging: developer-guide/debugging.md
     - 📉 Profiling: developer-guide/profiling.md