Merge branch 'master' into fix-locations-pred

.github/workflows/docs.yml

@@ -41,7 +41,7 @@ jobs:
 
       - name: Setup Pages
         id: pages
-        uses: actions/configure-pages@v4
+        uses: actions/configure-pages@v5
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-doc

.github/workflows/unlocked.yml

@@ -134,7 +134,7 @@ jobs:
       - name: Downgrade dependencies
         # must specify ocaml-base-compiler again to prevent it from being downgraded
         # prevent num downgrade to avoid dune/jbuilder error: https://github.com/ocaml/dune/issues/5280
-        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda num.1.4)
+        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda num.1.5)
 
       - name: Build
         run: ./make.sh nat

README.md

@@ -8,6 +8,7 @@
 [![Coverage Status](https://coveralls.io/repos/github/goblint/analyzer/badge.svg?branch=master)](https://coveralls.io/github/goblint/analyzer?branch=master)
 [![docker workflow status](https://github.com/goblint/analyzer/actions/workflows/docker.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/docker.yml)
 [![Documentation Status](https://readthedocs.org/projects/goblint/badge/?version=latest)](https://goblint.readthedocs.io/en/latest/?badge=latest)
+[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://goblint.zulipchat.com)
 
 Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/en/latest/) or [GitHub](./docs/).
 
@@ -56,3 +57,9 @@ docker run -it --rm -v $(pwd):/data goblint /data/tests/regression/04-mutex/01-s
 If pulled from GitHub Container Registry, use the container name `ghcr.io/goblint/analyzer:latest` (or `:nightly`) instead.
 
 For further information, see [documentation](https://goblint.readthedocs.io/en/latest/user-guide/running/).
+
+## Acknowledgements
+
+Work on Goblint was supported in part by Deutsche Forschungsgemeinschaft (DFG) (47140942/1480 [PUMA](https://gepris.dfg.de/gepris/projekt/4714094), 378803395/2428 [ConVeY](http://convey.in.tum.de)), ARTEMIS Joint Undertaking (269335 [MBAT](http://www.mbat-artemis.eu/home/)), ITEA3 project 14014 [ASSUME](http://assume-project.eu/), the Shota Rustaveli National Science Foundation of Georgia [FR-21-7973](https://viam.science.tsu.ge/new/index.php?lang=eng&page=projects&subpage=111), the Estonian Research Council ([IUT2-1](https://www.etis.ee/Portal/Projects/Display/561b7b1d-d1dd-43a2-90e5-0661de823823?lang=ENG), [PSG61](https://www.etis.ee/Portal/Projects/Display/743243bb-15c2-47b3-9c10-e7d86a9a276d?lang=ENG)), and the Estonian Centre of Excellence in IT (EXCITE), funded by the European Regional Development Fund.
+
+We also thank [Zulip](https://zulip.com) for providing free Zulip Cloud Standard hosting for the Goblint project. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized.

conf/svcomp2var.json

@@ -0,0 +1,146 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins" ,
+      "lin2vareq"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc",
+        "ldv_kzalloc"
+      ]
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true,
+      "exclude-vars": [
+        "tmp\\(___[0-9]+\\)?",
+        "cond",
+        "RETURN",
+        "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+        ".*____CPAchecker_TMP_[0-9]+",
+        "__VERIFIER_assert__cond",
+        "__ksymtab_.*",
+        "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+      ]
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

docs/developer-guide/debugging.md

@@ -13,25 +13,25 @@ Goblint extensively uses [CIL's `Pretty`](https://people.eecs.berkeley.edu/~necu
 * Logging CIL values (e.g. an expression `exp`) using the corresponding pretty-printer `d_exp` from `Cil` module:
 
 ```ocaml
-Logs.debug "A CIL exp: %a\n" d_exp exp;
+Logs.debug "A CIL exp: %a" d_exp exp;
 ```
 
 * Logging Goblint's `Printable` values (e.g. a domain `D` element `d`) using the corresponding pretty-printer `D.pretty`:
 
 ```ocaml
-Logs.debug "A domain element: %a\n" D.pretty d;
+Logs.debug "A domain element: %a" D.pretty d;
 ```
 
 * Logging primitives (e.g. OCaml ints, strings, etc) using the standard [OCaml `Printf`](https://ocaml.org/api/Printf.html) specifiers:
 
 ```ocaml
-Logs.debug "An int and a string: %d %s\n" 42 "magic";
+Logs.debug "An int and a string: %d %s" 42 "magic";
 ```
 
 * Logging lists of pretty-printables (e.g. expressions list `exps`) using `d_list`:
 
 ```ocaml
-Logs.debug "Some expressions: %a\n" (d_list ", " d_exp) exps;
+Logs.debug "Some expressions: %a" (d_list ", " d_exp) exps;
 ```
 
 
@@ -42,7 +42,7 @@ Recompile with tracing enabled: `./scripts/trace_on.sh`.
 
 Instead of logging use a tracing function from the `Messages` module, which is often aliased to just `M` (and pick a relevant name instead of `mything`):
 ```ocaml
-if M.tracing then M.trace "mything" "A domain element: %a\n" D.pretty d;
+if M.tracing then M.trace "mything" "A domain element: %a" D.pretty d;
 ```
 
 Then run Goblint with the additional argument `--trace mything`.

dune-project

@@ -26,11 +26,11 @@
     (ocaml (>= 4.10))
     (goblint-cil (>= 2.0.3)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
     (batteries (>= 3.5.1))
-    (zarith (>= 1.8))
+    (zarith (>= 1.10))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))
     ppx_deriving
-    ppx_deriving_hash
+    (ppx_deriving_hash (>= 0.1.2))
     (ppx_deriving_yojson (>= 3.7.0))
     (ounit2 :with-test)
     (qcheck-ounit :with-test)

goblint.opam

@@ -24,11 +24,11 @@ depends: [
   "ocaml" {>= "4.10"}
   "goblint-cil" {>= "2.0.3"}
   "batteries" {>= "3.5.1"}
-  "zarith" {>= "1.8"}
+  "zarith" {>= "1.10"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}
   "ppx_deriving"
-  "ppx_deriving_hash"
+  "ppx_deriving_hash" {>= "0.1.2"}
   "ppx_deriving_yojson" {>= "3.7.0"}
   "ounit2" {with-test}
   "qcheck-ounit" {with-test}

goblint.opam.locked

@@ -82,7 +82,7 @@ depends: [
   "pp" {= "1.1.2"}
   "ppx_derivers" {= "1.2.1"}
   "ppx_deriving" {= "5.2.1"}
-  "ppx_deriving_hash" {= "0.1.1"}
+  "ppx_deriving_hash" {= "0.1.2"}
   "ppx_deriving_yojson" {= "3.7.0"}
   "ppxlib" {= "0.28.0"}
   "qcheck-core" {= "0.20"}

make.sh

@@ -80,10 +80,11 @@ rule() {
       opam_setup
     ;; dev)
       eval $(opam env)
+      echo "Installing opam packages for test and doc..."
+      opam install -y . --deps-only --locked --with-test --with-doc
       echo "Installing opam packages for development..."
-      opam install -y utop ocaml-lsp-server ocp-indent ocamlformat ounit2
+      opam install -y ocaml-lsp-server ocp-indent
       # ocaml-lsp-server is needed for https://github.com/ocamllabs/vscode-ocaml-platform
-      echo "Be sure to adjust your vim/emacs config!"
       echo "Installing Pre-commit hook..."
       cd .git/hooks; ln -sf ../../scripts/hooks/pre-commit; cd -
       # Use `git commit -n` to temporarily bypass the hook if necessary.
@@ -138,6 +139,9 @@ rule() {
       eval $(opam env)
       dune runtest
 
+    ;; sanitytest)
+      ./scripts/update_suite.rb
+
     ;; *)
       echo "Unknown action '$1'. Try clean, native, byte, profile or doc.";;
   esac;

scripts/goblint-lib-modules.py

@@ -48,6 +48,7 @@
     "ConfigVersion",
     "ConfigProfile",
     "ConfigOcaml",
+    "ConfigDatetime",
 ])
 
 src_modules = set()

scripts/update_suite.rb

@@ -36,7 +36,11 @@ def itemize(n=2); self.map {|x| "- #{x}".indent(n)}.join() end
 end
 # clear the current line
 def clearline
-  print "\r\e[K"
+  if $stdout.isatty
+    print "\r\e[K"
+  else
+    print "\n"
+  end
 end
 
 $goblint = File.join(Dir.getwd,"goblint")

src/analyses/abortUnless.ml

@@ -11,7 +11,7 @@ struct
 
   let name () = "abortUnless"
   module D = BoolDomain.MustBool
-  module C = Lattice.Unit
+  module C = Printable.Unit
 
   let context _ _ = ()
 

src/analyses/accessAnalysis.ml

@@ -14,7 +14,7 @@ struct
   let name () = "access"
 
   module D = Lattice.Unit
-  module C = Lattice.Unit
+  module C = Printable.Unit
 
   module V =
   struct
@@ -32,7 +32,7 @@ struct
     emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
 
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) =
-    if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach;
+    if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach;
     let reach_or_mpt: _ Queries.t = if reach then ReachableFrom e else MayPointTo e in
     let ad = ctx.ask reach_or_mpt in
     ctx.emit (Access {exp=e; ad; kind; reach})
@@ -42,15 +42,15 @@ struct
       + [deref=true], [reach=false] - Access [exp] by dereferencing once (may-point-to), used for lval writes and shallow special accesses.
       + [deref=true], [reach=true] - Access [exp] by dereferencing transitively (reachable), used for deep special accesses. *)
   let access_one_top ?(force=false) ?(deref=false) ctx (kind: AccessKind.t) reach exp =
-    if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)\n" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
+    if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
     if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) then (
       if deref && Cil.isPointerType (Cilfacade.typeOf exp) then (* avoid dereferencing integers to unknown pointers, which cause many spurious type-based accesses *)
         do_access ctx kind reach exp;
-      if M.tracing then M.tracei "access" "distribute_access_exp\n";
+      if M.tracing then M.tracei "access" "distribute_access_exp";
       Access.distribute_access_exp (do_access ctx Read false) exp;
-      if M.tracing then M.traceu "access" "distribute_access_exp\n";
+      if M.tracing then M.traceu "access" "distribute_access_exp";
     );
-    if M.tracing then M.traceu "access" "access_one_top\n"
+    if M.tracing then M.traceu "access" "access_one_top"
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()

src/analyses/activeLongjmp.ml

@@ -5,15 +5,12 @@ open Analyses
 
 module Spec =
 struct
-  include Analyses.IdentitySpec
+  include Analyses.IdentityUnitContextsSpec
 
   let name () = "activeLongjmp"
 
   (* The first component are the longjmp targets, the second are the longjmp callers *)
   module D = JmpBufDomain.ActiveLongjmps
-  module C = Lattice.Unit
-
-  let context _ _ = ()
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     let desc = LibraryFunctions.find f in