Move config modules to build_info dune library

src/build-info/.gitignore

@@ -0,0 +1 @@
+config*.ml

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}\"")))
+

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

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

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

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.

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

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

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

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;

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;
   }