Merge branch 'master' of github.com:goblint/analyzer into parallelism_backwards_compat_1

Author: arkocal

.gitattributes

@@ -0,0 +1,13 @@
+# GitHub repository language overrides
+# https://github.com/github-linguist/linguist/blob/main/docs/overrides.md
+
+# currently only dune-project is classified: https://github.com/github-linguist/linguist/pull/7126
+dune linguist-language=dune
+dune.inc linguist-language=dune
+
+# avoid misclassification as Standard ML
+*.ml linguist-language=ocaml
+*.mli linguist-language=ocaml
+
+# cram tests are classified as Raku/Terra/Turing, cram isn't separate language so consider them also dune
+*.t linguist-language=dune

goblint.opam

@@ -99,8 +99,8 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f" ]
+  # published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility
+  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#8385ab315bc7461f6801af57673c64731bfa036a" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
   [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release

goblint.opam.locked

@@ -66,7 +66,7 @@ depends: [
   "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.5"}
+  "goblint-cil" {= "2.0.6"}
   "hex" {= "1.5.0"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "1.0.1"}
@@ -141,8 +141,8 @@ post-messages: [
 ]
 pin-depends: [
   [
-    "goblint-cil.2.0.5"
-    "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f"
+    "goblint-cil.2.0.6"
+    "git+https://github.com/goblint/cil.git#8385ab315bc7461f6801af57673c64731bfa036a"
   ]
   [
     "camlidl.1.12"

goblint.opam.template

@@ -2,8 +2,8 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f" ]
+  # published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility
+  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#8385ab315bc7461f6801af57673c64731bfa036a" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
   [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release

gobview

@@ -740,7 +740,12 @@ struct
         in
         ({ f } : Queries.ask) in
       let rel = RD.assert_inv dummyask rel e false (no_overflow ask e_orig) in (* assume *)
-      let rel = RD.keep_vars rel (List.map RV.local vars) in (* restrict *)
+      let rel =
+        if GobConfig.get_bool "ana.apron.strengthening" then
+          RD.keep_vars rel (List.map RV.local vars) (* restrict *)
+        else
+          rel (* naive unassume: will be homogeneous join below *)
+      in
 
       (* TODO: parallel write_global? *)
       let st =