From cd1af7ae737a97047a72e3d59bee569e006f0657 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 12:57:52 +0300
Subject: [PATCH 01/24] Add yaml witness parsing prototype

---
 src/framework/control.ml     |  5 ++++
 src/util/options.schema.json |  6 +++++
 src/witness/yamlWitness.ml   | 50 ++++++++++++++++++++++++++++++++++++
 3 files changed, 61 insertions(+)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index 7393cd1b4b..295a212e81 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -683,6 +683,11 @@ struct
       YWitness.write lh gh
     );
 
+    if get_string "witness.yaml.validate" <> "" then (
+      let module YWitness = YamlWitness.Validator (Spec) (EQSys) (LHT) (GHT) in
+      YWitness.validate lh gh
+    );
+
     let marshal = Spec.finalize () in
     (* copied from solve_and_postprocess *)
     let gobview = get_bool "gobview" in
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index e52a9b0bc5..c4c7ce8490 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1805,6 +1805,12 @@
               "description": "YAML witness output path",
               "type": "string",
               "default": "witness.yml"
+            },
+            "validate": {
+              "title": "witness.yaml.validate",
+              "description": "YAML witness input path",
+              "type": "string",
+              "default": ""
             }
           },
           "additionalProperties": false
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index ad73090e05..c4ea4b97a8 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -112,3 +112,53 @@ struct
     let yaml = `A yaml_entries in
     Yaml_unix.to_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.path")) yaml
 end
+
+
+module Validator
+    (Spec : Spec)
+    (EQSys : GlobConstrSys with module LVar = VarF (Spec.C)
+                        and module GVar = GVarF (Spec.V)
+                        and module D = Spec.D
+                        and module G = Spec.G)
+    (LHT : BatHashtbl.S with type key = EQSys.LVar.t)
+    (GHT : BatHashtbl.S with type key = EQSys.GVar.t) =
+struct
+
+  module NH = BatHashtbl.Make (Node)
+
+  (* copied from Constraints.CompareNode *)
+  let join_contexts (lh: Spec.D.t LHT.t): Spec.D.t NH.t =
+    let nh = NH.create 113 in
+    LHT.iter (fun (n, _) d ->
+        let d' = try Spec.D.join (NH.find nh n) d with Not_found -> d in
+        NH.replace nh n d'
+      ) lh;
+    nh
+
+  let validate lh gh =
+    let nh = join_contexts lh in
+
+    let yaml = Yaml_unix.of_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.validate")) in
+    let yaml_entries = match yaml with
+      | `A yaml_entries -> yaml_entries
+      | _ -> failwith "invalid YAML"
+    in
+    List.iter (fun yaml_entry ->
+        let yaml_location = Yaml.Util.(yaml_entry |> find_exn "location" |> Option.get) in
+        let file = Yaml.Util.(yaml_location |> find_exn "file_name" |> Option.get |> to_string_exn) in
+        let line = Yaml.Util.(yaml_location |> find_exn "line" |> Option.get |> to_float_exn |> int_of_float) in
+        let column = Yaml.Util.(yaml_location |> find_exn "column" |> Option.get |> to_float_exn |> int_of_float) + 1 in
+        let inv = Yaml.Util.(yaml_entry |> find_exn "loop_invariant" |> Option.get |> find_exn "string" |> Option.get |> to_string_exn) in
+        let loc: Cil.location = {
+          file;
+          line;
+          column;
+          byte = -1;
+          endLine = -1;
+          endColumn = -1;
+          endByte = -1;
+        }
+        in
+        ignore (Pretty.printf "%a: %s\n" CilType.Location.pretty loc inv)
+      ) yaml_entries
+end

From 7a85a96a8ea0b3dc243711145eb90e136d4bf096 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 14:29:48 +0300
Subject: [PATCH 02/24] Add yaml witness assert evaluation

---
 src/framework/control.ml   |  2 +-
 src/witness/yamlWitness.ml | 50 ++++++++++++++++++++++++++++++++++++--
 2 files changed, 49 insertions(+), 3 deletions(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index 295a212e81..5f28a427f0 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -685,7 +685,7 @@ struct
 
     if get_string "witness.yaml.validate" <> "" then (
       let module YWitness = YamlWitness.Validator (Spec) (EQSys) (LHT) (GHT) in
-      YWitness.validate lh gh
+      YWitness.validate lh gh file
     );
 
     let marshal = Spec.finalize () in
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index c4ea4b97a8..436186f88e 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -135,9 +135,36 @@ struct
       ) lh;
     nh
 
-  let validate lh gh =
+  let validate lh gh (file: Cil.file) =
     let nh = join_contexts lh in
 
