From 98bf2b5c4655722e5a1f451bdf7ebf1a0a9f3b49 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Mon, 19 Jun 2023 18:35:36 +0200
Subject: [PATCH 01/19] avoid truncation of very large integers

---
 src/framework/cfgTools.ml | 2 +-
 src/util/cilfacade.ml     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index 8f98a48e84..85a1c73732 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -123,7 +123,7 @@ let rec pretty_edges () = function
   | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs
 
 let get_pseudo_return_id fd =
-  let start_id = 10_000_000_000 in (* TODO get max_sid? *)
+  let start_id = 1_000_000_000 in (* TODO get max_sid? *)
   let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
   if sid < start_id then sid + start_id else sid
 
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 09231b4f45..6d48770a50 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -9,7 +9,7 @@ include Cilfacade0
 (** Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method *)
 let create_var (var: varinfo) =
   (* TODO Hack: this offset should preempt conflicts with ids generated by CIL *)
-  let start_id = 10_000_000_000 in
+  let start_id = 1_000_000_000 in
   let hash = Hashtbl.hash { var with vid = 0 } in
   let hash = if hash < start_id then hash + start_id else hash in
   { var with vid = hash }

From 1fa71e1021902611a63f15e6f5296aabf440e6d2 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Wed, 21 Jun 2023 16:08:12 +0200
Subject: [PATCH 02/19] allow syntactic queries (no expression field) through
 Goblint

---
 src/transform/expressionEvaluation.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml
index 815e5742f6..56e73d815f 100644
--- a/src/transform/expressionEvaluation.ml
+++ b/src/transform/expressionEvaluation.ml
@@ -17,7 +17,7 @@ type query =
     structure : (CodeQuery.structure [@default None_s]);
     limitation : (CodeQuery.constr [@default None_c]);
 
-    expression : string;
+    expression : (string option [@default None]);
     mode : [ `Must | `May ];
 
   } [@@deriving yojson]
@@ -191,8 +191,8 @@ struct
         |> List.group file_compare
         (* Sort, remove duplicates, ungroup *)
         |> List.concat_map (fun ls -> List.sort_uniq byte_compare ls)
