diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index 7472cbc820..5635ebbeea 100644
--- a/.github/workflows/coverage.yml
+++ b/.github/workflows/coverage.yml
@@ -28,7 +28,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
index 02c5f07d90..1ef104db29 100644
--- a/.github/workflows/docker.yml
+++ b/.github/workflows/docker.yml
@@ -35,7 +35,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
         uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index cd0414d6fe..e1648904c3 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -30,7 +30,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
+
+      - name: Check for undocumented modules
+        run: python scripts/goblint-lib-modules.py
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
diff --git a/.github/workflows/indentation.yml b/.github/workflows/indentation.yml
index 14db288d60..e22e674301 100644
--- a/.github/workflows/indentation.yml
+++ b/.github/workflows/indentation.yml
@@ -20,7 +20,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
 
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 358682a2f3..007ea34619 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -30,7 +30,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -101,7 +101,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -141,7 +141,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
diff --git a/.github/workflows/metadata.yml b/.github/workflows/metadata.yml
index da20c6b675..1092606bc6 100644
--- a/.github/workflows/metadata.yml
+++ b/.github/workflows/metadata.yml
@@ -19,7 +19,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Validate CITATION.cff
         uses: docker://citationcff/cffconvert:latest
@@ -36,7 +36,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
         uses: actions/setup-node@v3
diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
index b8522c03bb..b5f690a700 100644
--- a/.github/workflows/options.yml
+++ b/.github/workflows/options.yml
@@ -15,7 +15,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
         uses: actions/setup-node@v3
diff --git a/.github/workflows/semgrep.yml b/.github/workflows/semgrep.yml
index acd696e597..bd2dfd285c 100644
--- a/.github/workflows/semgrep.yml
+++ b/.github/workflows/semgrep.yml
@@ -16,10 +16,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Run semgrep
-        run: semgrep scan --sarif --output=semgrep.sarif
+        run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif
 
       - name: Upload SARIF file to GitHub Advanced Security Dashboard
         uses: github/codeql-action/upload-sarif@v2
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index 2bec6b72fb..15cd9138d8 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -45,7 +45,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
@@ -131,7 +131,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
@@ -208,7 +208,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
         uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
@@ -246,7 +246,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
diff --git a/.semgrep/tracing.yml b/.semgrep/tracing.yml
index 4892066c76..061b3efa0d 100644
--- a/.semgrep/tracing.yml
+++ b/.semgrep/tracing.yml
@@ -9,6 +9,7 @@ rules:
         - pattern: Messages.traceu
         - pattern: Messages.traceli
       - pattern-not-inside: if Messages.tracing then ...
+      - pattern-not-inside: if Messages.tracing && ... then ...
     message: trace functions should only be called if tracing is enabled at compile time
     languages: [ocaml]
     severity: WARNING
diff --git a/conf/bench-yaml-validate.json b/conf/bench-yaml-validate.json
index ca830be08a..7b18371bd1 100644
--- a/conf/bench-yaml-validate.json
+++ b/conf/bench-yaml-validate.json
@@ -52,14 +52,6 @@
       "tokens": true
     }
   },
-  "witness": {
-    "enabled": false,
-    "invariant": {
-      "loop-head": true,
-      "after-lock": true,
-      "other": false
-    }
-  },
   "sem": {
     "unknown_function": {
       "invalidate": {
diff --git a/conf/bench-yaml.json b/conf/bench-yaml.json
index a24035fc9b..fd97b2c08c 100644
--- a/conf/bench-yaml.json
+++ b/conf/bench-yaml.json
@@ -48,20 +48,6 @@
       ]
     }
   },