+    let global_variables =
+      file.globals
+      |> List.filter_map (function Cil.GVar (v, _, _) -> Some (v.vname, Cil.Fv v) | _ -> None)
+    in
+
+    let ask_local n local =
+      (* build a ctx for using the query system *)
+      let rec ctx =
+        { ask    = (fun (type a) (q: a Queries.t) -> Spec.query ctx q)
+        ; emit   = (fun _ -> failwith "Cannot \"emit\" in witness context.")
+        ; node   = n
+        ; prev_node = MyCFG.dummy_node
+        ; control_context = Obj.repr (fun () -> failwith "TODO")
+        ; context = (fun () -> failwith "TODO")
+        ; edge    = MyCFG.Skip
+        ; local  = local
+        ; global = GHT.find gh
+        ; presub = (fun _ -> raise Not_found)
+        ; postsub= (fun _ -> raise Not_found)
+        ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in witness context.")
+        ; split  = (fun d es   -> failwith "Cannot \"split\" in witness context.")
+        ; sideg  = (fun v g    -> failwith "Cannot \"sideg\" in witness context.")
+        }
+      in
+      Spec.query ctx
+    in
+
     let yaml = Yaml_unix.of_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.validate")) in
     let yaml_entries = match yaml with
       | `A yaml_entries -> yaml_entries
@@ -159,6 +186,25 @@ struct
           endByte = -1;
         }
         in
-        ignore (Pretty.printf "%a: %s\n" CilType.Location.pretty loc inv)
+        ignore (Pretty.printf "%a: %s\n" CilType.Location.pretty loc inv);
+
+        (* TODO: better node finding *)
+        NH.iter (fun n d ->
+            let nloc = Node.location n in
+            if loc.file = nloc.file && loc.line = nloc.line && loc.column = nloc.column then (
+              ignore (Pretty.printf "  %a\n" Node.pretty n);
+
+              let fd = Node.find_fundec n in
+              let local_variables = fd.slocals |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v) in
+
+              match Formatcil.cExp inv (local_variables @ global_variables) with
+              | inv_exp ->
+                ignore (Pretty.printf "  parsed %a\n" Cil.d_plainexp inv_exp);
+                let r = ask_local n d (Queries.EvalInt inv_exp) in
+                ignore (Pretty.printf "  -> %a\n" Queries.ID.pretty r)
+              | exception _ ->
+                ignore (Pretty.printf "  couldn't parse %s\n" inv)
+            )
+          ) nh
       ) yaml_entries
 end

From d0d75585e85f693555965ea966ad6a6e289b65d2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 14:34:20 +0300
Subject: [PATCH 03/24] Split conjunctions in yaml witness output to work
 around misparsing

https://github.com/goblint/cil/issues/94.
---
 src/witness/yamlWitness.ml | 53 ++++++++++++++++++++------------------
 1 file changed, 28 insertions(+), 25 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 436186f88e..36011c2f3b 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -76,31 +76,34 @@ struct
             | Some inv ->
               let inv = InvariantCil.exp_replace_original_name inv in
               let loc = Node.location n in
-              let uuid = Uuidm.v4_gen uuid_random_state () in
-              let entry = `O [
-                  ("entry_type", `String "loop_invariant");
-                  ("metadata", `O [
-                      ("format_version", `String "0.1");
-                      ("uuid", `String (Uuidm.to_string uuid));
-                      ("creation_time", yaml_creation_time);
-                      ("producer", yaml_producer);
-                      ("task", yaml_task);
-                    ]);
-                  ("location", `O [
-                      ("file_name", `String loc.file);
-                      ("file_hash", `String (sha256_file loc.file));
-                      ("line", `Float (float_of_int loc.line));
-                      ("column", `Float (float_of_int (loc.column - 1)));
-                      ("function", `String (Node.find_fundec n).svar.vname);
-                    ]);
-                  ("loop_invariant", `O [
-                      ("string", `String (CilType.Exp.show inv));
-                      ("type", `String "assertion");
-                      ("format", `String "C");
-                    ]);
-                ]
-              in
-              entry :: acc
+              let invs = EvalAssert.EvalAssert.pullOutCommonConjuncts inv in
+              EvalAssert.ES.fold (fun inv acc ->
+                  let uuid = Uuidm.v4_gen uuid_random_state () in
+                  let entry = `O [
+                      ("entry_type", `String "loop_invariant");
+                      ("metadata", `O [
+                          ("format_version", `String "0.1");
+                          ("uuid", `String (Uuidm.to_string uuid));
+                          ("creation_time", yaml_creation_time);
+                          ("producer", yaml_producer);
+                          ("task", yaml_task);
+                        ]);
+                      ("location", `O [
+                          ("file_name", `String loc.file);
+                          ("file_hash", `String (sha256_file loc.file));
+                          ("line", `Float (float_of_int loc.line));
+                          ("column", `Float (float_of_int (loc.column - 1)));
+                          ("function", `String (Node.find_fundec n).svar.vname);
+                        ]);
+                      ("loop_invariant", `O [
+                          ("string", `String (CilType.Exp.show inv));
+                          ("type", `String "assertion");
+                          ("format", `String "C");
+                        ]);
+                    ]
+                  in
+                  entry :: acc
+                ) invs acc
             | None ->
               acc
           end

From f15bd32ca08e7a511b1d9da8a16467eac46ea7fa Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 14:34:40 +0300
Subject: [PATCH 04/24] Fix yaml witness validate not handling formals

---
 src/witness/yamlWitness.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 36011c2f3b..b8869a6172 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -198,7 +198,7 @@ struct
               ignore (Pretty.printf "  %a\n" Node.pretty n);
 
               let fd = Node.find_fundec n in
-              let local_variables = fd.slocals |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v) in
+              let local_variables = (fd.slocals @ fd.sformals) |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v) in
 
               match Formatcil.cExp inv (local_variables @ global_variables) with
               | inv_exp ->

From b6b8449d079d758f51c8a45b26fba74ab8c1b6ad Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 17:09:18 +0300
Subject: [PATCH 05/24] Use messages for yaml witness validation output

---
 src/util/messageCategory.ml  |  5 +++++
 src/util/options.schema.json |  6 ++++++
 src/witness/yamlWitness.ml   | 34 ++++++++++++++++++++++------------
 3 files changed, 33 insertions(+), 12 deletions(-)

diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml
index 6ec026fa83..cf51baacc1 100644
--- a/src/util/messageCategory.ml
+++ b/src/util/messageCategory.ml
@@ -35,6 +35,7 @@ type category =
   | Analyzer
   | Unsound
   | Imprecise
+  | Witness
 [@@deriving eq, ord, hash]
 
 type t = category [@@deriving eq, ord, hash]
@@ -169,6 +170,7 @@ let should_warn e =
     | Analyzer -> "analyzer"
     | Unsound -> "unsound"
     | Imprecise -> "imprecise"
+    | Witness -> "witness"
   in get_bool ("warn." ^ (to_string e))
 
 let path_show e =
@@ -184,6 +186,7 @@ let path_show e =
   | Analyzer -> ["Analyzer"]
   | Unsound -> ["Unsound"]
   | Imprecise -> ["Imprecise"]
+  | Witness -> ["Witness"]
 
 let show x = String.concat " > " (path_show x)
 
@@ -208,6 +211,7 @@ let categoryName = function
   | Analyzer -> "Analyzer"
   | Unsound -> "Unsound"
   | Imprecise -> "Imprecise"
+  | Witness -> "Witness"
 
   | Behavior x -> behaviorName x
   | Integer x -> match x with
@@ -229,6 +233,7 @@ let from_string_list (s: string list) =
     | "analyzer" -> Analyzer
     | "unsound" -> Unsound
     | "imprecise" -> Imprecise
+    | "witness" -> Witness
     | _ -> Unknown
 
 let to_yojson x = `List (List.map (fun x -> `String x) (path_show x))
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index da1580c60c..2399b123c7 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1586,6 +1586,12 @@
           "type": "boolean",
           "default": true
         },
+        "witness": {
+          "title": "warn.witness",
+          "description": "Witness messages",
+          "type": "boolean",
+          "default": true
+        },
         "unknown": {
           "title": "warn.unknown",
           "description": "Unknown (of string) warnings",
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index d98e8fe25f..dc5de420f1 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -191,25 +191,35 @@ struct
           endByte = -1;
         }
         in
-        ignore (Pretty.printf "%a: %s\n" CilType.Location.pretty loc inv);
 
         (* TODO: better node finding *)
-        NH.iter (fun n d ->
+        let found = NH.fold (fun n d found ->
             let nloc = Node.location n in
             if loc.file = nloc.file && loc.line = nloc.line && loc.column = nloc.column then (
-              ignore (Pretty.printf "  %a\n" Node.pretty n);
-
               let fd = Node.find_fundec n in
               let local_variables = (fd.slocals @ fd.sformals) |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v) in
 
-              match Formatcil.cExp inv (local_variables @ global_variables) with
-              | inv_exp ->
-                ignore (Pretty.printf "  parsed %a\n" Cil.d_plainexp inv_exp);
-                let r = ask_local n d (Queries.EvalInt inv_exp) in
-                ignore (Pretty.printf "  -> %a\n" Queries.ID.pretty r)
-              | exception _ ->
-                ignore (Pretty.printf "  couldn't parse %s\n" inv)
+              begin match Formatcil.cExp inv (local_variables @ global_variables) with
+                | inv_exp ->
+                  begin match ask_local n d (Queries.EvalInt inv_exp) with
+                    | x when Queries.ID.is_bool x ->
+                      if Option.get (Queries.ID.to_bool x) then
+                        M.success ~category:Witness ~loc "invariant confirmed: %s" inv
+                      else
+                        M.error ~category:Witness ~loc "invariant refuted: %s" inv
+                    | _ ->
+                      M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv
+                  end
+                | exception _ ->
+                  M.error ~category:Witness ~loc "couldn't parse invariant: %s" inv
+              end;
+              true
             )
-          ) nh
+            else
+              found
+          ) nh false
+        in
+        if not found then
+          M.warn ~category:Witness ~loc "couldn't locate invariant: %s" inv
       ) yaml_entries
 end

From a3d32645bade4aabb1e0a0b8914dbd1538f14aa1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 17:18:18 +0300
Subject: [PATCH 06/24] Validate yaml witnesses context sensitively

---
 src/witness/yamlWitness.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index dc5de420f1..eeea615a65 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -141,22 +141,21 @@ struct
     nh
 
   let validate lh gh (file: Cil.file) =
-    let nh = join_contexts lh in
 
     let global_variables =
       file.globals
       |> List.filter_map (function Cil.GVar (v, _, _) -> Some (v.vname, Cil.Fv v) | _ -> None)
     in
 
-    let ask_local n local =
+    let ask_local (lvar:EQSys.LVar.t) local =
       (* build a ctx for using the query system *)
       let rec ctx =
         { ask    = (fun (type a) (q: a Queries.t) -> Spec.query ctx q)
         ; emit   = (fun _ -> failwith "Cannot \"emit\" in witness context.")
-        ; node   = n
+        ; node   = fst lvar
         ; prev_node = MyCFG.dummy_node
-        ; control_context = Obj.repr (fun () -> failwith "TODO")
-        ; context = (fun () -> failwith "TODO")
+        ; control_context = Obj.repr (fun () -> snd lvar)
+        ; context = (fun () -> snd lvar)
         ; edge    = MyCFG.Skip
         ; local  = local
         ; global = GHT.find gh
@@ -193,7 +192,7 @@ struct
         in
 
         (* TODO: better node finding *)
-        let found = NH.fold (fun n d found ->
+        let found = LHT.fold (fun ((n, _) as lvar) d found ->
             let nloc = Node.location n in
             if loc.file = nloc.file && loc.line = nloc.line && loc.column = nloc.column then (
               let fd = Node.find_fundec n in
@@ -201,7 +200,7 @@ struct
 
               begin match Formatcil.cExp inv (local_variables @ global_variables) with
                 | inv_exp ->
-                  begin match ask_local n d (Queries.EvalInt inv_exp) with
+                  begin match ask_local lvar d (Queries.EvalInt inv_exp) with
                     | x when Queries.ID.is_bool x ->
                       if Option.get (Queries.ID.to_bool x) then
                         M.success ~category:Witness ~loc "invariant confirmed: %s" inv
@@ -217,7 +216,7 @@ struct
             )
             else
               found
-          ) nh false
+          ) lh false
         in
         if not found then
           M.warn ~category:Witness ~loc "couldn't locate invariant: %s" inv

From a92600d89e99588165178b7ed28f1803c4277e4d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 May 2022 10:58:26 +0300
Subject: [PATCH 07/24] Check parsed yaml witness invariants to avoid
 downstream crashing

---
 goblint.opam               |  2 +-
 goblint.opam.locked        |  2 +-
 goblint.opam.template      |  2 +-
 src/witness/yamlWitness.ml | 19 ++++++++++++-------
 4 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index 26d33c1475..637a9a945c 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -68,7 +68,7 @@ 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!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#56f5f9ad58e71908ff66e179e056a22ea71693a2" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#bbfc0b3a3a2604f6a7e8060082ba29e3b61f8d47" ]
   # 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" ]
   # quoter workaround reverted for release, so no pin needed
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 9946ac7b25..aa23632214 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -124,7 +124,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#56f5f9ad58e71908ff66e179e056a22ea71693a2"
+    "git+https://github.com/goblint/cil.git#bbfc0b3a3a2604f6a7e8060082ba29e3b61f8d47"
   ]
   [
     "apron.v0.9.13"
diff --git a/goblint.opam.template b/goblint.opam.template
index 5813c9f0ae..73efa5877a 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#56f5f9ad58e71908ff66e179e056a22ea71693a2" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#bbfc0b3a3a2604f6a7e8060082ba29e3b61f8d47" ]
   # 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" ]
   # quoter workaround reverted for release, so no pin needed
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index eeea615a65..4f703f2c71 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -142,9 +142,10 @@ struct
 
   let validate lh gh (file: Cil.file) =
 
-    let global_variables =
-      file.globals
-      |> List.filter_map (function Cil.GVar (v, _, _) -> Some (v.vname, Cil.Fv v) | _ -> None)
+    let global_vars = List.filter_map (function
+        | Cil.GVar (v, _, _) -> Some v
+        | _ -> None
+      ) file.globals
     in
 
     let ask_local (lvar:EQSys.LVar.t) local =
@@ -196,11 +197,13 @@ struct
             let nloc = Node.location n in
             if loc.file = nloc.file && loc.line = nloc.line && loc.column = nloc.column then (
               let fd = Node.find_fundec n in
-              let local_variables = (fd.slocals @ fd.sformals) |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v) in
+              let vars = fd.sformals @ fd.slocals @ global_vars in
+              let fas = List.map (fun (v: Cil.varinfo) -> (v.vname, Cil.Fv v)) vars in
 
-              begin match Formatcil.cExp inv (local_variables @ global_variables) with
+              begin match Formatcil.cExp inv fas with
                 | inv_exp ->
-                  begin match ask_local lvar d (Queries.EvalInt inv_exp) with
+                  if Check.checkStandaloneExp ~vars inv_exp then (
+                    match ask_local lvar d (Queries.EvalInt inv_exp) with
                     | x when Queries.ID.is_bool x ->
                       if Option.get (Queries.ID.to_bool x) then
                         M.success ~category:Witness ~loc "invariant confirmed: %s" inv
@@ -208,7 +211,9 @@ struct
                         M.error ~category:Witness ~loc "invariant refuted: %s" inv
                     | _ ->
                       M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv
-                  end
+                  )
+                  else
+                    M.error ~category:Witness ~loc "invalid CIL expression invariant: %s" inv
                 | exception _ ->
                   M.error ~category:Witness ~loc "couldn't parse invariant: %s" inv
               end;

From 7d3cd2f6ced8aeeb7981ba96f66f5f0971e63272 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 May 2022 11:13:57 +0300
Subject: [PATCH 08/24] Clean up YamlWitness.Validator

---
 src/witness/yamlWitness.ml | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 4f703f2c71..5cfc9a97cd 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -129,17 +129,6 @@ module Validator
     (GHT : BatHashtbl.S with type key = EQSys.GVar.t) =
 struct
 
-  module NH = BatHashtbl.Make (Node)
-
-  (* copied from Constraints.CompareNode *)
-  let join_contexts (lh: Spec.D.t LHT.t): Spec.D.t NH.t =
-    let nh = NH.create 113 in
-    LHT.iter (fun (n, _) d ->
-        let d' = try Spec.D.join (NH.find nh n) d with Not_found -> d in
-        NH.replace nh n d'
-      ) lh;
-    nh
-
   let validate lh gh (file: Cil.file) =
 
     let global_vars = List.filter_map (function
@@ -213,7 +202,7 @@ struct
                       M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv
                   )
                   else
-                    M.error ~category:Witness ~loc "invalid CIL expression invariant: %s" inv
+                    M.error ~category:Witness ~loc "broken CIL expression invariant: %s" inv
                 | exception _ ->
                   M.error ~category:Witness ~loc "couldn't parse invariant: %s" inv
               end;

From 14c51293e53221d1b8919986d9a613125f76dd52 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 May 2022 12:20:37 +0300
Subject: [PATCH 09/24] Locate yaml witness invariants efficiently and
 inexactly

---
 src/witness/yamlWitness.ml | 76 ++++++++++++++++++++++++--------------
 1 file changed, 48 insertions(+), 28 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 5cfc9a97cd..acf4e78a12 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -129,7 +129,19 @@ module Validator
     (GHT : BatHashtbl.S with type key = EQSys.GVar.t) =
 struct
 
+  module FileH = BatHashtbl.Make (Basetype.RawStrings)
+  module LocM = BatMap.Make (CilType.Location)
+  module LvarS = BatSet.Make (EQSys.LVar)
+
   let validate lh gh (file: Cil.file) =
+    (* for each file, locations (of lvar nodes) have total order, so LocM essentially does binary search *)
+    let file_loc_lvars: LvarS.t LocM.t FileH.t = FileH.create 100 in
+    LHT.iter (fun ((n, _) as lvar) _ ->
+        let loc = Node.location n in
+        FileH.modify_def LocM.empty loc.file (
+          LocM.modify_def LvarS.empty loc (LvarS.add lvar)
+        ) file_loc_lvars
+      ) lh;
 
     let global_vars = List.filter_map (function
         | Cil.GVar (v, _, _) -> Some v
@@ -181,38 +193,46 @@ struct
         }
         in
 
-        (* TODO: better node finding *)
-        let found = LHT.fold (fun ((n, _) as lvar) d found ->
-            let nloc = Node.location n in
-            if loc.file = nloc.file && loc.line = nloc.line && loc.column = nloc.column then (
+        let lvars_opt: LvarS.t option =
+          let (let*) = Option.bind in (* TODO: move to general library *)
+          let* loc_lvars = FileH.find_option file_loc_lvars loc.file in
+          (* for each file, locations (of lvar nodes) have total order, so LocM essentially does binary search *)
+          let* (_, lvars) = LocM.find_first_opt (fun loc' ->
+              CilType.Location.compare loc loc' <= 0 (* allow inexact match *)
+            ) loc_lvars
+          in
+          if LvarS.is_empty lvars then
+            None
+          else
+            Some lvars
+        in
+
+        match lvars_opt with
+        | Some lvars ->
+          LvarS.iter (fun ((n, _) as lvar) ->
+              let d = LHT.find lh lvar in
               let fd = Node.find_fundec n in
               let vars = fd.sformals @ fd.slocals @ global_vars in
               let fas = List.map (fun (v: Cil.varinfo) -> (v.vname, Cil.Fv v)) vars in
 
-              begin match Formatcil.cExp inv fas with
-                | inv_exp ->
-                  if Check.checkStandaloneExp ~vars inv_exp then (
-                    match ask_local lvar d (Queries.EvalInt inv_exp) with
-                    | x when Queries.ID.is_bool x ->
-                      if Option.get (Queries.ID.to_bool x) then
-                        M.success ~category:Witness ~loc "invariant confirmed: %s" inv
-                      else
-                        M.error ~category:Witness ~loc "invariant refuted: %s" inv
-                    | _ ->
-                      M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv
-                  )
-                  else
-                    M.error ~category:Witness ~loc "broken CIL expression invariant: %s" inv
-                | exception _ ->
-                  M.error ~category:Witness ~loc "couldn't parse invariant: %s" inv
-              end;
-              true
-            )
-            else
-              found
-          ) lh false
-        in
-        if not found then
+              match Formatcil.cExp inv fas with
+              | inv_exp ->
+                if Check.checkStandaloneExp ~vars inv_exp then (
+                  match ask_local lvar d (Queries.EvalInt inv_exp) with
+                  | x when Queries.ID.is_bool x ->
+                    if Option.get (Queries.ID.to_bool x) then
+                      M.success ~category:Witness ~loc "invariant confirmed: %s" inv
+                    else
+                      M.error ~category:Witness ~loc "invariant refuted: %s" inv
+                  | _ ->
+                    M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv
+                )
+                else
+                  M.error ~category:Witness ~loc "broken CIL expression invariant: %s" inv
+              | exception _ ->
+                M.error ~category:Witness ~loc "couldn't parse invariant: %s" inv
+            ) lvars
+        | None ->
           M.warn ~category:Witness ~loc "couldn't locate invariant: %s" inv
       ) yaml_entries
 end

From 3841fe79e0957bae0b59f00a7dcd4508e5cc3278 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 May 2022 12:57:47 +0300
Subject: [PATCH 10/24] Hide mutex structure contents in base analysis

---
 src/cdomains/valueDomain.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index b66cec2bb1..b01934329d 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -883,6 +883,7 @@ struct
       let mu = function `Blob (`Blob (y, s', orig), s, orig2) -> `Blob (y, ID.join s s',orig) | x -> x in
       let r =
       match x, offs with
+      | _, _ when is_mutex_type t -> `Top (* hide mutex structure contents, not updated anyway *)
       | `Blob (x,s,orig), `Index (_,ofs) ->
         begin
           let l', o' = shift_one_over l o in

From db1ce04e5d1d52f6c6633fa2ab63180ff6d8cd87 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 May 2022 13:25:31 +0300
Subject: [PATCH 11/24] Insert explicit casts in IntDomain invariants

---
 src/cdomains/intDomain.ml  | 10 +++++-----
 src/witness/yamlWitness.ml |  2 +-
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index d0e18db891..1ebc343438 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -830,7 +830,7 @@ struct
   let invariant c x = failwith "unimplemented"
 
   let invariant_ikind c ik x =
-    let c = Cil.(Lval (BatOption.get c.Invariant.lval)) in
+    let c = Cil.(mkCast ~e:(Lval (BatOption.get c.Invariant.lval)) ~newt:(TInt (ik, []))) in
     match x with
     | Some (x1, x2) when Ints_t.compare x1 x2 = 0 ->
       let x1 = Ints_t.to_bigint x1 in
@@ -1599,7 +1599,7 @@ struct
   let lognot ik = eq ik (of_int ik BigInt.zero)
 
   let invariant_ikind c ik (x:t) =
-    let c = Cil.(Lval (BatOption.get c.Invariant.lval)) in
+    let c = Cil.(mkCast ~e:(Lval (BatOption.get c.Invariant.lval)) ~newt:(TInt (ik, []))) in
     match x with
     | `Definite x -> Invariant.of_exp Cil.(BinOp (Eq, c, kintegerCilint ik x, intType))
     | `Excluded (s, _) ->
@@ -2005,7 +2005,7 @@ module Enums : S with type int_t = BigInt.t = struct
   let ne ik x y = lognot ik (eq ik x y)
 
   let invariant_ikind c ik x =
-    let c = Cil.(Lval (Option.get c.Invariant.lval)) in
+    let c = Cil.(mkCast ~e:(Lval (BatOption.get c.Invariant.lval)) ~newt:(TInt (ik, []))) in
     match x with
     | Inc ps ->
       List.fold_left (fun a x ->
@@ -2448,7 +2448,7 @@ struct
     res
 
   let invariant_ikind ctxt ik x =
-    let l = Cil.(Lval (BatOption.get ctxt.Invariant.lval)) in
+    let l = Cil.(mkCast ~e:(Lval (BatOption.get ctxt.Invariant.lval)) ~newt:(TInt (ik, []))) in
     match x with
     | Some (c, m) when m =: Ints_t.zero ->
       let c = Ints_t.to_bigint c in
@@ -2894,7 +2894,7 @@ module IntDomTupleImpl = struct
     match to_int x with
     | Some v ->
       (* If definite, output single equality instead of every subdomain repeating same equality *)
-      let c_exp = Cil.(Lval (Option.get c.Invariant.lval)) in
+      let c_exp = Cil.(mkCast ~e:(Lval (BatOption.get c.Invariant.lval)) ~newt:(TInt (ik, []))) in
       Invariant.of_exp Cil.(BinOp (Eq, c_exp, kintegerCilint ik v, intType))
     | None ->
       let is = to_list (mapp { fp = fun (type a) (module I:S with type t = a) -> I.invariant_ikind c ik } x)
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index acf4e78a12..e43e13c5e2 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -228,7 +228,7 @@ struct
                     M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv
                 )
                 else
-                  M.error ~category:Witness ~loc "broken CIL expression invariant: %s" inv
+                  M.error ~category:Witness ~loc "broken CIL expression invariant: %s (%a)" inv Cil.d_plainexp inv_exp
               | exception _ ->
                 M.error ~category:Witness ~loc "couldn't parse invariant: %s" inv
             ) lvars

From 53495c1e21aacae7bf86abb795212e5fcc2a6e42 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 May 2022 13:34:21 +0300
Subject: [PATCH 12/24] Use long long zero in apron invariants to match lhs

---
 src/cdomains/apron/apronDomain.apron.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 873e48b54e..d47253c930 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -335,7 +335,7 @@ struct
 
 
   let cil_exp_of_lincons1 fundec (lincons1:Lincons1.t) =
-    let zero = Cil.zero in
+    let zero = Cil.kinteger ILongLong 0 in
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
       let cilexp = cil_exp_of_linexpr1 fundec linexpr1 in

From 1fa8d17ffa46849911da243b741d34c2a89f19d3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 May 2022 17:01:16 +0300
Subject: [PATCH 13/24] Use bot instead of top for base mutex contents

This avoids unknown value escape warnings.
---
 src/cdomains/valueDomain.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index b01934329d..48727c03c1 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -142,7 +142,7 @@ struct
 
   let rec init_value (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *)
     match t with
-    | t when is_mutex_type t -> `Top
+    | t when is_mutex_type t -> `Bot (* use `Bot instead of `Top to avoid unknown value escape warnings *)
     | TInt (ik,_) -> `Int (ID.top_of ik)
     | TPtr _ -> `Address AD.top_ptr
     | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> init_value fd.ftype) ci)
@@ -883,7 +883,8 @@ struct
       let mu = function `Blob (`Blob (y, s', orig), s, orig2) -> `Blob (y, ID.join s s',orig) | x -> x in
       let r =
       match x, offs with
-      | _, _ when is_mutex_type t -> `Top (* hide mutex structure contents, not updated anyway *)
+      | _, _ when is_mutex_type t -> (* hide mutex structure contents, not updated anyway *)
+        `Bot (* use `Bot instead of `Top to avoid unknown value escape warnings *)
       | `Blob (x,s,orig), `Index (_,ofs) ->
         begin
           let l', o' = shift_one_over l o in

From 4c8d769a72406a6656beca24b93e7850ce94b717 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 26 May 2022 10:25:40 +0300
Subject: [PATCH 14/24] Use Frontc to parse yaml witness invariants

---
 goblint.opam               |  2 +-
 goblint.opam.locked        |  2 +-
 goblint.opam.template      |  2 +-
 src/witness/yamlWitness.ml | 88 ++++++++++++++++++++++----------------
 4 files changed, 53 insertions(+), 41 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index 637a9a945c..0de7ba3927 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -68,7 +68,7 @@ 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!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#bbfc0b3a3a2604f6a7e8060082ba29e3b61f8d47" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#a6c158d8db352f38db0ad026e22128321031e185" ]
   # 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" ]
   # quoter workaround reverted for release, so no pin needed
diff --git a/goblint.opam.locked b/goblint.opam.locked
index aa23632214..420a8799cd 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -124,7 +124,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#bbfc0b3a3a2604f6a7e8060082ba29e3b61f8d47"
+    "git+https://github.com/goblint/cil.git#a6c158d8db352f38db0ad026e22128321031e185"
   ]
   [
     "apron.v0.9.13"
diff --git a/goblint.opam.template b/goblint.opam.template
index 73efa5877a..1a16cf74ff 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#bbfc0b3a3a2604f6a7e8060082ba29e3b61f8d47" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#a6c158d8db352f38db0ad026e22128321031e185" ]
   # 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" ]
   # quoter workaround reverted for release, so no pin needed
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index e43e13c5e2..3a382a9e50 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -193,46 +193,58 @@ struct
         }
         in
 
-        let lvars_opt: LvarS.t option =
-          let (let*) = Option.bind in (* TODO: move to general library *)
-          let* loc_lvars = FileH.find_option file_loc_lvars loc.file in
-          (* for each file, locations (of lvar nodes) have total order, so LocM essentially does binary search *)
-          let* (_, lvars) = LocM.find_first_opt (fun loc' ->
-              CilType.Location.compare loc loc' <= 0 (* allow inexact match *)
-            ) loc_lvars
+        match Frontc.parse_standalone_exp inv with
+        | inv_cabs ->
+
+          let lvars_opt: LvarS.t option =
+            let (let*) = Option.bind in (* TODO: move to general library *)
+            let* loc_lvars = FileH.find_option file_loc_lvars loc.file in
+            (* for each file, locations (of lvar nodes) have total order, so LocM essentially does binary search *)
+            let* (_, lvars) = LocM.find_first_opt (fun loc' ->
+                CilType.Location.compare loc loc' <= 0 (* allow inexact match *)
+              ) loc_lvars
+            in
+            if LvarS.is_empty lvars then
+              None
+            else
+              Some lvars
           in
-          if LvarS.is_empty lvars then
-            None
-          else
-            Some lvars
-        in
 
-        match lvars_opt with
-        | Some lvars ->
-          LvarS.iter (fun ((n, _) as lvar) ->
-              let d = LHT.find lh lvar in
-              let fd = Node.find_fundec n in
-              let vars = fd.sformals @ fd.slocals @ global_vars in
-              let fas = List.map (fun (v: Cil.varinfo) -> (v.vname, Cil.Fv v)) vars in
-
-              match Formatcil.cExp inv fas with
-              | inv_exp ->
-                if Check.checkStandaloneExp ~vars inv_exp then (
-                  match ask_local lvar d (Queries.EvalInt inv_exp) with
-                  | x when Queries.ID.is_bool x ->
-                    if Option.get (Queries.ID.to_bool x) then
-                      M.success ~category:Witness ~loc "invariant confirmed: %s" inv
+          begin match lvars_opt with
+            | Some lvars ->
+              LvarS.iter (fun ((n, _) as lvar) ->
+                  let d = LHT.find lh lvar in
+                  let fd = Node.find_fundec n in
+                  let vars = fd.sformals @ fd.slocals @ global_vars in
+
+                  let genv = Cabs2cil.genvironment in
+                  let env = Hashtbl.copy genv in
+                  List.iter (fun (v: Cil.varinfo) ->
+                      Hashtbl.replace env v.vname (Cabs2cil.EnvVar v, v.vdecl)
+                    ) (fd.sformals @ fd.slocals);
+
+                  match Cabs2cil.convStandaloneExp ~genv ~env inv_cabs with
+                  | Some inv_exp ->
+                    if Check.checkStandaloneExp ~vars inv_exp then (
+                      match ask_local lvar d (Queries.EvalInt inv_exp) with
+                      | x when Queries.ID.is_bool x ->
+                        if Option.get (Queries.ID.to_bool x) then
+                          M.success ~category:Witness ~loc "invariant confirmed: %s" inv
+                        else
+                          M.error ~category:Witness ~loc "invariant refuted: %s" inv
+                      | _ ->
+                        M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv
+                    )
                     else
-                      M.error ~category:Witness ~loc "invariant refuted: %s" inv
-                  | _ ->
-                    M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv
-                )
-                else
-                  M.error ~category:Witness ~loc "broken CIL expression invariant: %s (%a)" inv Cil.d_plainexp inv_exp
-              | exception _ ->
-                M.error ~category:Witness ~loc "couldn't parse invariant: %s" inv
-            ) lvars
-        | None ->
-          M.warn ~category:Witness ~loc "couldn't locate invariant: %s" inv
+                      M.error ~category:Witness ~loc "broken CIL expression invariant: %s (%a)" inv Cil.d_plainexp inv_exp
+                  | None ->
+                    M.error ~category:Witness ~loc "CIL couldn't parse invariant: %s" inv
+                ) lvars
+            | None ->
+              M.warn ~category:Witness ~loc "couldn't locate invariant: %s" inv
+          end
+        | exception Frontc.ParseError _ ->
+          Errormsg.log "\n"; (* CIL prints garbage without \n before *)
+          M.error ~category:Witness ~loc "Frontc couldn't parse invariant: %s" inv
       ) yaml_entries
 end

From 4e5e10c7698bd7db4ff064f3cea51672cbd66c3d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 26 May 2022 10:55:23 +0300
Subject: [PATCH 15/24] Fix Cabs2cil mangling fundec locals during yaml witness
 invariant parsing

---
 goblint.opam               |  2 +-
 goblint.opam.locked        |  2 +-
 goblint.opam.template      |  2 +-
 src/witness/yamlWitness.ml | 14 +++++++++++++-
 4 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index 0de7ba3927..a1ffc3d048 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -68,7 +68,7 @@ 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!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#a6c158d8db352f38db0ad026e22128321031e185" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#fe7da7b4203735d84670e68f3044a9bf33bd6e65" ]
   # 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" ]
   # quoter workaround reverted for release, so no pin needed
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 420a8799cd..adf761e3c8 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -124,7 +124,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#a6c158d8db352f38db0ad026e22128321031e185"
+    "git+https://github.com/goblint/cil.git#fe7da7b4203735d84670e68f3044a9bf33bd6e65"
   ]
   [
     "apron.v0.9.13"
diff --git a/goblint.opam.template b/goblint.opam.template
index 1a16cf74ff..0ba278543a 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#a6c158d8db352f38db0ad026e22128321031e185" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#fe7da7b4203735d84670e68f3044a9bf33bd6e65" ]
   # 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" ]
   # quoter workaround reverted for release, so no pin needed
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 3a382a9e50..f03c48b0c9 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -223,7 +223,19 @@ struct
                       Hashtbl.replace env v.vname (Cabs2cil.EnvVar v, v.vdecl)
                     ) (fd.sformals @ fd.slocals);
 
-                  match Cabs2cil.convStandaloneExp ~genv ~env inv_cabs with
+                  let inv_exp_opt =
+                    Cil.currentLoc := loc;
+                    Cil.currentExpLoc := loc;
+                    Cabs2cil.currentFunctionFDEC := fd;
+                    let old_locals = fd.slocals in
+                    Fun.protect ~finally:(fun () ->
+                        fd.slocals <- old_locals (* restore locals, Cabs2cil may mangle them by inserting temporary variables *)
+                      ) (fun () ->
+                        Cabs2cil.convStandaloneExp ~genv ~env inv_cabs
+                      )
+                  in
+
+                  match inv_exp_opt with
                   | Some inv_exp ->
                     if Check.checkStandaloneExp ~vars inv_exp then (
                       match ask_local lvar d (Queries.EvalInt inv_exp) with

From b42da55c7d4034b609890c6d5bdc9a03b7c25930 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 26 May 2022 11:17:20 +0300
Subject: [PATCH 16/24] Use logical operators in yaml witness invariant parsing

---
 src/witness/yamlWitness.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index f03c48b0c9..1f9e43e224 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -228,9 +228,12 @@ struct
                     Cil.currentExpLoc := loc;
                     Cabs2cil.currentFunctionFDEC := fd;
                     let old_locals = fd.slocals in
+                    let old_useLogicalOperators = !Cil.useLogicalOperators in
                     Fun.protect ~finally:(fun () ->
-                        fd.slocals <- old_locals (* restore locals, Cabs2cil may mangle them by inserting temporary variables *)
+                        fd.slocals <- old_locals; (* restore locals, Cabs2cil may mangle them by inserting temporary variables *)
+                        Cil.useLogicalOperators := old_useLogicalOperators
                       ) (fun () ->
+                        Cil.useLogicalOperators := true;
                         Cabs2cil.convStandaloneExp ~genv ~env inv_cabs
                       )
                   in

From 4e997270d551e286ca0ed3c987202aef805ffb3d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 26 May 2022 11:34:38 +0300
Subject: [PATCH 17/24] Add Question exp handling

These may occur in yaml witness invariants.
---
 src/analyses/base.ml            |  2 +-
 src/analyses/malloc_null.ml     |  2 +-
 src/analyses/tutorials/taint.ml |  2 +-
 src/analyses/uninit.ml          |  2 +-
 src/analyses/varEq.ml           | 26 +++++++++++++-------------
 src/cdomains/basetype.ml        |  6 +++---
 src/cdomains/exp.ml             | 28 ++++++++++++++--------------
 src/cdomains/lockDomain.ml      |  6 +++---
 src/domains/access.ml           |  4 ++--
 src/domains/invariantCil.ml     |  2 +-
 src/incremental/compareAST.ml   |  2 +-
 src/transform/evalAssert.ml     |  2 +-
 12 files changed, 42 insertions(+), 42 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 7658ecad96..493ff25cb7 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -797,7 +797,7 @@ struct
       | CastE  (t, exp) ->
         let v = eval_rv a gs st exp in
         VD.cast ~torg:(Cilfacade.typeOf exp) t v
-      | _ -> VD.top ()
+      | _ -> VD.top () (* TODO: remove wildcard *)
     in
     if M.tracing then M.traceu "evalint" "base eval_rv_base %a -> %a\n" d_exp exp VD.pretty r;
     r
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 0f38566d1e..104ef49719 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -79,7 +79,7 @@ struct
     | UnOp (_,e,_)
     | CastE  (_,e) ->
       warn_deref_exp a st e
-    | _ -> ()
+    | _ -> () (* TODO: remove wildcard *)
 
   let may (f: 'a -> 'b) (x: 'a option) : unit =
     match x with
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 83721d802b..d5c7360fa0 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -42,7 +42,7 @@ struct
     | CastE (_,e)
     | UnOp (_,e,_) -> is_exp_tainted state e
     | SizeOf _ | SizeOfStr _ | Const _  | AlignOf _ | AddrOfLabel _ -> false
-    | Question _ -> failwith "should be optimized away by CIL"
+    | Question (b, t, f, _) -> is_exp_tainted state b || is_exp_tainted state t || is_exp_tainted state f
   and is_lval_tainted state = function
     | (Var v, _) ->
       (* TODO: Check whether variable v is tainted *)
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index b859d4ed81..48480c5307 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -65,7 +65,7 @@ struct
     | StartOf lval -> access_lv_byval a lval
     (* Most casts are currently just ignored, that's probably not a good idea! *)
     | CastE  (t, exp) -> access_one_byval a rw exp
-    | _ -> []
+    | _ -> [] (* TODO: remove wildcard *)
   (* Accesses during the evaluation of an lval, not the lval itself! *)
   and access_lv_byval a (lval:lval) =
     let rec access_offset (ofs: offset) =
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index ce93e043dd..1044598b23 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -145,8 +145,8 @@ struct
       | AddrOf (Mem e,o)
       | StartOf (Mem e,o) -> may_change_t_offset o || type_may_change_t e bt
       | CastE (t,e) -> type_may_change_t e bt
-      | Question _ -> failwith "Logical operations should be compiled away by CIL."
-      | _ -> failwith "Unmatched pattern."
+      | Question (b, t, f, _) -> type_may_change_t b bt || type_may_change_t t bt || type_may_change_t f bt
+      | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     let bt =  unrollTypeDeep (Cilfacade.typeOf b) in
     type_may_change_t a bt
@@ -178,8 +178,8 @@ struct
       | AddrOf (Mem e,o)
       | StartOf (Mem e,o) -> may_change_pt_offset o || lval_may_change_pt e bl
       | CastE (t,e) -> lval_may_change_pt e bl
-      | Question _ -> failwith "Logical operations should be compiled away by CIL."
-      | _ -> failwith "Unmatched pattern."
+      | Question (b, t, f, _) -> lval_may_change_pt t bl || lval_may_change_pt t bl || lval_may_change_pt f bl
+      | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     let bls = pt b in
     if Queries.LS.is_top bls
@@ -245,8 +245,8 @@ struct
               | AddrOf (Mem e,o)  -> (*Messages.warn "Addr" ;*) may_change_t_offset o || type_may_change_t false e
               | StartOf (Mem e,o) -> (*Messages.warn "Start";*) may_change_t_offset o || type_may_change_t false e
               | CastE (t,e) -> type_may_change_t deref e
-              | Question _ -> failwith "Logical operations should be compiled away by CIL."
-              | _ -> failwith "Unmatched pattern."
+              | Question (b, t, f, _) -> type_may_change_t deref b || type_may_change_t deref t || type_may_change_t deref f
+              | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
     and lval_may_change_pt a bl : bool =
       let rec may_change_pt_offset o =
@@ -311,8 +311,8 @@ struct
            | AddrOf (Mem e,o)
            | StartOf (Mem e,o) -> may_change_pt_offset o || lval_may_change_pt e bl
            | CastE (t,e) -> lval_may_change_pt e bl
-           | Question _ -> failwith "Logical operations should be compiled away by CIL."
-           | _ -> failwith "Unmatched pattern."
+           | Question (b, t, f, _) -> lval_may_change_pt b bl || lval_may_change_pt t bl || lval_may_change_pt f bl
+           | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     let r =
       if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
@@ -350,7 +350,8 @@ struct
     | AlignOf _
     | AlignOfE _
     | UnOp _
-    | BinOp _ -> None
+    | BinOp _
+    | Question _ -> None
     | Const _ -> Some false
     | Lval (Var v,_) ->
       Some (v.vglob || (ask.f (Queries.IsMultiple v)))
@@ -365,8 +366,7 @@ struct
     | AddrOf lv -> Some false (* TODO: sound?! *)
     | StartOf (Var v,_) ->  Some (ask.f (Queries.IsMultiple v)) (* Taking an address of a global is fine*)
     | StartOf lv -> Some false (* TODO: sound?! *)
-    | Question _ -> failwith "Logical operations should be compiled away by CIL."
-    | _ -> failwith "Unmatched pattern."
+    | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
   (* Set given lval equal to the result of given expression. On doubt do nothing. *)
   let add_eq ask (lv:lval) (rv:Exp.t) st =
@@ -528,6 +528,7 @@ struct
     | AlignOfE _
     | UnOp _
     | BinOp _
+    | Question _
     | AddrOf  (Var _,_)
     | StartOf (Var _,_)
     | Lval    (Var _,_) -> eq_set e s
@@ -539,8 +540,7 @@ struct
       Queries.ES.map (fun e -> Lval (mkMem ~addr:e ~off:ofs)) (eq_set_clos e s)
     | CastE (t,e) ->
       Queries.ES.map (fun e -> CastE (t,e)) (eq_set_clos e s)
-    | Question _ -> failwith "Logical operations should be compiled away by CIL."
-    | _ -> failwith "Unmatched pattern."
+    | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
 
   let query ctx (type a) (x: a Queries.t): a Queries.result =
diff --git a/src/cdomains/basetype.ml b/src/cdomains/basetype.ml
index 3d48c74292..9ee7d1475e 100644
--- a/src/cdomains/basetype.ml
+++ b/src/cdomains/basetype.ml
@@ -103,7 +103,7 @@ struct
     | UnOp (_,e,_) -> occurs x e
     | BinOp (_,e1,e2,_) -> occurs x e1 || occurs x e2
     | CastE (_,e) -> occurs x e
-    | _ -> false
+    | _ -> false (* TODO: remove wildcard? *)
 
   let replace (x:varinfo) (exp: exp) (e:exp): exp =
     let rec replace_lv (v,offs): lval =
@@ -123,7 +123,7 @@ struct
       | UnOp (op,e,t) -> UnOp (op, replace_rv e, t)
       | BinOp (op,e1,e2,t) -> BinOp (op, replace_rv e1, replace_rv e2, t)
       | CastE (t,e) -> CastE(t, replace_rv e)
-      | x -> x
+      | x -> x (* TODO: remove wildcard? *)
     in
     constFold true (replace_rv e)
 
@@ -138,7 +138,7 @@ struct
     | AlignOf _
     | Question _
     | AddrOf _
-    | StartOf _ -> []
+    | StartOf _ -> [] (* TODO: return not empty, some may contain vars! *)
     | UnOp (_, e, _ )
     | CastE (_, e)
     | Real e
diff --git a/src/cdomains/exp.ml b/src/cdomains/exp.ml
index 35c585f8ef..4a765f6ca4 100644
--- a/src/cdomains/exp.ml
+++ b/src/cdomains/exp.ml
@@ -16,7 +16,8 @@ struct
     | AlignOf _
     | AlignOfE _
     | UnOp  _
-    | BinOp _ -> false
+    | BinOp _
+    | Question _ -> false
     | Const _ -> true
     | AddrOf  (Var v2,_)
     | StartOf (Var v2,_)
@@ -25,8 +26,7 @@ struct
     | StartOf (Mem e,_)
     | Lval    (Mem e,_)
     | CastE (_,e)           -> interesting e
-    | Question _ -> failwith "Logical operations should be compiled away by CIL."
-    | _ -> failwith "Unmatched pattern."
+    | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
   let  contains_var v e =
     let rec offs_contains o =
@@ -54,8 +54,8 @@ struct
         if deref
         then CilType.Varinfo.equal v v2 || offs_contains o
         else offs_contains o
-      | Question _ -> failwith "Logical operations should be compiled away by CIL."
-      | _ -> failwith "Unmatched pattern."
+      | Question (b, t, f, _) -> cv deref b || cv deref t || cv deref f
+      | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     cv false e
 
@@ -82,8 +82,8 @@ struct
       | Lval    (Var v2,o) -> offs_contains o
       | AddrOf  (Var v2,o)
       | StartOf (Var v2,o) -> offs_contains o
-      | Question _ -> failwith "Logical operations should be compiled away by CIL."
-      | _ -> failwith "Unmatched pattern."
+      | Question (b, t, f, _) -> cv b || cv t || cv f
+      | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     cv e
 
@@ -146,6 +146,7 @@ struct
     | UnOp _
     | BinOp _
     | Const _
+    | Question _
     | Lval (Var _,_)
     | AddrOf (Var _,_)
     | StartOf (Var _,_) -> exp
@@ -156,8 +157,7 @@ struct
     | StartOf (Mem e,o) when simple_eq e q -> StartOf (Var v, addOffset o (conv_offs offs))
     | StartOf (Mem e,o)                    -> StartOf (Mem (replace_base (v,offs) q e), o)
     | CastE (t,e) -> CastE (t, replace_base (v,offs) q e)
-    | Question _ -> failwith "Logical operations should be compiled away by CIL."
-    | _ -> failwith "Unmatched pattern."
+    | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
   let rec base_compinfo q exp =
     match exp with
@@ -169,6 +169,7 @@ struct
     | UnOp _
     | BinOp _
     | Const _
+    | Question _
     | Lval (Var _,_)
     | AddrOf (Var _,_)
     | StartOf (Var _,_) -> None
@@ -179,8 +180,7 @@ struct
     | StartOf (Mem e,Field (f,_)) when simple_eq e q -> Some f.fcomp
     | StartOf (Mem e,o) -> base_compinfo q e
     | CastE (t,e) -> base_compinfo q e
-    | Question _ -> failwith "Logical operations should be compiled away by CIL."
-    | _ -> failwith "Unmatched pattern."
+    | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
   let rec conc i =
     match i with
@@ -298,14 +298,14 @@ struct
       | UnOp _
       | BinOp _
       | StartOf _
-      | Const _ -> raise NotSimpleEnough
+      | Const _
+      | Question _ -> raise NotSimpleEnough
       | Lval (Var v, os) -> EVar v :: conv_o os
       | Lval (Mem e, os) -> helper e @ [EDeref] @ conv_o os
       | AddrOf (Var v, os) -> EVar v :: conv_o os @ [EAddr]
       | AddrOf (Mem e, os) -> helper e @ [EDeref] @ conv_o os @ [EAddr]
       | CastE (_,e) -> helper e
-      | Question _ -> failwith "Logical operations should be compiled away by CIL."
-      | _ -> failwith "Unmatched pattern."
+      | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     try helper exp
     with NotSimpleEnough -> []
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index 78244bd9c3..b3f69b678f 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -123,7 +123,8 @@ struct
        | Const _
        | AlignOfE _
        | UnOp _
-       | BinOp _ -> S.empty ()
+       | BinOp _
+       | Question _ -> S.empty ()
        | AddrOf  (Var _,_)
        | StartOf (Var _,_)
        | Lval    (Var _,_) -> S.singleton e
@@ -131,8 +132,7 @@ struct
        | StartOf (Mem e,ofs) -> S.map (fun e -> StartOf (Mem e,ofs)) (eq_set ask e)
        | Lval    (Mem e,ofs) -> S.map (fun e -> Lval    (Mem e,ofs)) (eq_set ask e)
        | CastE (_,e)           -> eq_set ask e
-       | Question _ -> failwith "Logical operations should be compiled away by CIL."
-       | _ -> failwith "Unmatched pattern.")
+       | _ -> failwith "Unmatched pattern.") (* TODO: remove wildcard *)
 
   let add (ask: Queries.ask) e st =
     let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
diff --git a/src/domains/access.ml b/src/domains/access.ml
index ae3b4b0147..f5c40d6d49 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -111,7 +111,7 @@ let rec get_type (fb: typ) : exp -> acc_typ = function
         `Struct (s1, o1)
       | _ -> `Type t
     end
-  | _ -> `Type fb
+  | _ -> `Type fb (* TODO: remove wildcard *)
 
 let get_type fb e =
   (* printf "e = %a\n" d_plainexp e; *)
@@ -298,7 +298,7 @@ and distribute_access_exp f kind r c = function
     distribute_access_exp f `Read r c b;
     distribute_access_exp f kind r c t;
     distribute_access_exp f kind r c e
-  | _ -> ()
+  | _ -> () (* TODO: remove wildcard *)
 
 let add side e kind conf vo oo a =
   let ty = get_val_type e vo oo in
diff --git a/src/domains/invariantCil.ml b/src/domains/invariantCil.ml
index 1306dfed65..74c19b34ad 100644
--- a/src/domains/invariantCil.ml
+++ b/src/domains/invariantCil.ml
@@ -45,7 +45,7 @@ let rec exp_contains_tmp = function
   | UnOp (_, e, _) -> exp_contains_tmp e
   | BinOp (_, e1, e2, _) -> exp_contains_tmp e1 || exp_contains_tmp e2
   | CastE (_, e) -> exp_contains_tmp e
-  | exp -> exp = MyCFG.unknown_exp
+  | exp -> exp = MyCFG.unknown_exp (* TODO: remove wildcard *)
 
 (* TODO: synchronize magic constant with BaseDomain *)
 let var_is_heap {vname; _} = BatString.starts_with vname "(alloc@"
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index 1fb1965c7a..4109667a72 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -41,7 +41,7 @@ and eq_exp (a: exp) (b: exp) = match a,b with
   | CastE (typ1, exp1), CastE (typ2, exp2) -> eq_typ typ1 typ2 &&  eq_exp exp1 exp2
   | AddrOf lv1, AddrOf lv2 -> eq_lval lv1 lv2
   | StartOf lv1, StartOf lv2 -> eq_lval lv1 lv2
-  | _, _ -> false
+  | _, _ -> false (* TODO: remove wildcard *)
 
 and eq_lhost (a: lhost) (b: lhost) = match a, b with
     Var v1, Var v2 -> eq_varinfo v1 v2
diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index 71f4a40769..c66e8e079a 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -105,7 +105,7 @@ module EvalAssert = struct
         | Lval (Var v, _) -> [v]
         | UnOp (_, e, _) -> get_vars e
         | BinOp (_, e1, e2, _) -> (get_vars e1) @ (get_vars e2)
-        | _ -> []
+        | _ -> [] (* TODO: remove wildcard, return not empty because some may contain vars! *)
       in
 
       let instrument_join s =

From f8f39847492b8d4c5dc92685d6c8fbd69fe75eca Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 26 May 2022 16:14:22 +0300
Subject: [PATCH 18/24] Expand and fix exp pattern matching

---
 src/analyses/base.ml          | 12 +++++++++-
 src/analyses/malloc_null.ml   | 16 +++++++++++--
 src/analyses/uninit.ml        | 18 ++++++++++-----
 src/analyses/varEq.ml         | 42 ++++++++++++++++++++++-------------
 src/cdomains/basetype.ml      | 28 +++++++++++++++++++----
 src/cdomains/exp.ml           | 36 ++++++++++++++++++++----------
 src/cdomains/lockDomain.ml    |  7 ++++--
 src/domains/access.ml         | 21 ++++++++++++++----
 src/domains/invariantCil.ml   | 27 ++++++++++++++++------
 src/incremental/compareAST.ml |  6 ++++-
 src/transform/evalAssert.ml   | 10 +--------
 11 files changed, 161 insertions(+), 62 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 493ff25cb7..81679e81d8 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -700,6 +700,7 @@ struct
         let x = Pretty.sprint ~width:80 (d_const () c) in (* escapes, see impl. of d_const in cil.ml *)
         let x = String.sub x 2 (String.length x - 3) in (* remove surrounding quotes: L"foo" -> foo *)
         `Address (AD.from_string x) (* `Address (AD.str_ptr ()) *)
+      | Const _ -> VD.top ()
       (* Variables and address expressions *)
       | Lval (Var v, ofs) -> do_offs (get a gs st (eval_lv a gs st (Var v, ofs)) (Some exp)) ofs
       (*| Lval (Mem e, ofs) -> do_offs (get a gs st (eval_lv a gs st (Mem e, ofs))) ofs*)
@@ -797,7 +798,16 @@ struct
       | CastE  (t, exp) ->
         let v = eval_rv a gs st exp in
         VD.cast ~torg:(Cilfacade.typeOf exp) t v
-      | _ -> VD.top () (* TODO: remove wildcard *)
+      | SizeOf _
+      | Real _
+      | Imag _
+      | SizeOfE _
+      | SizeOfStr _
+      | AlignOf _
+      | AlignOfE _
+      | Question _
+      | AddrOfLabel _ ->
+        VD.top ()
     in
     if M.tracing then M.traceu "evalint" "base eval_rv_base %a -> %a\n" d_exp exp VD.pretty r;
     r
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 104ef49719..d80522a300 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -65,7 +65,12 @@ struct
       | _ -> ()
     in
     match e with
-    | Lval (Var v, offs) -> ()
+    | Const _
+    | SizeOf _
+    | SizeOfStr _
+    | AlignOf _
+    | AddrOfLabel _
+    | Lval (Var _, _) -> ()
     | AddrOf (Var _, _)
     | StartOf (Var _, _) ->  warn_lval_mem e NoOffset
     | AddrOf (Mem e, offs)
@@ -77,9 +82,16 @@ struct
       warn_deref_exp a st e1;
       warn_deref_exp a st e2
     | UnOp (_,e,_)
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e
     | CastE  (_,e) ->
       warn_deref_exp a st e
-    | _ -> () (* TODO: remove wildcard *)
+    | Question (b, t, f, _) ->
+      warn_deref_exp a st b;
+      warn_deref_exp a st t;
+      warn_deref_exp a st f
 
   let may (f: 'a -> 'b) (x: 'a option) : unit =
     match x with
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 48480c5307..c1ce7c4a28 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -49,8 +49,11 @@ struct
 
   let rec access_one_byval a rw (exp:exp) =
     match exp with
-    (* Integer literals *)
-    | Const _ -> []
+    | Const _
+    | SizeOf _
+    | SizeOfStr _
+    | AlignOf _
+    | AddrOfLabel _ -> []
     (* Variables and address expressions *)
     | Lval lval -> access_address a rw lval @ (access_lv_byval a lval)
     (* Binary operators *)
@@ -58,14 +61,19 @@ struct
       let a1 = access_one_byval a rw arg1 in
       let a2 = access_one_byval a rw arg2 in
       a1 @ a2
-    (* Unary operators *)
-    | UnOp (op,arg1,typ) -> access_one_byval a rw arg1
+    | UnOp (_,e,_)
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e ->
+      access_one_byval a rw e
     (* The address operators, we just check the accesses under them *)
     | AddrOf lval -> access_lv_byval a lval
     | StartOf lval -> access_lv_byval a lval
     (* Most casts are currently just ignored, that's probably not a good idea! *)
     | CastE  (t, exp) -> access_one_byval a rw exp
-    | _ -> [] (* TODO: remove wildcard *)
+    | Question (b, t, f, _) ->
+      access_one_byval a rw b @ access_one_byval a rw t @ access_one_byval a rw f
   (* Accesses during the evaluation of an lval, not the lval itself! *)
   and access_lv_byval a (lval:lval) =
     let rec access_offset (ofs: offset) =
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 1044598b23..5475a1a71f 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -135,8 +135,11 @@ struct
       | SizeOfE _
       | SizeOfStr _
       | AlignOf _
-      | AlignOfE _ -> false
-      | UnOp (_,e,_) -> type_may_change_t e bt
+      | AlignOfE _
+      | AddrOfLabel _ -> false (* TODO: some may contain exps? *)
+      | UnOp (_,e,_)
+      | Real e
+      | Imag e -> type_may_change_t e bt
       | BinOp (_,e1,e2,_) -> type_may_change_t e1 bt || type_may_change_t e2 bt
       | Lval (Var _,o)
       | AddrOf (Var _,o)
@@ -146,7 +149,6 @@ struct
       | StartOf (Mem e,o) -> may_change_t_offset o || type_may_change_t e bt
       | CastE (t,e) -> type_may_change_t e bt
       | Question (b, t, f, _) -> type_may_change_t b bt || type_may_change_t t bt || type_may_change_t f bt
-      | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     let bt =  unrollTypeDeep (Cilfacade.typeOf b) in
     type_may_change_t a bt
@@ -168,8 +170,11 @@ struct
       | SizeOfE _
       | SizeOfStr _
       | AlignOf _
-      | AlignOfE _ -> false
-      | UnOp (_,e,_) -> lval_may_change_pt e bl
+      | AlignOfE _
+      | AddrOfLabel _ -> false (* TODO: some may contain exps? *)
+      | UnOp (_,e,_)
+      | Real e
+      | Imag e -> lval_may_change_pt e bl
       | BinOp (_,e1,e2,_) -> lval_may_change_pt e1 bl || lval_may_change_pt e2 bl
       | Lval (Var _,o)
       | AddrOf (Var _,o)
@@ -179,7 +184,6 @@ struct
       | StartOf (Mem e,o) -> may_change_pt_offset o || lval_may_change_pt e bl
       | CastE (t,e) -> lval_may_change_pt e bl
       | Question (b, t, f, _) -> lval_may_change_pt t bl || lval_may_change_pt t bl || lval_may_change_pt f bl
-      | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     let bls = pt b in
     if Queries.LS.is_top bls
@@ -235,8 +239,11 @@ struct
               | SizeOfE _
               | SizeOfStr _
               | AlignOf _
-              | AlignOfE _ -> false
-              | UnOp (_,e,_) -> type_may_change_t deref e
+              | AlignOfE _
+              | AddrOfLabel _ -> false (* TODO: some may contain exps? *)
+              | UnOp (_,e,_)
+              | Real e
+              | Imag e -> type_may_change_t deref e
               | BinOp (_,e1,e2,_) -> type_may_change_t deref e1 || type_may_change_t deref e2
               | Lval (Var _,o)
               | AddrOf (Var _,o)
@@ -246,7 +253,6 @@ struct
               | StartOf (Mem e,o) -> (*Messages.warn "Start";*) may_change_t_offset o || type_may_change_t false e
               | CastE (t,e) -> type_may_change_t deref e
               | Question (b, t, f, _) -> type_may_change_t deref b || type_may_change_t deref t || type_may_change_t deref f
-              | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
     and lval_may_change_pt a bl : bool =
       let rec may_change_pt_offset o =
@@ -301,8 +307,11 @@ struct
            | SizeOfE _
            | SizeOfStr _
            | AlignOf _
-           | AlignOfE _ -> false
-           | UnOp (_,e,_) -> lval_may_change_pt e bl
+           | AlignOfE _
+           | AddrOfLabel _ -> false (* TODO: some may contain exps? *)
+           | UnOp (_,e,_)
+           | Real e
+           | Imag e -> lval_may_change_pt e bl
            | BinOp (_,e1,e2,_) -> lval_may_change_pt e1 bl || lval_may_change_pt e2 bl
            | Lval (Var _,o)
            | AddrOf (Var _,o)
@@ -312,7 +321,6 @@ struct
            | StartOf (Mem e,o) -> may_change_pt_offset o || lval_may_change_pt e bl
            | CastE (t,e) -> lval_may_change_pt e bl
            | Question (b, t, f, _) -> lval_may_change_pt b bl || lval_may_change_pt t bl || lval_may_change_pt f bl
-           | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     let r =
       if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
@@ -351,7 +359,10 @@ struct
     | AlignOfE _
     | UnOp _
     | BinOp _
-    | Question _ -> None
+    | Question _
+    | AddrOfLabel _
+    | Real _
+    | Imag _ -> None
     | Const _ -> Some false
     | Lval (Var v,_) ->
       Some (v.vglob || (ask.f (Queries.IsMultiple v)))
@@ -366,7 +377,6 @@ struct
     | AddrOf lv -> Some false (* TODO: sound?! *)
     | StartOf (Var v,_) ->  Some (ask.f (Queries.IsMultiple v)) (* Taking an address of a global is fine*)
     | StartOf lv -> Some false (* TODO: sound?! *)
-    | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
   (* Set given lval equal to the result of given expression. On doubt do nothing. *)
   let add_eq ask (lv:lval) (rv:Exp.t) st =
@@ -529,6 +539,9 @@ struct
     | UnOp _
     | BinOp _
     | Question _
+    | AddrOfLabel _
+    | Real _
+    | Imag _
     | AddrOf  (Var _,_)
     | StartOf (Var _,_)
     | Lval    (Var _,_) -> eq_set e s
@@ -540,7 +553,6 @@ struct
       Queries.ES.map (fun e -> Lval (mkMem ~addr:e ~off:ofs)) (eq_set_clos e s)
     | CastE (t,e) ->
       Queries.ES.map (fun e -> CastE (t,e)) (eq_set_clos e s)
-    | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
 
   let query ctx (type a) (x: a Queries.t): a Queries.result =
diff --git a/src/cdomains/basetype.ml b/src/cdomains/basetype.ml
index 9ee7d1475e..ce1467e50d 100644
--- a/src/cdomains/basetype.ml
+++ b/src/cdomains/basetype.ml
@@ -100,10 +100,20 @@ struct
     match e with
     | Lval l -> occurs_lv l
     | AddrOf l -> occurs_lv l
-    | UnOp (_,e,_) -> occurs x e
+    | StartOf l -> occurs_lv l
+    | UnOp (_,e,_)
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e -> occurs x e
     | BinOp (_,e1,e2,_) -> occurs x e1 || occurs x e2
     | CastE (_,e) -> occurs x e
-    | _ -> false (* TODO: remove wildcard? *)
+    | Question (b, t, f, _) -> occurs x b || occurs x t || occurs x f
+    | Const _
+    | SizeOf _
+    | SizeOfStr _
+    | AlignOf _
+    | AddrOfLabel _ -> false
 
   let replace (x:varinfo) (exp: exp) (e:exp): exp =
     let rec replace_lv (v,offs): lval =
@@ -119,11 +129,21 @@ struct
       match e with
       | Lval (Var y, NoOffset) when Variables.equal x y -> exp
       | Lval l -> Lval (replace_lv l)
-      | AddrOf l -> Lval (replace_lv l)
+      | AddrOf l -> Lval (replace_lv l) (* TODO: should be AddrOf? *)
+      | StartOf l -> StartOf (replace_lv l)
       | UnOp (op,e,t) -> UnOp (op, replace_rv e, t)
       | BinOp (op,e1,e2,t) -> BinOp (op, replace_rv e1, replace_rv e2, t)
       | CastE (t,e) -> CastE(t, replace_rv e)
-      | x -> x (* TODO: remove wildcard? *)
+      | Real e -> Real (replace_rv e)
+      | Imag e -> Imag (replace_rv e)
+      | SizeOfE e -> SizeOfE (replace_rv e)
+      | AlignOfE e -> AlignOfE (replace_rv e)
+      | Question (b, t, f, typ) -> Question (replace_rv b, replace_rv t, replace_rv f, typ)
+      | Const _
+      | SizeOf _
+      | SizeOfStr _
+      | AlignOf _
+      | AddrOfLabel _ -> e
     in
     constFold true (replace_rv e)
 
diff --git a/src/cdomains/exp.ml b/src/cdomains/exp.ml
index 4a765f6ca4..a3ea45508b 100644
--- a/src/cdomains/exp.ml
+++ b/src/cdomains/exp.ml
@@ -17,7 +17,10 @@ struct
     | AlignOfE _
     | UnOp  _
     | BinOp _
-    | Question _ -> false
+    | Question _
+    | Real _
+    | Imag _
+    | AddrOfLabel _ -> false
     | Const _ -> true
     | AddrOf  (Var v2,_)
     | StartOf (Var v2,_)
@@ -26,7 +29,6 @@ struct
     | StartOf (Mem e,_)
     | Lval    (Mem e,_)
     | CastE (_,e)           -> interesting e
-    | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
   let  contains_var v e =
     let rec offs_contains o =
@@ -41,8 +43,11 @@ struct
       | SizeOfStr _
       | AlignOf _
       | Const _
-      | AlignOfE _ -> false
-      | UnOp  (_,e,_)     -> cv deref e
+      | AlignOfE _
+      | AddrOfLabel _ -> false (* TODO: some may contain vars? *)
+      | UnOp  (_,e,_)
+      | Real e
+      | Imag e -> cv deref e
       | BinOp (_,e1,e2,_) -> cv deref e1 || cv deref e2
       | AddrOf  (Mem e,o)
       | StartOf (Mem e,o)
@@ -55,7 +60,6 @@ struct
         then CilType.Varinfo.equal v v2 || offs_contains o
         else offs_contains o
       | Question (b, t, f, _) -> cv deref b || cv deref t || cv deref f
-      | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     cv false e
 
@@ -72,8 +76,11 @@ struct
       | SizeOfStr _
       | AlignOf _
       | Const _
-      | AlignOfE _ -> false
-      | UnOp  (_,e,_)     -> cv e
+      | AlignOfE _
+      | AddrOfLabel _ -> false (* TODO: some may contain fields? *)
+      | UnOp  (_,e,_)
+      | Real e
+      | Imag e -> cv e
       | BinOp (_,e1,e2,_) -> cv e1 || cv e2
       | AddrOf  (Mem e,o)
       | StartOf (Mem e,o)
@@ -83,7 +90,6 @@ struct
       | AddrOf  (Var v2,o)
       | StartOf (Var v2,o) -> offs_contains o
       | Question (b, t, f, _) -> cv b || cv t || cv f
-      | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     cv e
 
@@ -147,6 +153,9 @@ struct
     | BinOp _
     | Const _
     | Question _
+    | Real _
+    | Imag _
+    | AddrOfLabel _
     | Lval (Var _,_)
     | AddrOf (Var _,_)
     | StartOf (Var _,_) -> exp
@@ -157,7 +166,6 @@ struct
     | StartOf (Mem e,o) when simple_eq e q -> StartOf (Var v, addOffset o (conv_offs offs))
     | StartOf (Mem e,o)                    -> StartOf (Mem (replace_base (v,offs) q e), o)
     | CastE (t,e) -> CastE (t, replace_base (v,offs) q e)
-    | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
   let rec base_compinfo q exp =
     match exp with
@@ -170,6 +178,9 @@ struct
     | BinOp _
     | Const _
     | Question _
+    | Real _
+    | Imag _
+    | AddrOfLabel _
     | Lval (Var _,_)
     | AddrOf (Var _,_)
     | StartOf (Var _,_) -> None
@@ -180,7 +191,6 @@ struct
     | StartOf (Mem e,Field (f,_)) when simple_eq e q -> Some f.fcomp
     | StartOf (Mem e,o) -> base_compinfo q e
     | CastE (t,e) -> base_compinfo q e
-    | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
 
   let rec conc i =
     match i with
@@ -299,13 +309,15 @@ struct
       | BinOp _
       | StartOf _
       | Const _
-      | Question _ -> raise NotSimpleEnough
+      | Question _
+      | Real _
+      | Imag _
+      | AddrOfLabel _ -> raise NotSimpleEnough
       | Lval (Var v, os) -> EVar v :: conv_o os
       | Lval (Mem e, os) -> helper e @ [EDeref] @ conv_o os
       | AddrOf (Var v, os) -> EVar v :: conv_o os @ [EAddr]
       | AddrOf (Mem e, os) -> helper e @ [EDeref] @ conv_o os @ [EAddr]
       | CastE (_,e) -> helper e
-      | _ -> failwith "Unmatched pattern." (* TODO: remove wildcard *)
     in
     try helper exp
     with NotSimpleEnough -> []
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index b3f69b678f..59d70f6d50 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -124,7 +124,10 @@ struct
        | AlignOfE _
        | UnOp _
        | BinOp _
-       | Question _ -> S.empty ()
+       | Question _
+       | Real _
+       | Imag _
+       | AddrOfLabel _ -> S.empty ()
        | AddrOf  (Var _,_)
        | StartOf (Var _,_)
        | Lval    (Var _,_) -> S.singleton e
@@ -132,7 +135,7 @@ struct
        | StartOf (Mem e,ofs) -> S.map (fun e -> StartOf (Mem e,ofs)) (eq_set ask e)
        | Lval    (Mem e,ofs) -> S.map (fun e -> Lval    (Mem e,ofs)) (eq_set ask e)
        | CastE (_,e)           -> eq_set ask e
-       | _ -> failwith "Unmatched pattern.") (* TODO: remove wildcard *)
+      )
 
   let add (ask: Queries.ask) e st =
     let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
diff --git a/src/domains/access.ml b/src/domains/access.ml
index f5c40d6d49..fe20965640 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -111,7 +111,11 @@ let rec get_type (fb: typ) : exp -> acc_typ = function
         `Struct (s1, o1)
       | _ -> `Type t
     end
-  | _ -> `Type fb (* TODO: remove wildcard *)
+  | Const _
+  | Lval _
+  | Real _
+  | Imag _ ->
+    `Type fb (* TODO: is this right? *)
 
 let get_type fb e =
   (* printf "e = %a\n" d_plainexp e; *)
@@ -281,8 +285,12 @@ and distribute_access_exp f kind r c = function
     distribute_access_exp f kind r c arg1;
     distribute_access_exp f kind r c arg2
 
-  (* Unary operators *)
-  | UnOp (op,arg1,typ) -> distribute_access_exp f kind r c arg1
+  | UnOp (_,e,_)
+  | Real e
+  | Imag e
+  | SizeOfE e
+  | AlignOfE e ->
+    distribute_access_exp f kind r c e
 
   (* The address operators, we just check the accesses under them *)
   | AddrOf lval | StartOf lval ->
@@ -298,7 +306,12 @@ and distribute_access_exp f kind r c = function
     distribute_access_exp f `Read r c b;
     distribute_access_exp f kind r c t;
     distribute_access_exp f kind r c e
-  | _ -> () (* TODO: remove wildcard *)
+  | Const _
+  | SizeOf _
+  | SizeOfStr _
+  | AlignOf _
+  | AddrOfLabel _ ->
+    ()
 
 let add side e kind conf vo oo a =
   let ty = get_val_type e vo oo in
diff --git a/src/domains/invariantCil.ml b/src/domains/invariantCil.ml
index 74c19b34ad..ed9e7d6ddd 100644
--- a/src/domains/invariantCil.ml
+++ b/src/domains/invariantCil.ml
@@ -39,13 +39,26 @@ let exp_is_in_scope scope e =
 let tmp_var_regexp = Str.regexp "^\\(tmp\\(___[0-9]+\\)?\\|cond\\|RETURN\\)$"
 (* let var_is_tmp {vname; _} = Str.string_match tmp_var_regexp vname 0 *)
 let var_is_tmp vi = Option.is_none (Cilfacade.find_original_name vi)
-(* TODO: use visitor for this *)
-let rec exp_contains_tmp = function
-  | Lval (Var vi, _) -> var_is_tmp vi
-  | UnOp (_, e, _) -> exp_contains_tmp e
-  | BinOp (_, e1, e2, _) -> exp_contains_tmp e1 || exp_contains_tmp e2
-  | CastE (_, e) -> exp_contains_tmp e
-  | exp -> exp = MyCFG.unknown_exp (* TODO: remove wildcard *)
+class exp_contains_tmp_visitor (acc: bool ref) = object
+  inherit nopCilVisitor as super
+  method! vvrbl (vi: varinfo) =
+    if var_is_tmp vi then
+      acc := true;
+    SkipChildren
+
+  method! vexpr (e: exp) =
+    if e = MyCFG.unknown_exp then (
+      acc := true;
+      SkipChildren
+    )
+    else
+      super#vexpr e
+end
+let exp_contains_tmp e =
+  let acc = ref false in
+  let visitor = new exp_contains_tmp_visitor acc in
+  ignore (visitCilExpr visitor e);
+  !acc
 
 (* TODO: synchronize magic constant with BaseDomain *)
 let var_is_heap {vname; _} = BatString.starts_with vname "(alloc@"
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index 4109667a72..b2a959be47 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -41,7 +41,11 @@ and eq_exp (a: exp) (b: exp) = match a,b with
   | CastE (typ1, exp1), CastE (typ2, exp2) -> eq_typ typ1 typ2 &&  eq_exp exp1 exp2
   | AddrOf lv1, AddrOf lv2 -> eq_lval lv1 lv2
   | StartOf lv1, StartOf lv2 -> eq_lval lv1 lv2
-  | _, _ -> false (* TODO: remove wildcard *)
+  | Real exp1, Real exp2 -> eq_exp exp1 exp2
+  | Imag exp1, Imag exp2 -> eq_exp exp1 exp2
+  | Question (b1, t1, f1, typ1), Question (b2, t2, f2, typ2) -> eq_exp b1 b2 && eq_exp t1 t2 && eq_exp f1 f2 && eq_typ typ1 typ2
+  | AddrOfLabel _, AddrOfLabel _ -> false (* TODO: what to do? *)
+  | _, _ -> false
 
 and eq_lhost (a: lhost) (b: lhost) = match a, b with
     Var v1, Var v2 -> eq_varinfo v1 v2
diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index c66e8e079a..000ae48b53 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -100,14 +100,6 @@ module EvalAssert = struct
         instrument_instructions il
       in
 
-      let rec get_vars e =
-        match e with
-        | Lval (Var v, _) -> [v]
-        | UnOp (_, e, _) -> get_vars e
-        | BinOp (_, e1, e2, _) -> (get_vars e1) @ (get_vars e2)
-        | _ -> [] (* TODO: remove wildcard, return not empty because some may contain vars! *)
-      in
-
       let instrument_join s =
         match s.preds with
         | [p1; p2] when emit_other ->
@@ -126,7 +118,7 @@ module EvalAssert = struct
           s.skind <- Instr (instrument_instructions il s);
           s
         | If (e, b1, b2, l,l2) ->
-          let vars = get_vars e in
+          let vars = Basetype.CilExp.get_vars e in
           let asserts loc vs = if full then make_assert loc None else List.map (fun x -> make_assert loc (Some (Var x,NoOffset))) vs |> List.concat in
           let add_asserts block =
             if block.bstmts <> [] then

From 7407e484223087f0d9fb09cff1de2fadc92e577c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 26 May 2022 17:03:05 +0300
Subject: [PATCH 19/24] Add yaml witness certification

---
 src/util/options.schema.json |  6 +++
 src/witness/yamlWitness.ml   | 78 ++++++++++++++++++++++++++++++------
 2 files changed, 72 insertions(+), 12 deletions(-)

diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 2399b123c7..c7e248dc4c 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1822,6 +1822,12 @@
               "description": "YAML witness input path",
               "type": "string",
               "default": ""
+            },
+            "certificate": {
+              "title": "witness.yaml.certificate",
+              "description": "YAML witness certificate output path",
+              "type": "string",
+              "default": "witness.certificate.yml"
             }
           },
           "additionalProperties": false
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 1f9e43e224..bfa250c55d 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -176,7 +176,25 @@ struct
       | `A yaml_entries -> yaml_entries
       | _ -> failwith "invalid YAML"
     in
-    List.iter (fun yaml_entry ->
+
+    (* TODO: deduplicate *)
+    (* yaml_conf is too verbose *)
+    (* let yaml_conf: Yaml.value = Json_repr.convert (module Json_repr.Yojson) (module Json_repr.Ezjsonm) (!GobConfig.json_conf) in *)
+    let yaml_creation_time = `String (TimeUtil.iso8601_now ()) in
+    let yaml_producer = `O [
+        ("name", `String "Goblint");
+        ("version", `String Version.goblint);
+        (* TODO: configuration *)
+        (* ("configuration", yaml_conf); *) (* yaml_conf is too verbose *)
+        ("command_line", `String Goblintutil.command_line);
+        (* TODO: description *)
+      ]
+    in
+    let sha256_file f = Sha256.(to_hex (file f)) in
+    let sha256_file_cache = BatCache.make_ht ~gen:sha256_file ~init_size:5 in
+    let sha256_file = sha256_file_cache.get in
+
+    let yaml_entries' = List.fold_left (fun yaml_entries' yaml_entry ->
         let yaml_location = Yaml.Util.(yaml_entry |> find_exn "location" |> Option.get) in
         let file = Yaml.Util.(yaml_location |> find_exn "file_name" |> Option.get |> to_string_exn) in
         let line = Yaml.Util.(yaml_location |> find_exn "line" |> Option.get |> to_float_exn |> int_of_float) in
@@ -212,7 +230,8 @@ struct
 
           begin match lvars_opt with
             | Some lvars ->
-              LvarS.iter (fun ((n, _) as lvar) ->
+              (* TODO: only one certificate per entry *)
+              LvarS.fold (fun ((n, _) as lvar) yaml_entries' ->
                   let d = LHT.find lh lvar in
                   let fd = Node.find_fundec n in
                   let vars = fd.sformals @ fd.slocals @ global_vars in
@@ -243,23 +262,58 @@ struct
                     if Check.checkStandaloneExp ~vars inv_exp then (
                       match ask_local lvar d (Queries.EvalInt inv_exp) with
                       | x when Queries.ID.is_bool x ->
-                        if Option.get (Queries.ID.to_bool x) then
+                        let b = Option.get (Queries.ID.to_bool x) in
+                        if b then
                           M.success ~category:Witness ~loc "invariant confirmed: %s" inv
                         else
-                          M.error ~category:Witness ~loc "invariant refuted: %s" inv
+                          M.error ~category:Witness ~loc "invariant refuted: %s" inv;
+                        let yaml_metadata = Yaml.Util.(yaml_entry |> find_exn "metadata" |> Option.get) in
+                        let uuid = Yaml.Util.(yaml_metadata |> find_exn "uuid" |> Option.get |> to_string_exn) in
+                        let certificate_uuid = Uuidm.v4_gen uuid_random_state () in
+                        let certificate_entry = `O [
+                            ("entry_type", `String "loop_invariant_certificate");
+                            ("metadata", `O [
+                                ("format_version", `String "0.1");
+                                ("uuid", `String (Uuidm.to_string certificate_uuid));
+                                ("creation_time", yaml_creation_time);
+                                ("producer", yaml_producer);
+                              ]);
+                            ("target", `O [
+                                ("uuid", `String uuid);
+                                ("type", `String "loop_invariant"); (* TODO: check *)
+                                ("file_hash", `String (sha256_file loc.file));
+                              ]);
+                            ("certification", `O [
+                                ("string", `String (if b then "confirmed" else "rejected"));
+                                ("type", `String "verdict");
+                                ("format", `String "confirmed | rejected");
+                              ]);
+                          ]
+                        in
+                        certificate_entry :: yaml_entry :: yaml_entries'
                       | _ ->
-                        M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv
+                        M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv;
+                        yaml_entry :: yaml_entries'
+                    )
+                    else (
+                      M.error ~category:Witness ~loc "broken CIL expression invariant: %s (%a)" inv Cil.d_plainexp inv_exp;
+                      yaml_entry :: yaml_entries'
                     )
-                    else
-                      M.error ~category:Witness ~loc "broken CIL expression invariant: %s (%a)" inv Cil.d_plainexp inv_exp
                   | None ->
-                    M.error ~category:Witness ~loc "CIL couldn't parse invariant: %s" inv
-                ) lvars
+                    M.error ~category:Witness ~loc "CIL couldn't parse invariant: %s" inv;
+                    yaml_entry :: yaml_entries'
+                ) lvars yaml_entries'
             | None ->
-              M.warn ~category:Witness ~loc "couldn't locate invariant: %s" inv
+              M.warn ~category:Witness ~loc "couldn't locate invariant: %s" inv;
+              yaml_entry :: yaml_entries'
           end
         | exception Frontc.ParseError _ ->
           Errormsg.log "\n"; (* CIL prints garbage without \n before *)
-          M.error ~category:Witness ~loc "Frontc couldn't parse invariant: %s" inv
-      ) yaml_entries
+          M.error ~category:Witness ~loc "Frontc couldn't parse invariant: %s" inv;
+          yaml_entry :: yaml_entries'
+      ) [] yaml_entries
+    in
+
+    let yaml' = `A (List.rev yaml_entries') in
+    Yaml_unix.to_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.certificate")) yaml'
 end

From eb371f53c7e7b9c53283e1e4d10e9c6a6374b2f7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 26 May 2022 17:35:36 +0300
Subject: [PATCH 20/24] Deduplicate yaml witness entry creation

---
 src/witness/yamlWitness.ml | 196 ++++++++++++++++++-------------------
 1 file changed, 98 insertions(+), 98 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index bfa250c55d..2a99e5711f 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -2,6 +2,87 @@ open Analyses
 
 let uuid_random_state = Random.State.make_self_init ()
 
+let sha256_file f = Sha256.(to_hex (file f))
+let sha256_file_cache = BatCache.make_ht ~gen:sha256_file ~init_size:5
+let sha256_file = sha256_file_cache.get
+
+module Entry =
+struct
+  (* yaml_conf is too verbose *)
+  (* let yaml_conf: Yaml.value = Json_repr.convert (module Json_repr.Yojson) (module Json_repr.Ezjsonm) (!GobConfig.json_conf) in *)
+  let yaml_producer = `O [
+      ("name", `String "Goblint");
+      ("version", `String Version.goblint);
+      (* TODO: configuration *)
+      (* ("configuration", yaml_conf); *) (* yaml_conf is too verbose *)
+      ("command_line", `String Goblintutil.command_line);
+      (* TODO: description *)
+    ]
+
+  let yaml_metadata ?(extra=[]) () =
+    let uuid = Uuidm.v4_gen uuid_random_state () in
+    let creation_time = TimeUtil.iso8601_now () in
+    `O ([
+        ("format_version", `String "0.1");
+        ("uuid", `String (Uuidm.to_string uuid));
+        ("creation_time", `String creation_time);
+        ("producer", yaml_producer);
+      ] @ extra)
+
+  let yaml_task ~input_files ~data_model ~specification =
+    `O ([
+        ("input_files", `A (List.map Yaml.Util.string input_files));
+        ("input_file_hashes", `O (List.map (fun file ->
+             (file, `String (sha256_file file))
+           ) input_files));
+        ("data_model", `String data_model);
+        ("language", `String "C");
+      ] @ match specification with
+      | Some specification -> [
+          ("specification", `String specification)
+        ]
+      | None ->
+        []
+      )
+
+  let yaml_loop_invariant ~yaml_task ~location:(loc:Cil.location) ~location_function ~invariant =
+    `O [
+      ("entry_type", `String "loop_invariant");
+      ("metadata", yaml_metadata ~extra:[
+          ("task", yaml_task);
+        ] ());
+      ("location", `O [
+          ("file_name", `String loc.file);
+          ("file_hash", `String (sha256_file loc.file));
+          ("line", `Float (float_of_int loc.line));
+          ("column", `Float (float_of_int (loc.column - 1)));
+          ("function", `String location_function);
+        ]);
+      ("loop_invariant", `O [
+          ("string", `String invariant);
+          ("type", `String "assertion");
+          ("format", `String "C");
+        ]);
+    ]
+
+  let yaml_loop_invariant_certificate ~target_uuid ~target_file_name ~verdict =
+    `O [
+      ("entry_type", `String "loop_invariant_certificate");
+      ("metadata", yaml_metadata ());
+      ("target", `O [
+          ("uuid", `String target_uuid);
+          ("type", `String "loop_invariant"); (* TODO: check *)
+          ("file_hash", `String (sha256_file target_file_name));
+        ]);
+      ("certification", `O [
+          ("string", `String (if verdict then "confirmed" else "rejected"));
+          ("type", `String "verdict");
+          ("format", `String "confirmed | rejected");
+        ]);
+    ]
+end
+
+
 module Make
     (File: WitnessUtil.File)
     (Cfg: MyCFG.CfgBidir)
@@ -27,40 +108,17 @@ struct
     nh
 
   let write lh gh =
-    (* yaml_conf is too verbose *)
-    (* let yaml_conf: Yaml.value = Json_repr.convert (module Json_repr.Yojson) (module Json_repr.Ezjsonm) (!GobConfig.json_conf) in *)
-    let yaml_creation_time = `String (TimeUtil.iso8601_now ()) in
-    let yaml_producer = `O [
-        ("name", `String "Goblint");
-        ("version", `String Version.goblint);
-        (* TODO: configuration *)
-        (* ("configuration", yaml_conf); *) (* yaml_conf is too verbose *)
-        ("command_line", `String Goblintutil.command_line);
-        (* TODO: description *)
-      ]
+    let input_files = GobConfig.get_string_list "files" in
+    let data_model = match GobConfig.get_string "exp.architecture" with
+      | "64bit" -> "LP64"
+      | "32bit" -> "ILP32"
+      | _ -> failwith "invalid architecture"
     in
-    let files = GobConfig.get_string_list "files" in
-    let sha256_file f = Sha256.(to_hex (file f)) in
-    let sha256_file_cache = BatCache.make_ht ~gen:sha256_file ~init_size:5 in
-    let sha256_file = sha256_file_cache.get in
-    let yaml_task = `O ([
-        ("input_files", `A (List.map Yaml.Util.string files));
-        ("input_file_hashes", `O (List.map (fun file ->
-             (file, `String (sha256_file file))
-           ) files));
-        ("data_model", `String (match GobConfig.get_string "exp.architecture" with
-             | "64bit" -> "LP64"
-             | "32bit" -> "ILP32"
-             | _ -> failwith "invalid architecture"));
-        ("language", `String "C");
-      ] @ match !Svcomp.task with
-      | Some (module Task) -> [
-          ("specification", `String (Svcomp.Specification.to_string Task.specification))
-        ]
-      | None ->
-        []
-      )
+    let specification = Option.map (fun (module Task: Svcomp.Task) ->
+        Svcomp.Specification.to_string Task.specification
+      ) !Svcomp.task
     in
+    let yaml_task = Entry.yaml_task ~input_files ~data_model ~specification in
 
     let nh = join_contexts lh in
 
@@ -80,30 +138,9 @@ struct
               let loc = Node.location n in
               let invs = WitnessUtil.InvariantExp.process_exp inv in
               List.fold_left (fun acc inv ->
-                  let uuid = Uuidm.v4_gen uuid_random_state () in
-                  let entry = `O [
-                      ("entry_type", `String "loop_invariant");
-                      ("metadata", `O [
-                          ("format_version", `String "0.1");
-                          ("uuid", `String (Uuidm.to_string uuid));
-                          ("creation_time", yaml_creation_time);
-                          ("producer", yaml_producer);
-                          ("task", yaml_task);
-                        ]);
-                      ("location", `O [
-                          ("file_name", `String loc.file);
-                          ("file_hash", `String (sha256_file loc.file));
-                          ("line", `Float (float_of_int loc.line));
-                          ("column", `Float (float_of_int (loc.column - 1)));
-                          ("function", `String (Node.find_fundec n).svar.vname);
-                        ]);
-                      ("loop_invariant", `O [
-                          ("string", `String (CilType.Exp.show inv));
-                          ("type", `String "assertion");
-                          ("format", `String "C");
-                        ]);
-                    ]
-                  in
+                  let location_function = (Node.find_fundec n).svar.vname in
+                  let invariant = CilType.Exp.show inv in
+                  let entry = Entry.yaml_loop_invariant ~yaml_task ~location:loc ~location_function ~invariant in
                   entry :: acc
                 ) acc invs
             | None ->
@@ -177,24 +214,9 @@ struct
       | _ -> failwith "invalid YAML"
     in
 
-    (* TODO: deduplicate *)
-    (* yaml_conf is too verbose *)
-    (* let yaml_conf: Yaml.value = Json_repr.convert (module Json_repr.Yojson) (module Json_repr.Ezjsonm) (!GobConfig.json_conf) in *)
-    let yaml_creation_time = `String (TimeUtil.iso8601_now ()) in
-    let yaml_producer = `O [
-        ("name", `String "Goblint");
-        ("version", `String Version.goblint);
-        (* TODO: configuration *)
-        (* ("configuration", yaml_conf); *) (* yaml_conf is too verbose *)
-        ("command_line", `String Goblintutil.command_line);
-        (* TODO: description *)
-      ]
-    in
-    let sha256_file f = Sha256.(to_hex (file f)) in
-    let sha256_file_cache = BatCache.make_ht ~gen:sha256_file ~init_size:5 in
-    let sha256_file = sha256_file_cache.get in
-
     let yaml_entries' = List.fold_left (fun yaml_entries' yaml_entry ->
+        let yaml_metadata = Yaml.Util.(yaml_entry |> find_exn "metadata" |> Option.get) in
+        let uuid = Yaml.Util.(yaml_metadata |> find_exn "uuid" |> Option.get |> to_string_exn) in
         let yaml_location = Yaml.Util.(yaml_entry |> find_exn "location" |> Option.get) in
         let file = Yaml.Util.(yaml_location |> find_exn "file_name" |> Option.get |> to_string_exn) in
         let line = Yaml.Util.(yaml_location |> find_exn "line" |> Option.get |> to_float_exn |> int_of_float) in
@@ -262,34 +284,12 @@ struct
                     if Check.checkStandaloneExp ~vars inv_exp then (
                       match ask_local lvar d (Queries.EvalInt inv_exp) with
                       | x when Queries.ID.is_bool x ->
-                        let b = Option.get (Queries.ID.to_bool x) in
-                        if b then
+                        let verdict = Option.get (Queries.ID.to_bool x) in
+                        if verdict then
                           M.success ~category:Witness ~loc "invariant confirmed: %s" inv
                         else
                           M.error ~category:Witness ~loc "invariant refuted: %s" inv;
-                        let yaml_metadata = Yaml.Util.(yaml_entry |> find_exn "metadata" |> Option.get) in
-                        let uuid = Yaml.Util.(yaml_metadata |> find_exn "uuid" |> Option.get |> to_string_exn) in
-                        let certificate_uuid = Uuidm.v4_gen uuid_random_state () in
-                        let certificate_entry = `O [
-                            ("entry_type", `String "loop_invariant_certificate");
-                            ("metadata", `O [
-                                ("format_version", `String "0.1");
-                                ("uuid", `String (Uuidm.to_string certificate_uuid));
-                                ("creation_time", yaml_creation_time);
-                                ("producer", yaml_producer);
-                              ]);
-                            ("target", `O [
-                                ("uuid", `String uuid);
-                                ("type", `String "loop_invariant"); (* TODO: check *)
-                                ("file_hash", `String (sha256_file loc.file));
-                              ]);
-                            ("certification", `O [
-                                ("string", `String (if b then "confirmed" else "rejected"));
-                                ("type", `String "verdict");
-                                ("format", `String "confirmed | rejected");
-                              ]);
-                          ]
-                        in
+                        let certificate_entry = Entry.yaml_loop_invariant_certificate ~target_uuid:uuid ~target_file_name:loc.file ~verdict in
                         certificate_entry :: yaml_entry :: yaml_entries'
                       | _ ->
                         M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv;

From f2ff5f981b94e55fed09481dbc717e32cc3a27f2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 26 May 2022 18:13:06 +0300
Subject: [PATCH 21/24] Aggregate yaml witness invariant results over lvars

---
 src/witness/yamlWitness.ml | 82 ++++++++++++++++++++++++++------------
 1 file changed, 56 insertions(+), 26 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 2a99e5711f..3e148a6de3 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -156,6 +156,24 @@ struct
 end
 
 
+module ValidationResult =
+struct
+  (* constructor order is important for the chain lattice *)
+  type result =
+    | Confirmed
+    | Unconfirmed
+    | Refuted
+    | ParseError
+  [@@deriving enum, show]
+
+  module ChainParams =
+  struct
+    let n = max_result - 1
+    let names i = show_result (Option.get (result_of_enum i))
+  end
+  include Lattice.Chain (ChainParams)
+end
+
 module Validator
     (Spec : Spec)
     (EQSys : GlobConstrSys with module LVar = VarF (Spec.C)
@@ -252,8 +270,9 @@ struct
 
           begin match lvars_opt with
             | Some lvars ->
-              (* TODO: only one certificate per entry *)
-              LvarS.fold (fun ((n, _) as lvar) yaml_entries' ->
+              let module VR = ValidationResult in
+
+              let result = LvarS.fold (fun ((n, _) as lvar) (acc: VR.t) ->
                   let d = LHT.find lh lvar in
                   let fd = Node.find_fundec n in
                   let vars = fd.sformals @ fd.slocals @ global_vars in
@@ -279,30 +298,40 @@ struct
                       )
                   in
 
-                  match inv_exp_opt with
-                  | Some inv_exp ->
-                    if Check.checkStandaloneExp ~vars inv_exp then (
-                      match ask_local lvar d (Queries.EvalInt inv_exp) with
-                      | x when Queries.ID.is_bool x ->
-                        let verdict = Option.get (Queries.ID.to_bool x) in
-                        if verdict then
-                          M.success ~category:Witness ~loc "invariant confirmed: %s" inv
-                        else
-                          M.error ~category:Witness ~loc "invariant refuted: %s" inv;
-                        let certificate_entry = Entry.yaml_loop_invariant_certificate ~target_uuid:uuid ~target_file_name:loc.file ~verdict in
-                        certificate_entry :: yaml_entry :: yaml_entries'
-                      | _ ->
-                        M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv;
-                        yaml_entry :: yaml_entries'
-                    )
-                    else (
-                      M.error ~category:Witness ~loc "broken CIL expression invariant: %s (%a)" inv Cil.d_plainexp inv_exp;
-                      yaml_entry :: yaml_entries'
-                    )
-                  | None ->
-                    M.error ~category:Witness ~loc "CIL couldn't parse invariant: %s" inv;
-                    yaml_entry :: yaml_entries'
-                ) lvars yaml_entries'
+                  let result: VR.result = match inv_exp_opt with
+                    | Some inv_exp when Check.checkStandaloneExp ~vars inv_exp ->
+                      begin match ask_local lvar d (Queries.EvalInt inv_exp) with
+                        | x when Queries.ID.is_bool x ->
+                          let verdict = Option.get (Queries.ID.to_bool x) in
+                          if verdict then
+                            Confirmed
+                          else
+                            Refuted
+                        | _ ->
+                          Unconfirmed
+                      end
+                    | _ ->
+                      ParseError
+                  in
+                  VR.join acc (VR.result_to_enum result)
+                ) lvars (VR.bot ())
+              in
+
+              begin match Option.get (VR.result_of_enum result) with
+                | Confirmed ->
+                  M.success ~category:Witness ~loc "invariant confirmed: %s" inv;
+                  let certificate_entry = Entry.yaml_loop_invariant_certificate ~target_uuid:uuid ~target_file_name:loc.file ~verdict:true in
+                  certificate_entry :: yaml_entry :: yaml_entries'
+                | Unconfirmed ->
+                  M.warn ~category:Witness ~loc "invariant unconfirmed: %s" inv;yaml_entry :: yaml_entries'
+                | Refuted ->
+                  M.error ~category:Witness ~loc "invariant refuted: %s" inv;let certificate_entry = Entry.yaml_loop_invariant_certificate ~target_uuid:uuid ~target_file_name:loc.file ~verdict:false in
+                  certificate_entry :: yaml_entry :: yaml_entries'
+                | ParseError ->
+                  M.error ~category:Witness ~loc "CIL couldn't parse invariant: %s" inv;
+                  M.info ~category:Witness ~loc "invariant has undefined variables or side effects: %s" inv;
+                  yaml_entry :: yaml_entries'
+              end
             | None ->
               M.warn ~category:Witness ~loc "couldn't locate invariant: %s" inv;
               yaml_entry :: yaml_entries'
@@ -310,6 +339,7 @@ struct
         | exception Frontc.ParseError _ ->
           Errormsg.log "\n"; (* CIL prints garbage without \n before *)
           M.error ~category:Witness ~loc "Frontc couldn't parse invariant: %s" inv;
+          M.info ~category:Witness ~loc "invariant has invalid syntax: %s" inv;
           yaml_entry :: yaml_entries'
       ) [] yaml_entries
     in

From a4937cf09b9631edca3477488bd654061b24daa4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 27 May 2022 11:18:41 +0300
Subject: [PATCH 22/24] Revert "Use bot instead of top for base mutex contents"

This reverts commit 1fa8d17ffa46849911da243b741d34c2a89f19d3.
---
 src/cdomains/valueDomain.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index fe80c82603..74bc322f6e 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -135,7 +135,7 @@ struct
 
   let rec init_value (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *)
     match t with
-    | t when is_mutex_type t -> `Bot (* use `Bot instead of `Top to avoid unknown value escape warnings *)
+    | t when is_mutex_type t -> `Top
     | TInt (ik,_) -> `Int (ID.top_of ik)
     | TPtr _ -> `Address AD.top_ptr
     | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> init_value fd.ftype) ci)
@@ -855,8 +855,7 @@ struct
       let mu = function `Blob (`Blob (y, s', orig), s, orig2) -> `Blob (y, ID.join s s',orig) | x -> x in
       let r =
       match x, offs with
-      | _, _ when is_mutex_type t -> (* hide mutex structure contents, not updated anyway *)
-        `Bot (* use `Bot instead of `Top to avoid unknown value escape warnings *)
+      | _, _ when is_mutex_type t -> `Top (* hide mutex structure contents, not updated anyway *)
       | `Blob (x,s,orig), `Index (_,ofs) ->
         begin
           let l', o' = shift_one_over l o in

From 4bc3f35fc2912c37359b111c23ea8e1145499733 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 27 May 2022 11:18:51 +0300
Subject: [PATCH 23/24] Revert "Hide mutex structure contents in base analysis"

This reverts commit 3841fe79e0957bae0b59f00a7dcd4508e5cc3278.
---
 src/cdomains/valueDomain.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index 74bc322f6e..ee1b0f1740 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -855,7 +855,6 @@ struct
       let mu = function `Blob (`Blob (y, s', orig), s, orig2) -> `Blob (y, ID.join s s',orig) | x -> x in
       let r =
       match x, offs with
-      | _, _ when is_mutex_type t -> `Top (* hide mutex structure contents, not updated anyway *)
       | `Blob (x,s,orig), `Index (_,ofs) ->
         begin
           let l', o' = shift_one_over l o in

From 8b2cccf7e43a2cd8da890435aead4182cbf6b2bd Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 30 May 2022 10:19:47 +0300
Subject: [PATCH 24/24] Update CIL opam pin

---
 goblint.opam          | 2 +-
 goblint.opam.locked   | 2 +-
 goblint.opam.template | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index a1ffc3d048..986258fbf4 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -68,7 +68,7 @@ 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!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#fe7da7b4203735d84670e68f3044a9bf33bd6e65" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#0a37478e08b9ae10587b0355ad2805dfeca1cca9" ]
   # 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" ]
   # quoter workaround reverted for release, so no pin needed
diff --git a/goblint.opam.locked b/goblint.opam.locked
index adf761e3c8..b68b488a0d 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -124,7 +124,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#fe7da7b4203735d84670e68f3044a9bf33bd6e65"
+    "git+https://github.com/goblint/cil.git#0a37478e08b9ae10587b0355ad2805dfeca1cca9"
   ]
   [
     "apron.v0.9.13"
diff --git a/goblint.opam.template b/goblint.opam.template
index 0ba278543a..c354675c4f 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#fe7da7b4203735d84670e68f3044a9bf33bd6e65" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#0a37478e08b9ae10587b0355ad2805dfeca1cca9" ]
   # 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" ]
   # quoter workaround reverted for release, so no pin needed