-        (* Semantic queries *)
-        |> List.map (fun (n, l, s, i) -> ((n, l, s, i), evaluator#evaluate l query.expression))
+        (* Semantic queries if query.expression is some *)
+        |> List.map (fun (n, l, s, i) -> ((n, l, s, i), Option.map_default (evaluator#evaluate l) (Some true) query.expression))
       in
       let print ((_, loc, _, _), res) =
         match res with

From b6ac9e05e1920e6c997fc9125a4ba35cdcdcd94e Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Thu, 22 Jun 2023 11:08:48 +0200
Subject: [PATCH 03/19] use negative ids for varinfos generated by Goblint and
 pseudo return nodes

---
 src/framework/cfgTools.ml | 4 +---
 src/util/cilfacade.ml     | 6 ++----
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index 85a1c73732..f12dfbb590 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -123,9 +123,7 @@ let rec pretty_edges () = function
   | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs
 
 let get_pseudo_return_id fd =
-  let start_id = 1_000_000_000 in (* TODO get max_sid? *)
-  let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
-  if sid < start_id then sid + start_id else sid
+  - (Hashtbl.hash fd.svar.vid) (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
 
 let node_scc_global = NH.create 113
 
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 6d48770a50..b8d0aba906 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -8,11 +8,9 @@ include Cilfacade0
 
 (** Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method *)
 let create_var (var: varinfo) =
-  (* TODO Hack: this offset should preempt conflicts with ids generated by CIL *)
-  let start_id = 1_000_000_000 in
+  (* Hack: using negative integers should preempt conflicts with ids generated by CIL *)
   let hash = Hashtbl.hash { var with vid = 0 } in
-  let hash = if hash < start_id then hash + start_id else hash in
-  { var with vid = hash }
+  { var with vid = - hash }
 
 
 (** Is character type (N1570 6.2.5.15)? *)

From 11ab2274d2e471d22249c7a2300f2236ba0d988d Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Mon, 26 Jun 2023 16:07:58 +0200
Subject: [PATCH 04/19] add test cases for syntactic and semantic search in
 GobView

---
 scripts/test-gobview.py | 66 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)

diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py
index 0dc2cacaa4..5f6e3472d3 100644
--- a/scripts/test-gobview.py
+++ b/scripts/test-gobview.py
@@ -62,6 +62,72 @@ class Server(socketserver.TCPServer):
     panel = browser.find_element(By.CLASS_NAME, "panel")
     print("found DOM elements main, sidebar-left, sidebar-right, content and panel")
 
+    # test syntactic search
+    leftS.find_element(By.LINK_TEXT,  "Search").click()
+    leftS.find_element(By.CLASS_NAME, "switch-to-json").click()
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","fail"],"find":["uses"],"mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("syntactic search for variable use of 'fail' found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 2)
+    assert("tests/regression/00-sanity/01-assert.c:7" in locations)
+    assert("tests/regression/00-sanity/01-assert.c:12" in locations)
+
+    # clear results
+    leftS.find_element(By.CLASS_NAME, "clear-btn").click()
+
+    # test semantic search 1
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","success"],"find":["uses"],"expression":"success == 1","mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("semantic search for variable use of 'success' where it must be 1 found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 2)
+    assert("tests/regression/00-sanity/01-assert.c:10" in locations)
+    assert("tests/regression/00-sanity/01-assert.c:5" in locations)
+
+    # clear results
+    leftS.find_element(By.CLASS_NAME, "clear-btn").click()
+
+    # test semantic search 2
+    textfield = leftS.find_element(By.CLASS_NAME, "form-control")
+    textfield.clear()
+    textfield.send_keys('{"kind":["var"],"target":["name","success"],"find":["uses"],"expression":"success == 0","mode":["Must"]}')
+    leftS.find_element(By.CLASS_NAME, "exec-button").click()
+    results = leftS.find_elements(By.CLASS_NAME, "list-group-item")
+    locations = []
+    for r in results:
+        for tr in r.find_elements(By.TAG_NAME, "tr"):
+            if tr.find_element(By.TAG_NAME, "th").text == "Location":
+                locations.insert(0,tr.find_element(By.TAG_NAME, "td").find_element(By.TAG_NAME, "a").text)
+
+    print("semantic search for variable use of 'success' where it must be 0 found", len(results), "results")
+    for l in locations:
+        print(l)
+    assert(len(results) == 0)
+
+    # close "No results found" alert
+    leftS.find_element(By.CLASS_NAME, "btn-close").click()
+
     cleanup(browser, httpd, thread)
 
 except Exception as e:

From 2b47ef1ec9cac53efb89738a88b3ceb811d6ec07 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Tue, 27 Jun 2023 19:30:36 +0200
Subject: [PATCH 05/19] allow for semantic search expressions with function
 pointers and function parameters

---
 src/transform/expressionEvaluation.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml
index 56e73d815f..bde704f0c9 100644
--- a/src/transform/expressionEvaluation.ml
+++ b/src/transform/expressionEvaluation.ml
@@ -60,7 +60,11 @@ struct
 
       val global_variables =
         file.globals
-        |> List.filter_map (function Cil.GVar (v, _, _) -> Some (v.vname, Cil.Fv v) | _ -> None)
+        |> List.filter_map (function
+            | Cil.GVar (v, _, _) -> Some (v.vname, Cil.Fv v)
+            | Cil.GFun (f, l) -> Some (f.svar.vname, Cil.Fv f.svar)
+            | Cil.GVarDecl (v, l) -> Some (v.vname, Cil.Fv v)
+            | _ -> None)
       val statements =
         file.globals
         |> List.filter_map (function Cil.GFun (f, _) -> Some f | _ -> None)
@@ -77,7 +81,7 @@ struct
         (* Compute the available local variables *)
         let local_variables =
           match Hashtbl.find_option statements location with
-          | Some (function_definition, _) -> function_definition.slocals |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v)
+          | Some (fd, _) -> fd.slocals @ fd.sformals |> List.map (fun (v : Cil.varinfo) -> v.vname, Cil.Fv v)
           | None -> []
         in
         (* Parse expression *)

From 20c500fbec6504204a30e824916768105f3d9a18 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 24 Jan 2024 13:24:55 +0200
Subject: [PATCH 06/19] Exclude Goblint stubs from YAML witnesses

---
 src/witness/yamlWitness.ml | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 253ee5eecd..b7ec584dfb 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -193,15 +193,25 @@ struct
     in
     let task = Entry.task ~input_files ~data_model ~specification in
 
+    let is_stub_node n =
+      let fundec = Node.find_fundec n in
+      Cil.hasAttribute "goblint_stub" fundec.svar.vattr
+    in
+
     let is_invariant_node (n : Node.t) =
       let loc = Node.location n in
       match n with
-      | Statement _ when not loc.synthetic && WitnessInvariant.is_invariant_node n -> true
+      | Statement _ when not loc.synthetic && WitnessInvariant.is_invariant_node n ->
+        not (is_stub_node n)
       | _ ->
         (* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *)
         false
     in
 
+    let is_loop_head_node n =
+      WitnessUtil.NH.mem WitnessInvariant.loop_heads n && not (is_stub_node n)
+    in
+
     let local_lvals n local =
       if GobConfig.get_bool "witness.invariant.accessed" then (
         match R.ask_local_node n ~local MayAccessed with
@@ -277,7 +287,7 @@ struct
     let entries =
       if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then (
         LH.fold (fun loc ns acc ->
-            if WitnessInvariant.emit_loop_head && List.exists (WitnessUtil.NH.mem WitnessInvariant.loop_heads) ns then (
+            if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then (
               let inv = List.fold_left (fun acc n ->
                   let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
                   Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
@@ -472,7 +482,7 @@ struct
         let invariants =
           if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then (
             LH.fold (fun loc ns acc ->
-                if WitnessInvariant.emit_loop_head && List.exists (WitnessUtil.NH.mem WitnessInvariant.loop_heads) ns then (
+                if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then (
                   let inv = List.fold_left (fun acc n ->
                       let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
                       Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)

From c2d6c6752b43bb2dd9de5f9d2c5aabe9db7a8ea5 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Fri, 26 Jan 2024 13:27:05 +0100
Subject: [PATCH 07/19] use function id instead of (possibly negative) hash

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

diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index f12dfbb590..2555295902 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -123,7 +123,7 @@ let rec pretty_edges () = function
   | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs
 
 let get_pseudo_return_id fd =
-  - (Hashtbl.hash fd.svar.vid) (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
+  - fd.svar.vid (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
 
 let node_scc_global = NH.create 113
 

From 0cc39e2a3c60148b9339313e85d0e222dd1e22e0 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 28 Jan 2024 19:12:55 +0100
Subject: [PATCH 08/19] Handle LNot for float in forward evaluation and
 refinement

---
 src/analyses/base.ml                 |  7 +++---
 src/analyses/baseInvariant.ml        | 36 +++++++++++++++++++---------
 tests/regression/57-floats/22-lnot.c | 26 ++++++++++++++++++++
 3 files changed, 55 insertions(+), 14 deletions(-)
 create mode 100644 tests/regression/57-floats/22-lnot.c

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 42e43b623a..28e5d87c50 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -178,14 +178,15 @@ struct
     | LNot -> ID.lognot
 
   let unop_FD = function
-    | Neg  -> FD.neg
+    | Neg  -> (fun v -> (Float (FD.neg v):value))
+    | LNot -> (fun c -> Int (FD.eq c (FD.of_const (FD.get_fkind c) 0.)))
     (* other unary operators are not implemented on float values *)
-    | _ -> (fun c -> FD.top_of (FD.get_fkind c))
+    | _ -> (fun c -> Float (FD.top_of (FD.get_fkind c)))
 
   (* Evaluating Cil's unary operators. *)
   let evalunop op typ: value -> value = function
     | Int v1 -> Int (ID.cast_to (Cilfacade.get_ikind typ) (unop_ID op v1))
-    | Float v -> Float (unop_FD op v)
+    | Float v -> unop_FD op v
     | Address a when op = LNot ->
       if AD.is_null a then
         Int (ID.of_bool (Cilfacade.get_ikind typ) true)
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index e66a431ccf..7a3d5de806 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -568,17 +568,31 @@ struct
       else
         match exp, c_typed with
         | UnOp (LNot, e, _), Int c ->
-          let ikind = Cilfacade.get_ikind_exp e in
-          let c' =
-            match ID.to_bool (unop_ID LNot c) with
-            | Some true ->
-              (* i.e. e should evaluate to [1,1] *)
-              (* LNot x is 0 for any x != 0 *)
-              ID.of_excl_list ikind [BI.zero]
-            | Some false -> ID.of_bool ikind false
-            | _ -> ID.top_of ikind
-          in
-          inv_exp (Int c') e st
+          (match Cilfacade.typeOf e with
+           | TInt  _ | TPtr _ ->
+             let ikind = Cilfacade.get_ikind_exp e in
+             let c' =
+               match ID.to_bool (unop_ID LNot c) with
+               | Some true ->
+                 (* i.e. e should evaluate to [1,1] *)
+                 (* LNot x is 0 for any x != 0 *)
+                 ID.of_excl_list ikind [BI.zero]
+               | Some false -> ID.of_bool ikind false
+               | _ -> ID.top_of ikind
+             in
+             inv_exp (Int c') e st
+           | TFloat(fkind, _) when ID.to_bool (unop_ID LNot c) = Some false ->
+             (* C99 §6.5.3.3/5 *)
+             (* The result of the logical negation operator ! is 0 if the value of its operand compares *)
+             (* unequal to 0, 1 if the value of its operand compares equal to 0. The result has type int. *)
+             (* The expression !E is equivalent to (0==E). *)
+             (* NaN compares unequal to 0 so no problems *)
+             (* We do not have exclusions for floats, so we do not bother here with the other case *)
+             let zero_float = FD.of_const fkind 0. in
+             inv_exp (Float zero_float) e st
+           | _ -> st
+
+          )
         | UnOp (Neg, e, _), Float c -> inv_exp (Float (unop_FD Neg c)) e st
         | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st
         (* no equivalent for Float, as VD.is_safe_cast fails for all float types anyways *)
diff --git a/tests/regression/57-floats/22-lnot.c b/tests/regression/57-floats/22-lnot.c
new file mode 100644
index 0000000000..5c043e4ead
--- /dev/null
+++ b/tests/regression/57-floats/22-lnot.c
@@ -0,0 +1,26 @@
+//PARAM: --enable ana.float.interval
+#include<goblint.h>
+int main() {
+  float x = 0.0f;
+  int z = !x; 
+
+  int reach;
+
+  if(z) {
+    __goblint_check(1); //Reachable
+    reach = 1;
+  } else {
+    reach = 0;
+  }
+
+  __goblint_check(reach == 1);
+
+  float y;
+  if (!y) {
+    __goblint_check(y == 0.0f);
+  } else {
+    __goblint_check(1); //Reachable
+  }
+  
+  return 0;
+}
\ No newline at end of file

From 410cb621a74cd8846b366a0ec39cb49c607d1b23 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Mon, 29 Jan 2024 16:28:59 +0100
Subject: [PATCH 09/19] Clean up some relational code.

---
 src/analyses/apron/affineEqualityAnalysis.apron.ml | 8 +-------
 src/cdomains/apron/affineEqualityDomain.apron.ml   | 8 +++-----
 src/cdomains/apron/relationDomain.apron.ml         | 1 -
 3 files changed, 4 insertions(+), 13 deletions(-)

diff --git a/src/analyses/apron/affineEqualityAnalysis.apron.ml b/src/analyses/apron/affineEqualityAnalysis.apron.ml
index ce859d87b7..d4a1e5be2e 100644
--- a/src/analyses/apron/affineEqualityAnalysis.apron.ml
+++ b/src/analyses/apron/affineEqualityAnalysis.apron.ml
@@ -9,16 +9,10 @@ include RelationAnalysis
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
     let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
-    let module RD: RelationDomain.RD =
-    struct
-      module V = AffineEqualityDomain.V
-      include AD
-    end
-    in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct
-      include SpecFunctor (Priv) (RD) (RelationPrecCompareUtil.DummyUtil)
+      include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil)
       let name () = "affeq"
     end
     in
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index ea8a350d3c..dacdce659e 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -26,8 +26,6 @@ module Mpqf = struct
   let hash x = 31 * (Z.hash (get_den x)) + Z.hash (get_num x)
 end
 
-module V = RelationDomain.V
-
 (** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars.
     Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *)
 module VarManagement (Vec: AbstractVector) (Mx: AbstractMatrix)=
@@ -240,7 +238,7 @@ struct
   include VarManagement (Vc) (Mx)
 
   module Bounds = ExpressionBounds (Vc) (Mx)
-
+  module V = RelationDomain.V
   module Convert = SharedFunctions.Convert (V) (Bounds) (struct let allow_global = true end) (SharedFunctions.Tracked)
 
   type var = V.t
@@ -703,9 +701,9 @@ struct
   let unmarshal t = t
 end
 
-module D2(Vc: AbstractVector) (Mx: AbstractMatrix): RelationDomain.S3 with type var = Var.t =
+module D2(Vc: AbstractVector) (Mx: AbstractMatrix): RelationDomain.RD with type var = Var.t =
 struct
   module D =  D (Vc) (Mx)
-  include SharedFunctions.AssertionModule (V) (D)
+  include SharedFunctions.AssertionModule (D.V) (D)
   include D
 end
diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml
index 48720b0382..82e7e20d20 100644
--- a/src/cdomains/apron/relationDomain.apron.ml
+++ b/src/cdomains/apron/relationDomain.apron.ml
@@ -128,7 +128,6 @@ end
 module type S3 =
 sig
   include S2
-
   val cil_exp_of_lincons1: Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end

From eb1ad54e85985a45e66bc31194ac47f2306c7ecd Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Thu, 1 Feb 2024 13:51:37 +0100
Subject: [PATCH 10/19] Avoid intermediate definition of module in
 ApronAnalysis.

---
 src/analyses/apron/apronAnalysis.apron.ml | 11 ++---------
 src/cdomains/apron/apronDomain.apron.ml   |  7 ++++++-
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index 0ba17cdb35..f4d72c3d71 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -9,18 +9,11 @@ let spec_module: (module MCPSpec) Lazy.t =
     let module Man = (val ApronDomain.get_manager ()) in
     let module AD = ApronDomain.D2 (Man) in
     let diff_box = GobConfig.get_bool "ana.apron.invariant.diff-box" in
-    let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): ApronDomain.S3) else (module AD)) in
-    let module RD: RelationDomain.RD =
-    struct
-      module V = ApronDomain.V
-      include AD
-      type var = Apron.Var.t
-    end
-    in
+    let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): RelationDomain.RD) else (module AD)) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct
-      include SpecFunctor (Priv) (RD) (ApronPrecCompareUtil.Util)
+      include SpecFunctor (Priv) (AD) (ApronPrecCompareUtil.Util)
       let name () = "apron"
     end
     in
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index e78176fc41..2b8f360bc5 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -779,6 +779,7 @@ module type S2 =
 (* TODO: ExS3 or better extend RelationDomain.S3 directly?*)
 sig
   module Man: Manager
+  module V: RV
   include module type of AOps (Tracked) (Man)
   include SLattice with type t = Man.mt A.t
 
@@ -803,6 +804,7 @@ sig
   include SLattice
   include AOps with type t := t
 
+  module V: RV
   module Tracked: RelationDomain.Tracked
 
   val assert_inv : t -> exp -> bool -> bool Lazy.t -> t
@@ -813,6 +815,7 @@ end
 module D2 (Man: Manager) : S2 with module Man = Man  =
 struct
   include D (Man)
+  module V = RelationDomain.V
 
   type marshal = OctagonD.marshal
 
@@ -926,8 +929,10 @@ struct
     |> Lincons1Set.elements
 end
 
-module BoxProd (D: S3): S3 =
+module BoxProd (D: S3): RD =
 struct
+  module V = D.V
+  type var = V.t
   module BP0 = BoxProd0 (D)
   module Tracked = SharedFunctions.Tracked
   include BP0

From 7bd3b4f5e60a6e13dac7e3f50eebaad800dc5977 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Thu, 1 Feb 2024 19:15:17 +0100
Subject: [PATCH 11/19] add comment

---
 src/common/util/cilfacade.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index 276f67c78e..6100ab9a3c 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -10,7 +10,7 @@ include Cilfacade0
 let create_var (var: varinfo) =
   (* Hack: using negative integers should preempt conflicts with ids generated by CIL *)
   let hash = Hashtbl.hash { var with vid = 0 } in
-  { var with vid = - hash }
+  { var with vid = - hash } (* Hashtbl.hash returns non-negative integer *)
 
 
 (** Is character type (N1570 6.2.5.15)? *)

From e8da9169411052352c7785eca568dc7e1f81a684 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 2 Feb 2024 14:45:57 +0200
Subject: [PATCH 12/19] Remove trailing whitespace in Base

---
 src/analyses/base.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index c96106b29f..e846536a6d 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -877,9 +877,9 @@ struct
       | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~ctx st (Const (CStr (x,e))) (* TODO safe? *)
       | CastE  (t, exp) ->
         (let v = eval_rv ~ctx st exp in
-         try 
+         try
            VD.cast ~torg:(Cilfacade.typeOf exp) t v
-         with Cilfacade.TypeOfError _  -> 
+         with Cilfacade.TypeOfError _  ->
            VD.cast t v)
       | SizeOf _
       | Real _

From 9f0c940f17c354515f9d41465cc3fbd0de8875c3 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 4 Feb 2024 11:07:16 +0100
Subject: [PATCH 13/19] unop_FD: Handle `BNot` explicitely

---
 src/analyses/base.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 77394a52cd..383c76fad8 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -179,8 +179,8 @@ struct
   let unop_FD = function
     | Neg  -> (fun v -> (Float (FD.neg v):value))
     | LNot -> (fun c -> Int (FD.eq c (FD.of_const (FD.get_fkind c) 0.)))
-    (* other unary operators are not implemented on float values *)
-    | _ -> (fun c -> Float (FD.top_of (FD.get_fkind c)))
+    | BNot -> failwith "BNot on a value of type float!"
+
 
   (* Evaluating Cil's unary operators. *)
   let evalunop op typ: value -> value = function

From c8b2fb7f30357a1efce80df5cba00022f45b74d2 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 4 Feb 2024 11:08:55 +0100
Subject: [PATCH 14/19] Share `eval_unop` definitions between `base.ml` and
 `baseInvariant.ml`

---
 src/analyses/base.ml          |  6 ++++++
 src/analyses/baseInvariant.ml | 15 ++++-----------
 2 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 383c76fad8..63c2879a9a 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1645,6 +1645,9 @@ struct
     module V = V
     module G = G
 
+    let unop_ID = unop_ID
+    let unop_FD = unop_FD
+
     let eval_rv = eval_rv
     let eval_rv_address = eval_rv_address
     let eval_lv = eval_lv
@@ -2842,6 +2845,9 @@ struct
 
           let ost = octx.local
 
+          let unop_ID = unop_ID
+          let unop_FD = unop_FD
+
           (* all evals happen in octx with non-top values *)
           let eval_rv ~ctx st e = eval_rv ~ctx:octx ost e
           let eval_rv_address ~ctx st e = eval_rv_address ~ctx:octx ost e
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 08ec012c10..7154768a75 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -14,6 +14,9 @@ sig
   module V: Analyses.SpecSysVar
   module G: Lattice.S
 
+  val unop_ID: Cil.unop -> ID.t -> ID.t
+  val unop_FD: Cil.unop -> FD.t -> VD.t
+
   val eval_rv: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> VD.t
   val eval_rv_address: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> VD.t
   val eval_lv: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> lval -> AD.t
@@ -41,16 +44,6 @@ module Make (Eval: Eval) =
 struct
   open Eval
 
-  let unop_ID = function
-    | Neg  -> ID.neg
-    | BNot -> ID.lognot
-    | LNot -> ID.c_lognot
-
-  let unop_FD = function
-    | Neg  -> FD.neg
-    (* other unary operators are not implemented on float values *)
-    | _ -> (fun c -> FD.top_of (FD.get_fkind c))
-
   let is_some_bot (x:VD.t) =
     match x with
     | Bot -> false (* HACK: bot is here due to typing conflict (we do not cast appropriately) *)
@@ -589,7 +582,7 @@ struct
              inv_exp (Float zero_float) e st
            | _ -> st
           )
-        | UnOp (Neg, e, _), Float c -> inv_exp (Float (unop_FD Neg c)) e st
+        | UnOp (Neg, e, _), Float c -> inv_exp (unop_FD Neg c) e st
         | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st
         (* no equivalent for Float, as VD.is_safe_cast fails for all float types anyways *)
         | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_safe_cast t2 (Cilfacade.typeOf e2) ->

From d53037a7f56325ee0d117a5ff2ece234021d72aa Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Mon, 5 Feb 2024 15:50:23 +0100
Subject: [PATCH 15/19] update GobView submodule

---
 gobview | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gobview b/gobview
index c8fcb09e9a..7cfdafd2db 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit c8fcb09e9a3e27de22d4803606d5784f667a542a
+Subproject commit 7cfdafd2dbc6715007c5090a621581f454220658

From 7e51d9a0630532bf4930c00f7863fff2fab35cd4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 7 Feb 2024 12:12:57 +0200
Subject: [PATCH 16/19] Refactor is_invariant_node in YamlWitness

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

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index b7ec584dfb..d9d39ccee1 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -201,9 +201,9 @@ struct
     let is_invariant_node (n : Node.t) =
       let loc = Node.location n in
       match n with
-      | Statement _ when not loc.synthetic && WitnessInvariant.is_invariant_node n ->
-        not (is_stub_node n)
-      | _ ->
+      | Statement _ ->
+        not loc.synthetic && WitnessInvariant.is_invariant_node n && not (is_stub_node n)
+      | FunctionEntry _ | Function _ ->
         (* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *)
         false
     in

From a3629c90bd01be7aa0d3129e154cb5ec9b693d01 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 7 Feb 2024 13:01:17 +0200
Subject: [PATCH 17/19] Fix "seq_end failed" crash on YAML witness generation

---
 src/util/std/gobYaml.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/util/std/gobYaml.ml b/src/util/std/gobYaml.ml
index 131daaaebb..624cdbf1fa 100644
--- a/src/util/std/gobYaml.ml
+++ b/src/util/std/gobYaml.ml
@@ -3,7 +3,7 @@ let to_string' ?(len=65535 * 4) ?encoding ?scalar_style ?layout_style v =
   let rec aux len =
     match Yaml.to_string ~len ?encoding ?scalar_style ?layout_style v with
     | Ok _ as o -> o
-    | Error (`Msg ("scalar failed" | "doc_end failed")) when len < Sys.max_string_length / 2 ->
+    | Error (`Msg ("scalar failed" | "doc_end failed" | "seq_end failed")) when len < Sys.max_string_length / 2 ->
       aux (len * 2)
     | Error (`Msg _) as e -> e
   in

From 4957a9fe812b5994579f5de7dde811f6a4a8d99f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 7 Feb 2024 14:44:51 +0200
Subject: [PATCH 18/19] Upgrade mkdocs to 1.5.3

---
 docs/requirements.txt | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/docs/requirements.txt b/docs/requirements.txt
index c86e84d8e8..1936b24f68 100644
--- a/docs/requirements.txt
+++ b/docs/requirements.txt
@@ -1,5 +1,3 @@
 # Python requirements for MkDocs and Read the Docs
 
-mkdocs==1.2.4
-
-jinja2==3.1.3
+mkdocs==1.5.3

From 887ebe0b50ee78aa445cbee5ecbc478b77d67a2c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 8 Feb 2024 13:46:03 +0200
Subject: [PATCH 19/19] Add end locations and synthetic flag to node locations
 in HTML

---
 g2html                          | 2 +-
 src/framework/analysisResult.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/g2html b/g2html
index b18424d114..4b5e1bc630 160000
--- a/g2html
+++ b/g2html
@@ -1 +1 @@
-Subproject commit b18424d114c7838698b4323b49537d8e59faf55f
+Subproject commit 4b5e1bc630f2260ad3f05af557bc65f707af1a6d
diff --git a/src/framework/analysisResult.ml b/src/framework/analysisResult.ml
index 09ece868c1..e53ed37192 100644
--- a/src/framework/analysisResult.ml
+++ b/src/framework/analysisResult.ml
@@ -52,7 +52,7 @@ struct
       (* Not using Node.location here to have updated locations in incremental analysis.
          See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
       let loc = UpdateCil.getLoc n in
-      BatPrintf.fprintf f "<call id=\"%s\" file=\"%s\" line=\"%d\" order=\"%d\" column=\"%d\">\n" (Node.show_id n) loc.file loc.line loc.byte loc.column;
+      BatPrintf.fprintf f "<call id=\"%s\" file=\"%s\" line=\"%d\" order=\"%d\" column=\"%d\" endLine=\"%d\" endColumn=\"%d\" synthetic=\"%B\">\n" (Node.show_id n) loc.file loc.line loc.byte loc.column loc.endLine loc.endColumn loc.synthetic;
       BatPrintf.fprintf f "%a</call>\n" Range.printXml v
     in
     iter print_one xs