-  "witness": {
-    "enabled": false,
-    "yaml": {
-      "enabled": true
-    },
-    "invariant": {
-      "exact": false,
-      "exclude-vars": [
-        "tmp\\(___[0-9]+\\)?",
-        "cond",
-        "RETURN"
-      ]
-    }
-  },
   "sem": {
     "unknown_function": {
       "invalidate": {
diff --git a/conf/svcomp-yaml-validate.json b/conf/svcomp-yaml-validate.json
index 05bb1ebcc2..1934a56932 100644
--- a/conf/svcomp-yaml-validate.json
+++ b/conf/svcomp-yaml-validate.json
@@ -12,6 +12,10 @@
     "float": {
       "interval": true
     },
+    "apron": {
+      "domain": "polyhedra",
+      "strengthening": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -31,6 +35,7 @@
       "region",
       "thread",
       "threadJoins",
+      "apron",
       "unassume"
     ],
     "context": {
@@ -74,14 +79,6 @@
   "exp": {
     "region-offsets": true
   },
-  "witness": {
-    "enabled": false,
-    "invariant": {
-      "loop-head": true,
-      "after-lock": false,
-      "other": false
-    }
-  },
   "solver": "td3",
   "sem": {
     "unknown_function": {
diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json
index 6e3d0e4767..e09d1c80d7 100644
--- a/conf/svcomp-yaml.json
+++ b/conf/svcomp-yaml.json
@@ -12,6 +12,10 @@
     "float": {
       "interval": true
     },
+    "apron": {
+      "domain": "polyhedra",
+      "strengthening": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -30,7 +34,8 @@
       "symb_locks",
       "region",
       "thread",
-      "threadJoins"
+      "threadJoins",
+      "apron"
     ],
     "context": {
       "widen": false
@@ -76,6 +81,9 @@
       "enabled": true
     },
     "invariant": {
+      "loop-head": true,
+      "other": false,
+      "accessed": false,
       "exact": false,
       "exclude-vars": [
         "tmp\\(___[0-9]+\\)?",
diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
new file mode 100755
index 0000000000..342f9a76bd
--- /dev/null
+++ b/scripts/goblint-lib-modules.py
@@ -0,0 +1,59 @@
+#!/usr/bin/python3
+
+from pathlib import Path
+import re
+import sys
+
+src_root_path = Path("./src")
+
+goblint_lib_path = src_root_path / "goblint_lib.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)
+
+src_vendor_path = src_root_path / "vendor"
+exclude_module_names = set([
+    "Goblint_lib", # itself
+
+    # executables
+    "Goblint",
+    "MessagesCompare",
+    "PrivPrecCompare",
+    "ApronPrecCompare",
+    "Mainspec",
+
+    # libraries
+    "Goblint_timing",
+    "Goblint_backtrace",
+    "Goblint_sites",
+    "Goblint_build_info",
+
+    "MessageCategory", # included in Messages
+    "PreValueDomain", # included in ValueDomain
+    "SpecCore", # spec stuff
+    "SpecUtil", # spec stuff
+])
+
+src_modules = set()
+
+for ml_path in src_root_path.glob("**/*.ml"):
+    if str(ml_path).startswith(str(src_vendor_path)):
+        continue
+
+    module_name = ml_path.with_suffix("").with_suffix("").name
+    module_name = module_name[0].upper() + module_name[1:]
+    if module_name.endswith("0") or module_name.endswith("_intf") or module_name in exclude_module_names:
+        continue
+
+    src_modules.add(module_name)
+
+missing_modules = src_modules - goblint_lib_modules
+if len(missing_modules) > 0:
+    print(f"Modules missing from {goblint_lib_path}: {missing_modules}")
+    sys.exit(1)
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index fc293ae89b..0121efc04a 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -397,6 +397,8 @@ struct
           Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.zero else match eq p1 p2 with Some x when x -> ID.of_int ik BI.one | _ -> bool_top ik)
         | Ne ->
           Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.one else match eq p1 p2 with Some x when x -> ID.of_int ik BI.zero | _ -> bool_top ik)
+        | IndexPI when AD.to_string p2 = ["all_index"] ->
+          addToAddrOp p1 (ID.top_of (Cilfacade.ptrdiff_ikind ()))
         | _ -> VD.top ()
       end
     (* For other values, we just give up! *)
@@ -1053,7 +1055,6 @@ struct
            else if AD.may_be_null adr
            then M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer");
           AD.map (add_offset_varinfo (convert_offset a gs st ofs)) adr
-        | Bot -> AD.bot ()
         | _ ->
           M.debug ~category:Analyzer "Failed evaluating %a to lvalue" d_lval lval;
           AD.unknown_ptr
@@ -1262,13 +1263,8 @@ struct
         match p with
         | Address a ->
           let s = addrToLvalSet a in
-          let has_offset = function
-            | `NoOffset -> false
-            | `Field _
-            | `Index _ -> true
-          in
           (* If there's a non-heap var or an offset in the lval set, we answer with bottom *)
-          if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || has_offset o) s then
+          if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset) s then
             Queries.Result.bot q
           else (
             let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a  None in
@@ -2030,14 +2026,16 @@ struct
     let st' = invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) gs st shallow_addrs in
     invalidate ~deep:true ~ctx (Analyses.ask_of_ctx ctx) gs st' deep_addrs
 
-  let check_free_of_non_heap_mem ctx special_fn ptr =
+  let check_invalid_mem_dealloc ctx special_fn ptr =
     match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with
     | Address a ->
       let points_to_set = addrToLvalSet a in
       if Q.LS.is_top points_to_set then
-        M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potential free of non-dynamically allocated memory may occur" d_exp ptr special_fn.vname
+        M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potentially invalid memory deallocation may occur" d_exp ptr special_fn.vname
       else if (Q.LS.exists (fun (v, _) -> not (ctx.ask (Q.IsHeapVar v))) points_to_set) || (AD.mem Addr.UnknownPtr a) then
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr
+      else if Q.LS.exists (fun (_, o) -> Offset.Exp.cmp_zero_offset o <> `MustZero) points_to_set then
+        M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr
     | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname
 
   let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
@@ -2313,15 +2311,25 @@ struct
             then AD.join addr AD.null_ptr (* calloc can fail and return NULL *)
             else addr in
           let ik = Cilfacade.ptrdiff_ikind () in
-          let blobsize = ID.mul (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st size) (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st n) in
-          (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
-          set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
-                                                         (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
+          let sizeval = eval_int (Analyses.ask_of_ctx ctx) gs st size in
+          let countval = eval_int (Analyses.ask_of_ctx ctx) gs st n in
+          if ID.to_int countval = Some Z.one then (
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
+              add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false);
+              eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var))
+            ]
+          )
+          else (
+            let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
+            (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
+                                                          (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
+          )
         | _ -> st
       end
     | Realloc { ptr = p; size }, _ ->
       (* Realloc shouldn't be passed non-dynamically allocated memory *)
-      check_free_of_non_heap_mem ctx f p;
+      check_invalid_mem_dealloc ctx f p;
       begin match lv with
         | Some lv ->
           let ask = Analyses.ask_of_ctx ctx in
@@ -2355,7 +2363,7 @@ struct
       end
     | Free ptr, _ ->
       (* Free shouldn't be passed non-dynamically allocated memory *)
-      check_free_of_non_heap_mem ctx f ptr;
+      check_invalid_mem_dealloc ctx f ptr;
       st
     | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine
     | Setjmp { env }, _ ->
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 447263b3ef..5dc311a587 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -68,6 +68,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("free", special [__ "ptr" [f]] @@ fun ptr -> Free ptr);
     ("abort", special [] Abort);
     ("exit", special [drop "exit_code" []] Abort);
+    ("quick_exit", special [drop "exit_code" []] Abort);
     ("ungetc", unknown [drop "c" []; drop "stream" [r; w]]);
     ("scanf", unknown ((drop "format" [r]) :: (VarArgs (drop' [w]))));
     ("fscanf", unknown ((drop "stream" [r_deep; w_deep]) :: (drop "format" [r]) :: (VarArgs (drop' [w]))));
@@ -83,7 +84,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("getchar", unknown []);
     ("putchar", unknown [drop "ch" []]);
     ("puts", unknown [drop "s" [r]]);
-    ("rand", unknown ~attrs:[ThreadUnsafe] []);
+    ("rand", special ~attrs:[ThreadUnsafe] [] Rand);
     ("strerror", unknown ~attrs:[ThreadUnsafe] [drop "errnum" []]);
     ("strspn", unknown [drop "s" [r]; drop "accept" [r]]);
     ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]);
@@ -117,7 +118,6 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
-    ("rand", special [] Rand);
   ]
 
 (** C POSIX library functions.
@@ -889,70 +889,70 @@ struct
 
   let writesAllButFirst n f a x =
     match a with
-    | Write | Spawn -> f a x @ drop n x
+    | Write | Call | Spawn -> f a x @ drop n x
     | Read  -> f a x
     | Free  -> []
 
   let readsAllButFirst n f a x =
     match a with
-    | Write | Spawn -> f a x
+    | Write | Call | Spawn -> f a x
     | Read  -> f a x @ drop n x
     | Free  -> []
 
   let reads ns a x =
     let i, o = partition ns x in
     match a with
-    | Write | Spawn -> o
+    | Write | Call | Spawn -> o
     | Read  -> i
     | Free  -> []
 
   let writes ns a x =
     let i, o = partition ns x in
     match a with
-    | Write | Spawn -> i
+    | Write | Call | Spawn -> i
     | Read  -> o
     | Free  -> []
 
   let frees ns a x =
     let i, o = partition ns x in
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> o
     | Free  -> i
 
   let readsFrees rs fs a x =
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> keep rs x
     | Free  -> keep fs x
 
   let onlyReads ns a x =
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> keep ns x
     | Free  -> []
 
   let onlyWrites ns a x =
     match a with
-    | Write | Spawn -> keep ns x
+    | Write | Call | Spawn -> keep ns x
     | Read  -> []
     | Free  -> []
 
   let readsWrites rs ws a x =
     match a with
-    | Write | Spawn -> keep ws x
+    | Write | Call | Spawn -> keep ws x
     | Read  -> keep rs x
     | Free  -> []
 
   let readsAll a x =
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> x
     | Free  -> []
 
   let writesAll a x =
     match a with
-    | Write | Spawn -> x
+    | Write | Call | Spawn -> x
     | Read  -> []
     | Free  -> []
 end
@@ -1164,6 +1164,8 @@ let unknown_desc ~f name = (* TODO: remove name argument, unknown function shoul
     | Read when GobConfig.get_bool "sem.unknown_function.read.args" -> args
     | Read -> []
     | Free -> []
+    | Call when get_bool "sem.unknown_function.call.args" -> args
+    | Call -> []
     | Spawn when get_bool "sem.unknown_function.spawn" -> args
     | Spawn -> []
   in
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
new file mode 100644
index 0000000000..99df5695a7
--- /dev/null
+++ b/src/analyses/memLeak.ml
@@ -0,0 +1,91 @@
+(** An analysis for the detection of memory leaks ([memLeak]). *)
+
+open GoblintCil
+open Analyses
+open MessageCategory
+
+module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
+
+module Spec : Analyses.MCPSpec =
+struct
+  include Analyses.IdentitySpec
+
+  let name () = "memLeak"
+
+  module D = ToppedVarInfoSet
+  module C = Lattice.Unit
+
+  let context _ _ = ()
+
+  (* HELPER FUNCTIONS *)
+  let warn_for_multi_threaded ctx =
+    if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then
+      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program isn't running in single-threaded mode. A memory leak might occur due to multi-threading"
+
+  let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx =
+    let state = ctx.local in
+    if not @@ D.is_empty state then
+      match assert_exp_imprecise, exp with
+      | true, Some exp -> M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty state
+      | _ -> M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state
+
+  (* TRANSFER FUNCTIONS *)
+  let return ctx (exp:exp option) (f:fundec) : D.t =
+    (* Returning from "main" is one possible program exit => need to check for memory leaks *)
+    if f.svar.vname = "main" then check_for_mem_leak ctx;
+    ctx.local
+
+  let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let state = ctx.local in
+    let desc = LibraryFunctions.find f in
+    match desc.special arglist with
+    | Malloc _
+    | Calloc _
+    | Realloc _ ->
+      (* Warn about multi-threaded programs as soon as we encounter a dynamic memory allocation function *)
+      warn_for_multi_threaded ctx;
+      begin match ctx.ask Queries.HeapVar with
+        | `Lifted var -> D.add var state
+        | _ -> state
+      end
+    | Free ptr ->
+      begin match ctx.ask (Queries.MayPointTo ptr) with
+        | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) && Queries.LS.cardinal a = 1 ->
+          (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
+          let unique_pointed_to_heap_vars =
+            Queries.LS.filter (fun (v, _) -> ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v)) a
+            |> Queries.LS.elements
+            |> List.map fst
+            |> D.of_list
+          in
+          D.diff state unique_pointed_to_heap_vars
+        | _ -> state
+      end
+    | Abort ->
+      (* An "Abort" special function indicates program exit => need to check for memory leaks *)
+      check_for_mem_leak ctx;
+      state
+    | Assert { exp; _ } ->
+      let warn_for_assert_exp =
+        match ctx.ask (Queries.EvalInt exp) with
+        | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
+        | a ->
+          begin match Queries.ID.to_bool a with
+            | Some b ->
+              (* If we know for sure that the expression in "assert" is false => need to check for memory leaks *)
+              if b = false then
+                check_for_mem_leak ctx
+              else ()
+            | None -> check_for_mem_leak ctx ~assert_exp_imprecise:true ~exp:(Some exp)
+          end
+      in
+      warn_for_assert_exp;
+      state
+    | _ -> state
+
+  let startstate v = D.bot ()
+  let exitstate v = D.top ()
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index d9cdef9286..5a3aeb55ce 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -306,6 +306,7 @@ struct
             let write = match kind with
               | Write | Free -> true
               | Read -> false
+              | Call
               | Spawn -> false (* TODO: nonsense? *)
             in
             let s = GProtecting.make ~write ~recovered:is_recovered_to_st locks in
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index 3ed5a5acbe..970895e971 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -105,7 +105,7 @@ struct
       let g: V.t = Obj.obj g in
       begin match g with
         | `Left g' -> (* accesses *)
-          (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
+          (* ignore (Pretty.printf "WarnGlobal %a\n" Access.MemoRoot.pretty g'); *)
           let trie = G.access (ctx.global g) in
           (** Distribute access to contained fields. *)
           let rec distribute_inner offset (accs, children) ancestor_accs =
@@ -193,6 +193,19 @@ struct
     | _ ->
       ctx.local
 
+  let special ctx (lvalOpt: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    (* perform shallow and deep invalidate according to Library descriptors *)
+    let desc = LibraryFunctions.find f in
+    if List.mem LibraryDesc.ThreadUnsafe desc.attrs then (
+      let e = Lval (Var f, NoOffset) in
+      let conf = 110 in
+      let loc = Option.get !Node.current_node in
+      let vo = Some f in
+      let a = Obj.obj (ctx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind=Call}))) in
+      side_access ctx (conf, Call, loc, e, a) ((`Var f), `NoOffset) ;
+    );
+    ctx.local
+
   let finalize () =
     let total = !safe + !unsafe + !vulnerable in
     if total > 0 then (
diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml
index c4af80906e..2d38972d7a 100644
--- a/src/analyses/tmpSpecial.ml
+++ b/src/analyses/tmpSpecial.ml
@@ -1,5 +1,6 @@
-(* Analysis that tracks which variables hold the results of calls to math library functions.
-   For each equivalence a set of expressions is tracked, that contains the arguments of the corresponding call as well as the Lval it is assigned to, so an equivalence can be removed if one of these expressions may be changed.*)
+(** Analysis that tracks which variables hold the results of calls to math library functions ([tmpSpecial]). *)
+
+(** For each equivalence a set of expressions is tracked, that contains the arguments of the corresponding call as well as the Lval it is assigned to, so an equivalence can be removed if one of these expressions may be changed. *)
 
 module VarEq = VarEq.Spec
 
@@ -69,7 +70,7 @@ struct
         (* actually it would be necessary to check here, if one of the arguments is written by the call. However this is not the case for any of the math functions and no other functions are covered so far *)
         if List.exists (fun arg -> VarEq.may_change ask (mkAddrOf lv) arg) arglist then
           d
-        else 
+        else
           D.add (v, Offset.Exp.of_cil offs) ((ML.lift fun_args, Deps.of_list ((Lval lv)::arglist))) d
       | _ -> d
 
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 6b719c57b9..43707acd1e 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -111,7 +111,7 @@ struct
           Locator.ES.iter (fun n ->
               let fundec = Node.find_fundec n in
 
-              match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with
+              match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
               | Ok inv_exp ->
                 M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
                 NH.add invs n {exp = inv_exp; uuid}
@@ -157,12 +157,12 @@ struct
           Locator.ES.iter (fun n ->
               let fundec = Node.find_fundec n in
 
-              match InvariantParser.parse_cil inv_parser ~fundec ~loc pre_cabs with
+              match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc pre_cabs with
               | Ok pre_exp ->
                 M.debug ~category:Witness ~loc:msgLoc "located precondition to %a: %a" CilType.Fundec.pretty fundec Cil.d_exp pre_exp;
                 FH.add fun_pres fundec pre_exp;
 
-                begin match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with
+                begin match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
                   | Ok inv_exp ->
                     M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
                     if not (NH.mem pre_invs n) then
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 99307d5d37..3054f2e0da 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -291,7 +291,7 @@ struct
            | Question (b, t, f, _) -> lval_may_change_pt b bl || lval_may_change_pt t bl || lval_may_change_pt f bl
     in
     let r =
-      if Cil.isConstant b then false
+      if Cil.isConstant b || Cil.isConstant a then false
       else if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
       then ((*Messages.warn ~category:Analyzer "No PT-set: switching to types ";*) type_may_change_apt a )
       else Queries.LS.exists (lval_may_change_pt a) bls
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index d9928df597..7dffafe967 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -693,16 +693,16 @@ struct
 
   let join x y =
     (* just to optimize joining folds, which start with bot *)
-    if is_bot x then
+    if is_bot x then (* TODO: also for non-empty env *)
       y
-    else if is_bot y then
+    else if is_bot y then (* TODO: also for non-empty env *)
       x
     else (
       if M.tracing then M.traceli "apron" "join %a %a\n" pretty x pretty y;
       let j = join x y in
       if M.tracing then M.trace "apron" "j = %a\n" pretty j;
       let j =
-        if strengthening_enabled then
+        if strengthening_enabled then (* TODO: skip if same envs? *)
           strengthening j x y
         else
           j
diff --git a/src/cdomains/flagModeDomain.ml b/src/cdomains/flagModeDomain.ml
deleted file mode 100644
index 70ee6d0015..0000000000
--- a/src/cdomains/flagModeDomain.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(* TODO: unused *)
-
-module     Eq = IntDomain.MakeBooleans (struct let truename="==" let falsename="!=" end)
-module Method = IntDomain.MakeBooleans (struct let truename="guard" let falsename="assign" end)
-
-module L_names =
-struct
-  let bot_name = "unreachable"
-  let top_name = "unknown"
-end
-
-module P =
-struct
-  include Lattice.Flat (Printable.Prod3 (Method) (Eq) (IntDomain.FlatPureIntegers)) (L_names)
-  let show x = match x with
-    | `Lifted (m,b,e) -> Method.show m ^"ed "^ Eq.show b ^ " " ^ IntDomain.FlatPureIntegers.show e
-    | `Top -> top_name
-    | `Bot -> bot_name
-
-  let join x y = match x,y with
-    | `Bot , z | z , `Bot -> z
-    | `Lifted (false,_,c1),`Lifted (false,_,c2) when c1=c2 -> y
-    | `Lifted (true,false,c1),`Lifted (true,false,c2) when c1=c2 -> y
-    | `Lifted (true,true,c1),`Lifted (true, true, c2) when c1=c2 -> y
-    | `Lifted (true,true,c1),`Lifted (true, false, c2) when not(c1=c2) -> y
-    | `Lifted (true,false,c1),`Lifted (true, true, c2) when not(c1=c2) -> x
-    | _ -> `Top
-
-
-  let leq (x:t) (y:t) = match x,y with
-    | `Bot , _  -> true
-    | _ , `Top -> true
-    | _, `Bot -> false
-    | `Top ,_ -> false
-    | `Lifted (false,_,c1), `Lifted (false,_,c2) -> c1=c2
-    | _, `Lifted (false,_,_) ->  false
-    | `Lifted (false,_,_), _ ->  true
-    | `Lifted (true,true,c1),`Lifted (true, true, c2)  -> c1=c2
-    | _, `Lifted (true,true,_) -> false
-    | `Lifted (true, true, _), _ -> true
-    | `Lifted (true,false,c1),`Lifted (true,false,c2) -> c1=c2
-    (*    | _, `Lifted (true,false,c1) -> false
-          | `Lifted (true,false,_), _ -> true    *)
-    (*     | _ -> false *)
-end
-
-module Dom =
-struct
-  include MapDomain.MapTop_LiftBot (Basetype.Variables) (P)
-
-  (*   let find k x = if mem k x then find k x else P.top() *)
-end
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index b1db3796a8..5417598360 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -760,7 +760,7 @@ struct
       norm ik @@ Some (l2,u2) |> fst
   let widen ik x y =
     let r = widen ik x y in
-    if M.tracing then M.tracel "int" "interval widen %a %a -> %a\n" pretty x pretty y pretty r;
+    if M.tracing && not (equal x y) then M.tracel "int" "interval widen %a %a -> %a\n" pretty x pretty y pretty r;
     assert (leq x y); (* TODO: remove for performance reasons? *)
     r
 
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index 20c4f3bf21..a239be7c83 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -115,7 +115,7 @@ struct
     | _ -> false
 
   let is_mutex_type (t: typ): bool = match t with
-    | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t"
+    | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" || info.tname = "pthread_cond_t"
     | TInt (IInt, attr) -> hasAttribute "mutex" attr
     | _ -> false
 
diff --git a/src/domains/accessKind.ml b/src/domains/accessKind.ml
index 576581af02..b36e8f3eca 100644
--- a/src/domains/accessKind.ml
+++ b/src/domains/accessKind.ml
@@ -1,9 +1,10 @@
 (** Kinds of memory accesses. *)
 
 type t =
-  | Write  (** argument may be read or written to *)
+  | Write  (** argument may be written to *)
   | Read   (** argument may be read *)
   | Free   (** argument may be freed *)
+  | Call   (** argument may be called *)
   | Spawn  (** argument may be spawned *)
 [@@deriving eq, ord, hash]
 (** Specifies what is known about an argument. *)
@@ -12,6 +13,7 @@ let show: t -> string = function
   | Write -> "write"
   | Read -> "read"
   | Free -> "free"
+  | Call -> "call"
   | Spawn -> "spawn"
 
 include Printable.SimpleShow (
diff --git a/src/domains/partitionDomain.ml b/src/domains/partitionDomain.ml
index eab15e1b05..9675e9bfce 100644
--- a/src/domains/partitionDomain.ml
+++ b/src/domains/partitionDomain.ml
@@ -115,18 +115,23 @@ struct
       for_all (fun p -> exists (B.leq p) y) x
 
   let pretty_diff () (y, x) =
-    (* based on DisjointDomain.PairwiseSet *)
-    let x_not_leq = filter (fun p ->
-        not (exists (fun q -> B.leq p q) y)
-      ) x
-    in
-    let p_not_leq = choose x_not_leq in
-    GoblintCil.Pretty.(
-      dprintf "%a:\n" B.pretty p_not_leq
-      ++
-      fold (fun q acc ->
-          dprintf "not leq %a because %a\n" B.pretty q B.pretty_diff (p_not_leq, q) ++ acc
-        ) y nil
+    if E.is_top x then (
+      GoblintCil.Pretty.(dprintf "%a not leq bot" pretty y)
+    )
+    else (
+      (* based on DisjointDomain.PairwiseSet *)
+      let x_not_leq = filter (fun p ->
+          not (exists (fun q -> B.leq p q) y)
+        ) x
+      in
+      let p_not_leq = choose x_not_leq in
+      GoblintCil.Pretty.(
+        dprintf "%a:\n" B.pretty p_not_leq
+        ++
+        fold (fun q acc ->
+            dprintf "not leq %a because %a\n" B.pretty q B.pretty_diff (p_not_leq, q) ++ acc
+          ) y nil
+      )
     )
 
   let meet xs ys = if is_bot xs || is_bot ys then bot () else
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index dd57f40c70..df3346af93 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -75,6 +75,7 @@ end
 module GVarF (V: SpecSysVar) =
 struct
   include Printable.Either (V) (CilType.Fundec)
+  let name () = "FromSpec"
   let spec x = `Left x
   let contexts x = `Right x
 
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 5ceddf2870..5cefc1a7de 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -14,7 +14,7 @@ module type S2S = functor (X : Spec) -> Spec
 (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
 let spec_module: (module Spec) Lazy.t = lazy (
   GobConfig.building_spec := true;
-  let arg_enabled = get_bool "ana.sv-comp.enabled" || get_bool "exp.arg" in
+  let arg_enabled = (get_bool "ana.sv-comp.enabled" && get_bool "witness.enabled") || get_bool "exp.arg" in
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
diff --git a/src/goblint.ml b/src/goblint.ml
index a73d0a9fad..4ea3a3d242 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -73,7 +73,7 @@ let main () =
     exit 1
   | Sys.Break -> (* raised on Ctrl-C if `Sys.catch_break true` *)
     do_stats ();
-    (* Printexc.print_backtrace BatInnerIO.stderr *)
+    Printexc.print_backtrace stderr;
     eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!"));
     Goblint_timing.teardown_tef ();
     exit 131 (* same exit code as without `Sys.catch_break true`, otherwise 0 *)
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index d8d74acc0f..625e81f18b 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -74,6 +74,7 @@ module ApronAnalysis = ApronAnalysis
 module AffineEqualityAnalysis = AffineEqualityAnalysis
 module VarEq = VarEq
 module CondVars = CondVars
+module TmpSpecial = TmpSpecial
 
 (** {2 Heap}
 
@@ -82,6 +83,8 @@ module CondVars = CondVars
 module Region = Region
 module MallocFresh = MallocFresh
 module Malloc_null = Malloc_null
+module MemLeak = MemLeak
+module UseAfterFree = UseAfterFree
 
 (** {2 Concurrency}
 
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index f0a728f73b..29ad301292 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -334,6 +334,8 @@ module Base =
           );
           if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( (* value changed *)
             if tracing then trace "sol" "Changed\n";
+            (* if tracing && not (S.Dom.is_bot old) && HM.mem wpoint x then trace "solchange" "%a (wpx: %b): %a -> %a\n" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty old S.Dom.pretty wpd; *)
+            if tracing && not (S.Dom.is_bot old) && HM.mem wpoint x then trace "solchange" "%a (wpx: %b): %a\n" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old);
             update_var_event x old wpd;
             HM.replace rho x wpd;
             destabilize x;
@@ -429,7 +431,8 @@ module Base =
         if tracing then trace "sol2" "stable add %a\n" S.Var.pretty_trace y;
         HM.replace stable y ();
         if not (S.Dom.leq tmp old) then (
-          if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %b) from %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x;
+          if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %b) from %a: %a -> %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty old S.Dom.pretty tmp;
+          if tracing && not (S.Dom.is_bot old) then trace "solchange" "side to %a (wpx: %b) from %a: %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty_diff (tmp, old);
           let sided = match x with
             | Some x ->
               let sided = VS.mem x old_sides in
diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml
index 5452225c26..d1c8f0db3c 100644
--- a/src/util/messageCategory.ml
+++ b/src/util/messageCategory.ml
@@ -13,6 +13,7 @@ type undefined_behavior =
   | UseAfterFree
   | DoubleFree
   | InvalidMemoryDeallocation
+  | MemoryLeak
   | Uninitialized
   | DoubleLocking
   | Other
@@ -67,6 +68,7 @@ struct
     let use_after_free: category = create @@ UseAfterFree
     let double_free: category = create @@ DoubleFree
     let invalid_memory_deallocation: category = create @@ InvalidMemoryDeallocation
+    let memory_leak: category = create @@ MemoryLeak
     let uninitialized: category = create @@ Uninitialized
     let double_locking: category = create @@ DoubleLocking
     let other: category = create @@ Other
@@ -117,6 +119,7 @@ struct
       | UseAfterFree -> ["UseAfterFree"]
       | DoubleFree -> ["DoubleFree"]
       | InvalidMemoryDeallocation -> ["InvalidMemoryDeallocation"]
+      | MemoryLeak -> ["MemoryLeak"]
       | Uninitialized -> ["Uninitialized"]
       | DoubleLocking -> ["DoubleLocking"]
       | Other -> ["Other"]
@@ -228,6 +231,7 @@ let behaviorName = function
     |UseAfterFree -> "UseAfterFree"
     |DoubleFree -> "DoubleFree"
     |InvalidMemoryDeallocation -> "InvalidMemoryDeallocation"
+    |MemoryLeak -> "MemoryLeak"
     |Uninitialized -> "Uninitialized"
     |DoubleLocking -> "DoubleLocking"
     |Other -> "Other"
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index efa1dfabb8..0e89ede0b5 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1317,6 +1317,13 @@
               "type": "boolean",
               "default": true
             },
+            "call": {
+              "title": "sem.unknown_function.call",
+              "description":
+                "Unknown function call calls reachable functions",
+              "type": "boolean",
+              "default": true
+            },
             "invalidate": {
               "title": "sem.unknown_function.invalidate",
               "type": "object",
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index aff9a01383..baa465a1b3 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -297,12 +297,45 @@ struct
   module ArgTool = ArgTools.Make (R)
   module NHT = ArgTool.NHT
 
-  let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
-    let module Arg = (val ArgTool.create entrystates) in
+  module type BiArgInvariant =
+  sig
+    include ArgTools.BiArg
+    val find_invariant: Node.t -> Invariant.t
+  end
 
-    let find_invariant (n, c, i) =
-      let context = {Invariant.default_context with path = Some i} in
-      ask_local (n, c) (Invariant context)
+  let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
+    let module Arg: BiArgInvariant =
+      (val if GobConfig.get_bool "witness.enabled" then (
+           let module Arg = (val ArgTool.create entrystates) in
+           let module Arg =
+           struct
+             include Arg
+
+             let find_invariant (n, c, i) =
+               let context = {Invariant.default_context with path = Some i} in
+               ask_local (n, c) (Invariant context)
+           end
+           in
+           (module Arg: BiArgInvariant)
+         )
+         else (
+           let module Arg =
+           struct
+             module Node = ArgTool.Node
+             module Edge = MyARG.InlineEdge
+             let next _ = []
+             let prev _ = []
+             let find_invariant _ = Invariant.none
+             let main_entry =
+               let lvar = WitnessUtil.find_main_entry entrystates in
+               (fst lvar, snd lvar, -1)
+             let iter_nodes f = f main_entry
+             let query _ q = Queries.Result.top q
+           end
+           in
+           (module Arg: BiArgInvariant)
+         )
+      )
     in
 
     match Task.specification with
@@ -324,7 +357,7 @@ struct
         struct
           module Arg = Arg
           let result = Result.True
-          let invariant = find_invariant
+          let invariant = Arg.find_invariant
           let is_violation _ = false
           let is_sink _ = false
         end
@@ -332,13 +365,13 @@ struct
         (module TaskResult:WitnessTaskResult)
       ) else (
         let is_violation = function
-          | FunctionEntry f, _, _ when Svcomp.is_error_function f.svar -> true
-          | _, _, _ -> false
+          | FunctionEntry f when Svcomp.is_error_function f.svar -> true
+          | _ -> false
         in
         (* redefine is_violation to shift violations back by one, so enterFunction __VERIFIER_error is never used *)
         let is_violation n =
           Arg.next n
-          |> List.exists (fun (_, to_n) -> is_violation to_n)
+          |> List.exists (fun (_, to_n) -> is_violation (Arg.Node.cfgnode to_n))
         in
         let violations =
           (* TODO: fold_nodes?s *)
@@ -363,7 +396,7 @@ struct
           struct
             module Arg = Arg
             let result = Result.Unknown
-            let invariant = find_invariant
+            let invariant = Arg.find_invariant
             let is_violation = is_violation
             let is_sink = is_sink
           end
@@ -454,7 +487,7 @@ struct
         struct
           module Arg = Arg
           let result = Result.True
-          let invariant = find_invariant
+          let invariant = Arg.find_invariant
           let is_violation _ = false
           let is_sink _ = false
         end
@@ -480,7 +513,6 @@ struct
 
     print_task_result (module TaskResult);
 
-    (* TODO: use witness.enabled elsewhere as well *)
     if get_bool "witness.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.unknown") then (
       let witness_path = get_string "witness.path" in
       Timing.wrap "write" (write_file witness_path (module Task)) (module TaskResult)
diff --git a/tests/regression/04-mutex/90-thread-unsafe_fun_rc.c b/tests/regression/04-mutex/90-thread-unsafe_fun_rc.c
new file mode 100644
index 0000000000..8f2f01fc6d
--- /dev/null
+++ b/tests/regression/04-mutex/90-thread-unsafe_fun_rc.c
@@ -0,0 +1,22 @@
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  rand(); // RACE!
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex2);
+  rand(); // RACE!
+  pthread_mutex_unlock(&mutex2);
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/04-mutex/91-thread-unsafe_fun_nr.c b/tests/regression/04-mutex/91-thread-unsafe_fun_nr.c
new file mode 100644
index 0000000000..df02d23db9
--- /dev/null
+++ b/tests/regression/04-mutex/91-thread-unsafe_fun_nr.c
@@ -0,0 +1,21 @@
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  rand(); // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex1);
+  rand(); // NORACE
+  pthread_mutex_unlock(&mutex1);
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/34-localwn_restart/06-td-a2i.c b/tests/regression/34-localwn_restart/06-td-a2i.c
new file mode 100644
index 0000000000..e1fe6b05d0
--- /dev/null
+++ b/tests/regression/34-localwn_restart/06-td-a2i.c
@@ -0,0 +1,22 @@
+// PARAM: --enable ana.int.interval --set solver td3 --enable solvers.td3.remove-wpoint
+// Example from "The Top-Down Solver — An Exercise in A²I", Section 6.
+#include <goblint.h>
+
+int main() {
+  int i, j, x;
+  i = 0;
+  while (i < 42) {
+    j = 0;
+    while (j < 17) {
+      x = i + j;
+      j++;
+    }
+    __goblint_check(j == 17);
+    __goblint_check(i >= 0);
+    __goblint_check(i <= 41);
+    i++;
+  }
+  __goblint_check(i == 42);
+  __goblint_check(j == 17); // TODO
+  return 0;
+}
diff --git a/tests/regression/56-witness/37-hh-ex3.c b/tests/regression/56-witness/37-hh-ex3.c
index c3f26b5cf1..e59fd53108 100644
--- a/tests/regression/56-witness/37-hh-ex3.c
+++ b/tests/regression/56-witness/37-hh-ex3.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --disable solvers.td3.remove-wpoint --set ana.activated[+] unassume --set witness.yaml.unassume 37-hh-ex3.yml
+// SKIP PARAM: --set ana.activated[+] apron --enable ana.apron.strengthening --disable solvers.td3.remove-wpoint --set ana.activated[+] unassume --set witness.yaml.unassume 37-hh-ex3.yml
 #include <goblint.h>
 int main() {
   int i = 0;
diff --git a/tests/regression/56-witness/37-hh-ex3.yml b/tests/regression/56-witness/37-hh-ex3.yml
index 9a4562d6d2..d6cd5150a4 100644
--- a/tests/regression/56-witness/37-hh-ex3.yml
+++ b/tests/regression/56-witness/37-hh-ex3.yml
@@ -20,10 +20,10 @@
   location:
     file_name: 37-hh-ex3.c
     file_hash: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
-    line: 7
+    line: 6
     column: 4
     function: main
   location_invariant:
-    string: 0 <= i && i <= 3 && j == 0
+    string: 0 <= i && i <= 3
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/40-bh-ex1-poly.yml b/tests/regression/56-witness/40-bh-ex1-poly.yml
index e219e1f877..cdbd8d666b 100644
--- a/tests/regression/56-witness/40-bh-ex1-poly.yml
+++ b/tests/regression/56-witness/40-bh-ex1-poly.yml
@@ -20,10 +20,10 @@
   location:
     file_name: 40-bh-ex1-poly.c
     file_hash: 34f781dcae089ecb6b7b2811027395fcb501b8477b7e5016f7b38081724bea28
-    line: 8
+    line: 7
     column: 4
     function: main
   location_invariant:
-    string: 0 <= i && i <= 3 && j == 0
+    string: 0 <= i && i <= 3
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/63-hh-ex3-term.c b/tests/regression/56-witness/63-hh-ex3-term.c
new file mode 100644
index 0000000000..80913c3b9d
--- /dev/null
+++ b/tests/regression/56-witness/63-hh-ex3-term.c
@@ -0,0 +1,27 @@
+// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron --set ana.apron.domain polyhedra --enable ana.apron.strengthening --set ana.activated[+] unassume --set witness.yaml.unassume 63-hh-ex3-term.yml --enable ana.widen.tokens --disable witness.invariant.other --enable exp.arg
+extern void __assert_fail (const char *__assertion, const char *__file,
+      unsigned int __line, const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern void __assert_perror_fail (int __errnum, const char *__file,
+      unsigned int __line, const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern void __assert (const char *__assertion, const char *__file, int __line)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+
+extern void abort(void);
+void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "hh-ex3.c", 3, __extension__ __PRETTY_FUNCTION__); })); }
+void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
+int main() {
+  int i = 0;
+  while (i < 4) {
+    int j = 0;
+    while (j < 4) {
+      i++;
+      j++;
+      __VERIFIER_assert(0 <= j);
+    }
+    __VERIFIER_assert(0 <= j);
+    i = i - j + 1;
+  }
+  return 0;
+}
diff --git a/tests/regression/56-witness/63-hh-ex3-term.yml b/tests/regression/56-witness/63-hh-ex3-term.yml
new file mode 100644
index 0000000000..e635e24014
--- /dev/null
+++ b/tests/regression/56-witness/63-hh-ex3-term.yml
@@ -0,0 +1,25 @@
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: d834761a-d0d7-4fea-bf42-2ff2b9a19143
+    creation_time: 2022-10-12T10:59:25Z
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - /home/vagrant/eval-prec/prec/hh-ex3.i
+      input_file_hashes:
+        /home/vagrant/eval-prec/prec/hh-ex3.i: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
+      data_model: LP64
+      language: C
+  location:
+    file_name: 63-hh-ex3-term.c
+    file_hash: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
+    line: 17
+    column: 4
+    function: main
+  location_invariant:
+    string: 0 <= i && i <= 3
+    type: assertion
+    format: C
diff --git a/tests/regression/73-strings/04-smtprc_strlen_fp.c b/tests/regression/73-strings/04-smtprc_strlen_fp.c
new file mode 100644
index 0000000000..a046eac238
--- /dev/null
+++ b/tests/regression/73-strings/04-smtprc_strlen_fp.c
@@ -0,0 +1,21 @@
+// FIXPOINT extracted from smtprc_comb
+#include <unistd.h> // for optarg
+
+typedef unsigned int size_t; // size_t from 32bit cilly
+extern size_t strlen(char const   *__s );
+
+void *s_malloc(unsigned long size)
+{
+  void *mymem;
+  mymem = malloc((unsigned int) size);
+  return mymem;
+}
+
+int main() {
+  char const *p;
+  size_t s;
+  p = optarg;
+  s = strlen(optarg);
+  s_malloc((unsigned long) ((s + 1U) * sizeof(char)));
+  return 0;
+}
diff --git a/tests/regression/75-invalid_dealloc/05-free-at-offset.c b/tests/regression/75-invalid_dealloc/05-free-at-offset.c
new file mode 100644
index 0000000000..c9ec66c769
--- /dev/null
+++ b/tests/regression/75-invalid_dealloc/05-free-at-offset.c
@@ -0,0 +1,9 @@
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    char *ptr = malloc(42 * sizeof(char));
+    ptr = ptr + 7;
+    free(ptr); //WARN
+
+    return 0;
+}
diff --git a/tests/regression/75-invalid_dealloc/06-realloc-at-offset.c b/tests/regression/75-invalid_dealloc/06-realloc-at-offset.c
new file mode 100644
index 0000000000..64a42654e1
--- /dev/null
+++ b/tests/regression/75-invalid_dealloc/06-realloc-at-offset.c
@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+#define MAX_SIZE 5000
+
+int main(int argc, char const *argv[]) {
+    char *ptr = malloc(42 * sizeof(char));
+    ptr = ptr + 7;
+    realloc(ptr, MAX_SIZE); //WARN
+
+    return 0;
+}
diff --git a/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c b/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c
new file mode 100644
index 0000000000..f64d66d8fc
--- /dev/null
+++ b/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c
@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+typedef struct custom_t {
+    char *x;
+    int y;
+} custom_t;
+
+int main(int argc, char const *argv[]) {
+    custom_t *struct_ptr = malloc(sizeof(custom_t));
+    struct_ptr->x = malloc(10 * sizeof(char));
+    free(&struct_ptr->x); //NOWARN
+    free(&struct_ptr->y); //WARN
+    free(struct_ptr); //NOWARN
+    return 0;
+}
diff --git a/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c b/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c
new file mode 100644
index 0000000000..fddb8a7694
--- /dev/null
+++ b/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c
@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+typedef struct custom_t {
+    char *x;
+    int y;
+} custom_t;
+
+int main(int argc, char const *argv[]) {
+    custom_t *struct_ptr = malloc(sizeof(custom_t));
+    struct_ptr->x = malloc(10 * sizeof(char));
+    realloc(&struct_ptr->x, 50); //NOWARN
+    realloc(&struct_ptr->y, 50); //WARN
+    realloc(struct_ptr, 2 * sizeof(custom_t)); //NOWARN
+    return 0;
+}
diff --git a/tests/regression/76-memleak/01-simple-no-mem-leak.c b/tests/regression/76-memleak/01-simple-no-mem-leak.c
new file mode 100644
index 0000000000..da6cdacddb
--- /dev/null
+++ b/tests/regression/76-memleak/01-simple-no-mem-leak.c
@@ -0,0 +1,9 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    free(p);
+
+    return 0; //NOWARN
+}
diff --git a/tests/regression/76-memleak/02-simple-mem-leak.c b/tests/regression/76-memleak/02-simple-mem-leak.c
new file mode 100644
index 0000000000..3673addfdf
--- /dev/null
+++ b/tests/regression/76-memleak/02-simple-mem-leak.c
@@ -0,0 +1,8 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    // No free => memory is leaked
+    return 0; //WARN
+}
diff --git a/tests/regression/76-memleak/03-simple-exit-mem-leak.c b/tests/regression/76-memleak/03-simple-exit-mem-leak.c
new file mode 100644
index 0000000000..451dafa471
--- /dev/null
+++ b/tests/regression/76-memleak/03-simple-exit-mem-leak.c
@@ -0,0 +1,7 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    exit(0); //WARN
+}
diff --git a/tests/regression/76-memleak/04-simple-abort-mem-leak.c b/tests/regression/76-memleak/04-simple-abort-mem-leak.c
new file mode 100644
index 0000000000..d4001410de
--- /dev/null
+++ b/tests/regression/76-memleak/04-simple-abort-mem-leak.c
@@ -0,0 +1,7 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    abort(); //WARN
+}
diff --git a/tests/regression/76-memleak/05-simple-assert-no-mem-leak.c b/tests/regression/76-memleak/05-simple-assert-no-mem-leak.c
new file mode 100644
index 0000000000..8dbf20c433
--- /dev/null
+++ b/tests/regression/76-memleak/05-simple-assert-no-mem-leak.c
@@ -0,0 +1,10 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+#include <assert.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    assert(1);
+    free(p);
+    return 0; //NOWARN
+}
diff --git a/tests/regression/76-memleak/06-simple-assert-mem-leak.c b/tests/regression/76-memleak/06-simple-assert-mem-leak.c
new file mode 100644
index 0000000000..b2f78388dc
--- /dev/null
+++ b/tests/regression/76-memleak/06-simple-assert-mem-leak.c
@@ -0,0 +1,8 @@
+//PARAM: --set warn.assert false --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+#include <assert.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    assert(0); //WARN
+}
diff --git a/tests/regression/76-memleak/07-simple-quick-exit-mem-leak.c b/tests/regression/76-memleak/07-simple-quick-exit-mem-leak.c
new file mode 100644
index 0000000000..eba23385b8
--- /dev/null
+++ b/tests/regression/76-memleak/07-simple-quick-exit-mem-leak.c
@@ -0,0 +1,7 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    quick_exit(0); //WARN
+}