Merge branch 'master' into issue_843

goblint · Nov 1, 2023 · 809e5a0 · 809e5a0
2 parents b718e46 + 6131273
commit 809e5a0
Show file tree

Hide file tree

Showing 240 changed files with 3,526 additions and 765 deletions.
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
@@ -153,7 +153,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 

diff --git a/.github/workflows/metadata.yml b/.github/workflows/metadata.yml
@@ -39,7 +39,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 

diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
@@ -18,18 +18,18 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 
       - name: Install ajv-cli
         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
@@ -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/conf/svcomp.json b/conf/svcomp.json
@@ -70,7 +70,8 @@
         "congruence",
         "octagon",
         "wideningThresholds",
-        "loopUnrollHeuristic"
+        "loopUnrollHeuristic",
+        "memsafetySpecification"
       ]
     }
   },

diff --git 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/goblint.opam b/goblint.opam
@@ -74,12 +74,11 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-# pin-depends: [
-  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
+pin-depends: [
+  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
-  # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-# ]
+  [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -128,3 +128,14 @@ conflicts: [
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
+# TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
+pin-depends: [
+  [
+    "goblint-cil.2.0.2"
+    "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331"
+  ]
+  [
+    "ppx_deriving.5.2.1"
+    "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
+  ]
+]
diff --git a/goblint.opam.template b/goblint.opam.template
@@ -1,12 +1,11 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-# pin-depends: [
-  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
+pin-depends: [
+  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
-  # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-# ]
+  [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/gobview b/gobview
diff --git 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/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
@@ -6,16 +6,20 @@
 
 src_root_path = Path("./src")
 
-goblint_lib_path = src_root_path / "goblint_lib.ml"
+goblint_lib_paths = [
+    src_root_path / "goblint_lib.ml",
+    src_root_path / "util" / "std" / "goblint_std.ml",
+]
 goblint_lib_modules = set()
 
-with goblint_lib_path.open() as goblint_lib_file:
-    for line in goblint_lib_file:
-        line = line.strip()
-        m = re.match(r"module (.*) = .*", line)
-        if m is not None:
-            module_name = m.group(1)
-            goblint_lib_modules.add(module_name)
+for goblint_lib_path in goblint_lib_paths:
+    with goblint_lib_path.open() as goblint_lib_file:
+        for line in goblint_lib_file:
+            line = line.strip()
+            m = re.match(r"module (.*) = .*", line)
+            if m is not None:
+                module_name = m.group(1)
+                goblint_lib_modules.add(module_name)
 
 src_vendor_path = src_root_path / "vendor"
 exclude_module_names = set([
@@ -29,15 +33,21 @@
     "Mainspec",
 
     # libraries
+    "Goblint_std",
     "Goblint_timing",
     "Goblint_backtrace",
     "Goblint_sites",
     "Goblint_build_info",
+    "Dune_build_info",
 
     "MessageCategory", # included in Messages
     "PreValueDomain", # included in ValueDomain
     "SpecCore", # spec stuff
     "SpecUtil", # spec stuff
+
+    "ConfigVersion",
+    "ConfigProfile",
+    "ConfigOcaml",
 ])
 
 src_modules = set()