diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml index b5f690a700..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/util/options.schema.json + run: ajv migrate -s src/common/util/options.schema.json - name: Validate conf - run: ajv validate -s src/util/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/util/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 c9b41df49d..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/util/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 82e92f6fe7..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/util/options.schema.json" + "url": "/src/common/util/options.schema.json" } ] } diff --git a/gobview b/gobview index b373d06174..42b07f8253 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit b373d06174667537b671f3122daf4ebd4b195aea +Subproject commit 42b07f825316052ec030370daf0d00ebe28ec092 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 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/cdomains/basetype.ml b/src/common/cdomains/basetype.ml similarity index 100% rename from src/cdomains/basetype.ml rename to src/common/cdomains/basetype.ml 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/domains/lattice.ml b/src/common/domains/lattice.ml similarity index 98% rename from src/domains/lattice.ml rename to src/common/domains/lattice.ml index 4cdaa8fb9f..79455aea62 100644 --- a/src/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/domains/myCheck.ml b/src/common/domains/myCheck.ml similarity index 100% rename from src/domains/myCheck.ml rename to src/common/domains/myCheck.ml diff --git a/src/domains/printable.ml b/src/common/domains/printable.ml similarity index 100% rename from src/domains/printable.ml rename to src/common/domains/printable.ml diff --git a/src/common/dune b/src/common/dune new file mode 100644 index 0000000000..c8f1564782 --- /dev/null +++ b/src/common/dune @@ -0,0 +1,29 @@ +(include_subdirs unqualified) + +(library + (name goblint_common) + (public_name goblint.common) + (wrapped false) ; TODO: wrap + (libraries + batteries.unthreaded + 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 util/options.schema.json))) + +(documentation) diff --git a/src/framework/analysisState.ml b/src/common/framework/analysisState.ml similarity index 100% rename from src/framework/analysisState.ml rename to src/common/framework/analysisState.ml diff --git a/src/framework/controlSpecC.ml b/src/common/framework/controlSpecC.ml similarity index 100% rename from src/framework/controlSpecC.ml rename to src/common/framework/controlSpecC.ml diff --git a/src/framework/controlSpecC.mli b/src/common/framework/controlSpecC.mli similarity index 100% rename from src/framework/controlSpecC.mli rename to src/common/framework/controlSpecC.mli diff --git a/src/framework/edge.ml b/src/common/framework/edge.ml similarity index 100% rename from src/framework/edge.ml rename to src/common/framework/edge.ml diff --git a/src/framework/myCFG.ml b/src/common/framework/myCFG.ml similarity index 100% rename from src/framework/myCFG.ml rename to src/common/framework/myCFG.ml diff --git a/src/framework/node.ml b/src/common/framework/node.ml similarity index 100% rename from src/framework/node.ml rename to src/common/framework/node.ml diff --git a/src/framework/node0.ml b/src/common/framework/node0.ml similarity index 100% rename from src/framework/node0.ml rename to src/common/framework/node0.ml diff --git a/src/incremental/updateCil0.ml b/src/common/incremental/updateCil0.ml similarity index 100% rename from src/incremental/updateCil0.ml rename to src/common/incremental/updateCil0.ml diff --git a/src/util/afterConfig.ml b/src/common/util/afterConfig.ml similarity index 100% rename from src/util/afterConfig.ml rename to src/common/util/afterConfig.ml diff --git a/src/util/cilType.ml b/src/common/util/cilType.ml similarity index 100% rename from src/util/cilType.ml rename to src/common/util/cilType.ml diff --git a/src/util/cilfacade.ml b/src/common/util/cilfacade.ml similarity index 100% rename from src/util/cilfacade.ml rename to src/common/util/cilfacade.ml diff --git a/src/util/cilfacade0.ml b/src/common/util/cilfacade0.ml similarity index 100% rename from src/util/cilfacade0.ml rename to src/common/util/cilfacade0.ml diff --git a/src/util/gobConfig.ml b/src/common/util/gobConfig.ml similarity index 100% rename from src/util/gobConfig.ml rename to src/common/util/gobConfig.ml diff --git a/src/util/gobFormat.ml b/src/common/util/gobFormat.ml similarity index 100% rename from src/util/gobFormat.ml rename to src/common/util/gobFormat.ml diff --git a/src/util/jsonSchema.ml b/src/common/util/jsonSchema.ml similarity index 100% rename from src/util/jsonSchema.ml rename to src/common/util/jsonSchema.ml diff --git a/src/util/lazyEval.ml b/src/common/util/lazyEval.ml similarity index 79% rename from src/util/lazyEval.ml rename to src/common/util/lazyEval.ml index e49a5f4693..9007cdd089 100644 --- a/src/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/util/messageCategory.ml b/src/common/util/messageCategory.ml similarity index 99% rename from src/util/messageCategory.ml rename to src/common/util/messageCategory.ml index 1bb31d6d5b..c70b8faf5f 100644 --- a/src/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" diff --git a/src/util/messageUtil.ml b/src/common/util/messageUtil.ml similarity index 100% rename from src/util/messageUtil.ml rename to src/common/util/messageUtil.ml diff --git a/src/util/messages.ml b/src/common/util/messages.ml similarity index 100% rename from src/util/messages.ml rename to src/common/util/messages.ml diff --git a/src/util/options.ml b/src/common/util/options.ml similarity index 98% rename from src/util/options.ml rename to src/common/util/options.ml index d352c86465..3046f70809 100644 --- a/src/util/options.ml +++ b/src/common/util/options.ml @@ -1,4 +1,4 @@ -(** [src/util/options.schema.json] low-level access. *) +(** [src/common/util/options.schema.json] low-level access. *) open Json_schema diff --git a/src/util/options.schema.json b/src/common/util/options.schema.json similarity index 100% rename from src/util/options.schema.json rename to src/common/util/options.schema.json diff --git a/src/util/resettableLazy.ml b/src/common/util/resettableLazy.ml similarity index 100% rename from src/util/resettableLazy.ml rename to src/common/util/resettableLazy.ml diff --git a/src/util/resettableLazy.mli b/src/common/util/resettableLazy.mli similarity index 100% rename from src/util/resettableLazy.mli rename to src/common/util/resettableLazy.mli diff --git a/src/util/richVarinfo.ml b/src/common/util/richVarinfo.ml similarity index 100% rename from src/util/richVarinfo.ml rename to src/common/util/richVarinfo.ml diff --git a/src/util/richVarinfo.mli b/src/common/util/richVarinfo.mli similarity index 100% rename from src/util/richVarinfo.mli rename to src/common/util/richVarinfo.mli diff --git a/src/util/timing.ml b/src/common/util/timing.ml similarity index 100% rename from src/util/timing.ml rename to src/common/util/timing.ml diff --git a/src/util/tracing.ml b/src/common/util/tracing.ml similarity index 98% rename from src/util/tracing.ml rename to src/common/util/tracing.ml index f9dff2c2cf..ad8892c396 100644 --- a/src/util/tracing.ml +++ b/src/common/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/util/xmlUtil.ml b/src/common/util/xmlUtil.ml similarity index 100% rename from src/util/xmlUtil.ml rename to src/common/util/xmlUtil.ml diff --git a/src/dune b/src/dune index 85944375ea..acd5348acb 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 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. @@ -56,11 +56,11 @@ (-> violationZ3.no-z3.ml) ) ) + (flags :standard -open Goblint_std) (foreign_stubs (language c) (names stubs)) (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)) ) @@ -77,51 +77,35 @@ (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 - (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)) @@ -141,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/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 6e700485dd..dadeb2cda1 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -1,3 +1,4 @@ +(** Main library. *) (** {1 Framework} *) @@ -49,7 +50,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/util/options.schema.json]. *) module GobConfig = GobConfig module AfterConfig = AfterConfig @@ -452,46 +453,20 @@ 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. *) + 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/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} 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/std/dune b/src/util/std/dune new file mode 100644 index 0000000000..c6961a1725 --- /dev/null +++ b/src/util/std/dune @@ -0,0 +1,17 @@ +(include_subdirs no) + +(library + (name goblint_std) + (public_name goblint.std) + (libraries + batteries.unthreaded + 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 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; }