From 019227b6c90c391aad9a4e4df8ac6ab769900eaf Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 22 Jan 2025 17:44:25 +0200
Subject: [PATCH 01/11] Move no_overflow from relationAnalysis to
 sharedFunctions

---
 src/analyses/apron/relationAnalysis.apron.ml | 21 ++------------------
 src/analyses/apron/relationPriv.apron.ml     |  2 +-
 src/cdomains/apron/apronDomain.apron.ml      |  2 +-
 src/cdomains/apron/relationDomain.apron.ml   |  2 +-
 src/cdomains/apron/sharedFunctions.apron.ml  | 16 ++++++++++++++-
 5 files changed, 20 insertions(+), 23 deletions(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 3c6b6b14a5..8395a3d233 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -173,25 +173,8 @@ struct
     | _ ->
       st
 
-
-  (** An extended overflow handling inside relationAnalysis for expression assignments when overflows are assumed to occur.
-      Since affine equalities can only keep track of integer bounds of expressions evaluating to definite constants, we now query the integer bounds information for expressions from other analysis.
-      If an analysis returns bounds that are unequal to min and max of ikind , we can exclude the possibility that an overflow occurs and the abstract effect of the expression assignment can be used, i.e. we do not have to set the variable's value to top. *)
-
-  let no_overflow (ask: Queries.ask) exp =
-    match Cilfacade.get_ikind_exp exp with
-    | exception Invalid_argument _ -> false (* is thrown by get_ikind_exp when the type of the expression is not an integer type *)
-    | exception Cilfacade.TypeOfError _ -> false
-    | ik ->
-      if IntDomain.should_wrap ik then
-        false
-      else if IntDomain.should_ignore_overflow ik then
-        true
-      else
-        not (ask.f (MaySignedOverflow exp))
-
   let no_overflow man exp = lazy (
-    let res = no_overflow man exp in
+    let res = SharedFunctions.no_overflow man exp in
     if M.tracing then M.tracel "no_ov" "no_ov %b exp: %a" res d_exp exp;
     res
   )
@@ -631,7 +614,7 @@ struct
         (* filter one-vars and exact *)
         (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
         if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
-          RD.cil_exp_of_lincons1 lincons1
+          RD.cil_exp_of_lincons1 ask lincons1
           |> Option.map e_inv
           |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)
         else
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 45b3e5d617..8881e4f9ce 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -730,7 +730,7 @@ struct
               (* filter one-vars and exact *)
               (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
               if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
-                RD.cil_exp_of_lincons1 lincons1
+                RD.cil_exp_of_lincons1 ask lincons1
                 |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp))
               else
                 None
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 751db12dba..b752b0ef2e 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -216,7 +216,7 @@ sig
   val to_lincons_array : t -> Lincons1.earray
   val of_lincons_array : Lincons1.earray -> t
 
-  val cil_exp_of_lincons1: Lincons1.t -> exp option
+  val cil_exp_of_lincons1: Queries.ask -> Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end
 
diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml
index 3b7226889f..4f4645d7eb 100644
--- a/src/cdomains/apron/relationDomain.apron.ml
+++ b/src/cdomains/apron/relationDomain.apron.ml
@@ -139,7 +139,7 @@ end
 module type S3 =
 sig
   include S2
-  val cil_exp_of_lincons1: Lincons1.t -> exp option
+  val cil_exp_of_lincons1: Queries.ask -> Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end
 
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 55c0c355e8..c04965aa4a 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -42,6 +42,20 @@ let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) =
     | _ ->
       failwith ("int_of_scalar: unsupported: " ^ Scalar.show scalar)
 
+(** An extended overflow handling inside relationAnalysis for expression assignments when overflows are assumed to occur.
+    Since affine equalities can only keep track of integer bounds of expressions evaluating to definite constants, we now query the integer bounds information for expressions from other analysis.
+    If an analysis returns bounds that are unequal to min and max of ikind , we can exclude the possibility that an overflow occurs and the abstract effect of the expression assignment can be used, i.e. we do not have to set the variable's value to top. *)
+let no_overflow (ask: Queries.ask) exp =
+  match Cilfacade.get_ikind_exp exp with
+  | exception Invalid_argument _ -> false (* is thrown by get_ikind_exp when the type of the expression is not an integer type *)
+  | exception Cilfacade.TypeOfError _ -> false
+  | ik ->
+    if IntDomain.should_wrap ik then
+      false
+    else if IntDomain.should_ignore_overflow ik then
+      true
+    else
+      not (ask.f (MaySignedOverflow exp))
 
 module type ConvertArg =
 sig
@@ -325,7 +339,7 @@ struct
       Linexpr1.iter lcm_coeff linexpr1; !lcm_denom
     with UnsupportedScalar -> Z.one
 
-  let cil_exp_of_lincons1 (lincons1:Lincons1.t) =
+  let cil_exp_of_lincons1 (ask: Queries.ask) (lincons1:Lincons1.t) =
     let zero = Cil.kinteger ILongLong 0 in
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in

From f3fd46863e48725efebb710cc7bbdb2f8ab62602 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 23 Jan 2025 16:51:07 +0200
Subject: [PATCH 02/11] Add cram test for not suffixing int constants with LL
 in loop invariants

---
 .../71-safe-program-example-loop-invariants.c |  27 +++
 .../71-safe-program-example-loop-invariants.t | 154 ++++++++++++++++++
 2 files changed, 181 insertions(+)
 create mode 100644 tests/regression/56-witness/71-safe-program-example-loop-invariants.c
 create mode 100644 tests/regression/56-witness/71-safe-program-example-loop-invariants.t

diff --git a/tests/regression/56-witness/71-safe-program-example-loop-invariants.c b/tests/regression/56-witness/71-safe-program-example-loop-invariants.c
new file mode 100644
index 0000000000..82114b616b
--- /dev/null
+++ b/tests/regression/56-witness/71-safe-program-example-loop-invariants.c
@@ -0,0 +1,27 @@
+void reach_error(){}
+extern unsigned int __VERIFIER_nondet_uint();
+extern unsigned char __VERIFIER_nondet_uchar(void);
+// CRAM
+int main() {
+  unsigned int n = __VERIFIER_nondet_uint();
+  if (n == 0) {
+    return 0;
+  }
+  unsigned int v = 0;
+  unsigned int s = 0;
+  unsigned int i = 0;
+  while (i < n) {
+    v = __VERIFIER_nondet_uchar();
+    s += v;
+    ++i;
+  }
+  if (s < v) {
+    reach_error();
+    return 1;
+  }
+  if (s > 65025) {
+    reach_error();
+    return 1;
+  }
+  return 0;
+}
\ No newline at end of file
diff --git a/tests/regression/56-witness/71-safe-program-example-loop-invariants.t b/tests/regression/56-witness/71-safe-program-example-loop-invariants.t
new file mode 100644
index 0000000000..2377478427
--- /dev/null
+++ b/tests/regression/56-witness/71-safe-program-example-loop-invariants.t
@@ -0,0 +1,154 @@
+  $ goblint --set ana.activated[+] apron --enable witness.yaml.enabled --set witness.yaml.entry-types '["invariant_set"]' --set witness.yaml.invariant-types '["loop_invariant"]' --enable ana.sv-comp.functions 71-safe-program-example-loop-invariants.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 21
+    dead: 0
+    total lines: 21
+  [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 14
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: invariant_set
+    content:
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: (long long )i + 255 >= (long long )v
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: (long long )i + 4294967295LL >= (long long )n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: (long long )n + (long long )i >= 1
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: (long long )n + 254 >= (long long )v
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: (long long )n >= (long long )i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: (long long )v + (long long )i >= 0
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: (long long )v + (long long )n >= 1
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: (long long )v + 4294967295LL >= (long long )i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: (long long )v + 4294967295LL >= (long long )n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: 4294967550LL >= (long long )v + (long long )i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: 4294967550LL >= (long long )v + (long long )n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: 8589934590LL >= (long long )n + (long long )i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: n != 0U
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants.c
+          file_hash: $FILE_HASH
+          line: 13
+          column: 3
+          function: main
+        value: v <= 255U
+        format: c_expression

From 2ee30c3ad0dffcfa8670c6e0bf7fbfa9671c9416 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 23 Jan 2025 16:54:54 +0200
Subject: [PATCH 03/11] Use IInt ikind for constants fitting into int range and
 discard constants not fitting into long in invariants

---
 src/cdomains/apron/sharedFunctions.apron.ml | 24 +++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index c04965aa4a..cfd6855327 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -267,23 +267,35 @@ struct
 
   let longlong = TInt(ILongLong,[])
 
+  (* Determines the integer kind (ikind) for a given constant.
+     - Defaults to IInt for values that fit int range to minimize the number of LL suffixes in invariants.
+     - Uses ILongLong to handle larger constants and prevent integer overflows.
+     - If the constant cannot fit into ILongLong, it is discarded with a warning. *)
+  let const_ikind i =
+    match () with
+    | _ when Cil.fitsInInt IInt i -> IInt
+    | _ when Cil.fitsInInt ILongLong i -> ILongLong
+    | _ ->
+      M.warn ~category:Analyzer "Invariant Apron: coefficient does not fit long type: %s" (Z.to_string i);
+      raise Unsupported_Linexpr1
 
   let coeff_to_const ~scalewith (c:Coeff.union_5) =
     match c with
     | Scalar c ->
       (match int_of_scalar ?scalewith c with
       | Some i ->
-        let ci,truncation = truncateCilint ILongLong i in
+        let ikind = const_ikind i in
+        let ci,truncation = truncateCilint ikind i in
         if truncation = NoTruncation then
           if Z.compare i Z.zero >= 0 then
-            false, Const (CInt(i,ILongLong,None))
+            false, Const (CInt(i,ikind,None))
           else
             (* attempt to negate if that does not cause an overflow *)
-            let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
+            let cneg, truncation = truncateCilint ikind (Z.neg i) in
             if truncation = NoTruncation then
-              true, Const (CInt((Z.neg i),ILongLong,None))
+              true, Const (CInt((Z.neg i),ikind,None))
             else
-              false, Const (CInt(i,ILongLong,None))
+              false, Const (CInt(i,ikind,None))
         else
           (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
       | None -> raise Unsupported_Linexpr1)
@@ -340,7 +352,7 @@ struct
     with UnsupportedScalar -> Z.one
 
   let cil_exp_of_lincons1 (ask: Queries.ask) (lincons1:Lincons1.t) =
-    let zero = Cil.kinteger ILongLong 0 in
+    let zero = Cil.kinteger IInt 0 in
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
       let common_denominator = lcm_den linexpr1 in

From 6ac5ad25d2824310733d3a635b88b6c33b3a6918 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 23 Jan 2025 17:28:30 +0200
Subject: [PATCH 04/11] Check for overflows in invariants and discard
 overflowing expressions

---
 src/cdomains/apron/sharedFunctions.apron.ml   | 20 ++++++++++++-------
 .../71-safe-program-example-loop-invariants.t |  4 ++--
 2 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index cfd6855327..c08015ba0c 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -267,6 +267,12 @@ struct
 
   let longlong = TInt(ILongLong,[])
 
+  let check_for_overflows (ask: Queries.ask) exp =
+    if no_overflow ask exp then
+      exp
+    else
+      (M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" CilType.Exp.pretty exp; raise Unsupported_Linexpr1)
+
   (* Determines the integer kind (ikind) for a given constant.
      - Defaults to IInt for values that fit int range to minimize the number of LL suffixes in invariants.
      - Uses ILongLong to handle larger constants and prevent integer overflows.
@@ -301,12 +307,12 @@ struct
       | None -> raise Unsupported_Linexpr1)
     | _ -> raise Unsupported_Linexpr1
 
-  let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v =
+  let cil_exp_of_linexpr1_term ~scalewith (ask: Queries.ask) (c: Coeff.t) v =
     match V.to_cil_varinfo v with
     | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
       let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
       let flip, coeff = coeff_to_const ~scalewith c in
-      let prod = BinOp(Mult, coeff, var, longlong) in
+      let prod = check_for_overflows ask (Cilfacade.makeBinOp Mult coeff var) in
       flip, prod
     | None ->
       M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v;
@@ -315,11 +321,11 @@ struct
       M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v;
       raise Unsupported_Linexpr1
 
-  let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
+  let cil_exp_of_linexpr1 ?scalewith (ask: Queries.ask) (linexpr1:Linexpr1.t) =
     let terms = ref [coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1)] in
     let append_summand (c:Coeff.union_5) v =
       if not (Coeff.is_zero c) then
-        terms := cil_exp_of_linexpr1_term ~scalewith c v :: !terms
+        terms := cil_exp_of_linexpr1_term ~scalewith (ask: Queries.ask) c v :: !terms
     in
     Linexpr1.iter append_summand linexpr1;
     !terms
@@ -356,13 +362,13 @@ struct
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
       let common_denominator = lcm_den linexpr1 in
-      let terms = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
+      let terms = cil_exp_of_linexpr1 ~scalewith:common_denominator (ask: Queries.ask) linexpr1 in
       let (nterms, pterms) = Tuple2.mapn (List.map snd) (List.partition fst terms) in
       let fold_terms terms =
         List.fold_left (fun acc term ->
             match acc with
-            | None -> Some term
-            | Some exp -> Some (BinOp (PlusA, exp, term, longlong))
+            | None -> Some (check_for_overflows ask term)
+            | Some exp -> Some (check_for_overflows ask (Cilfacade.makeBinOp PlusA exp term))
           ) None terms
         |> Option.default zero
       in
diff --git a/tests/regression/56-witness/71-safe-program-example-loop-invariants.t b/tests/regression/56-witness/71-safe-program-example-loop-invariants.t
index 2377478427..72c91751c4 100644
--- a/tests/regression/56-witness/71-safe-program-example-loop-invariants.t
+++ b/tests/regression/56-witness/71-safe-program-example-loop-invariants.t
@@ -20,7 +20,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )i + 255 >= (long long )v
+        value: (long long )i + 255LL >= (long long )v
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -50,7 +50,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )n + 254 >= (long long )v
+        value: (long long )n + 254LL >= (long long )v
         format: c_expression
     - invariant:
         type: loop_invariant

From 6a3986738e7b9869cdadecfbb408ed1a8bdf5f58 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 24 Jan 2025 17:34:51 +0200
Subject: [PATCH 05/11] Rename test

---
 ...-safe-program-example-loop-invariants-2.c} |  0
 ...-safe-program-example-loop-invariants-2.t} | 30 +++++++++----------
 2 files changed, 15 insertions(+), 15 deletions(-)
 rename tests/regression/56-witness/{71-safe-program-example-loop-invariants.c => 72-safe-program-example-loop-invariants-2.c} (100%)
 rename tests/regression/56-witness/{71-safe-program-example-loop-invariants.t => 72-safe-program-example-loop-invariants-2.t} (80%)

diff --git a/tests/regression/56-witness/71-safe-program-example-loop-invariants.c b/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.c
similarity index 100%
rename from tests/regression/56-witness/71-safe-program-example-loop-invariants.c
rename to tests/regression/56-witness/72-safe-program-example-loop-invariants-2.c
diff --git a/tests/regression/56-witness/71-safe-program-example-loop-invariants.t b/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t
similarity index 80%
rename from tests/regression/56-witness/71-safe-program-example-loop-invariants.t
rename to tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t
index 72c91751c4..eb337aabac 100644
--- a/tests/regression/56-witness/71-safe-program-example-loop-invariants.t
+++ b/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t
@@ -1,4 +1,4 @@
-  $ goblint --set ana.activated[+] apron --enable witness.yaml.enabled --set witness.yaml.entry-types '["invariant_set"]' --set witness.yaml.invariant-types '["loop_invariant"]' --enable ana.sv-comp.functions 71-safe-program-example-loop-invariants.c
+  $ goblint --set ana.activated[+] apron --enable witness.yaml.enabled --set witness.yaml.entry-types '["invariant_set"]' --set witness.yaml.invariant-types '["loop_invariant"]' --enable ana.sv-comp.functions 72-safe-program-example-loop-invariants-2.c
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 21
     dead: 0
@@ -15,7 +15,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -25,7 +25,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -35,7 +35,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -45,7 +45,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -55,7 +55,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -65,7 +65,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -75,7 +75,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -85,7 +85,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -95,7 +95,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -105,7 +105,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -115,7 +115,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -125,7 +125,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -135,7 +135,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3
@@ -145,7 +145,7 @@
     - invariant:
         type: loop_invariant
         location:
-          file_name: 71-safe-program-example-loop-invariants.c
+          file_name: 72-safe-program-example-loop-invariants-2.c
           file_hash: $FILE_HASH
           line: 13
           column: 3

From a823c1d0c5876681b73c9b7368e8faf982dc0b02 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 27 Jan 2025 15:54:28 +0200
Subject: [PATCH 06/11] Add CRAM test for minimizing casts in invariants with
 char-type variables

---
 ...1-safe-program-example-loop-invariants-1.c |  31 ++++
 ...1-safe-program-example-loop-invariants-1.t | 144 ++++++++++++++++++
 2 files changed, 175 insertions(+)
 create mode 100644 tests/regression/56-witness/71-safe-program-example-loop-invariants-1.c
 create mode 100644 tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t

diff --git a/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.c b/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.c
new file mode 100644
index 0000000000..11424bc69b
--- /dev/null
+++ b/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.c
@@ -0,0 +1,31 @@
+// This file is part of sv-witnesses repository: https://github.com/sosy-lab/sv-witnesses
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+// CRAM
+void reach_error(){}
+extern unsigned char __VERIFIER_nondet_uchar(void);
+int main() {
+  unsigned char n = __VERIFIER_nondet_uchar();
+  if (n == 0) {
+    return 0;
+  }
+  unsigned char v = 0;
+  unsigned int  s = 0;
+  unsigned int  i = 0;
+  while (i < n) {
+    v = __VERIFIER_nondet_uchar();
+    s += v;
+    ++i;
+  }
+  if (s < v) {
+    reach_error();
+    return 1;
+  }
+  if (s > 65025) {
+    reach_error();
+    return 1;
+  }
+  return 0;
+}
diff --git a/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t b/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t
new file mode 100644
index 0000000000..9f23b6394d
--- /dev/null
+++ b/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t
@@ -0,0 +1,144 @@
+  $ goblint --set ana.activated[+] apron --enable witness.yaml.enabled --set witness.yaml.entry-types '["invariant_set"]' --set witness.yaml.invariant-types '["loop_invariant"]' --enable ana.sv-comp.functions 71-safe-program-example-loop-invariants-1.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 20
+    dead: 0
+    total lines: 20
+  [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 13
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: invariant_set
+    content:
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: (long long )i + 254LL >= (long long )v
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: (long long )i + 255LL >= (long long )n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: (long long )n + (long long )i >= 1
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: (long long )n + 254LL >= (long long )v
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: (long long )n >= (long long )i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: (long long )v + (long long )i >= 0
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: (long long )v + (long long )n >= 1
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: (long long )v + 255LL >= (long long )i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: (long long )v + 255LL >= (long long )n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: 510 >= (long long )n + (long long )i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: 510 >= (long long )v + (long long )i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: 510 >= (long long )v + (long long )n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 71-safe-program-example-loop-invariants-1.c
+          file_hash: $FILE_HASH
+          line: 17
+          column: 3
+          function: main
+        value: n != (unsigned char)0
+        format: c_expression

From 70309dd50d5fd11d3a6fa466330cff54ff5a5290 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 27 Jan 2025 19:41:55 +0200
Subject: [PATCH 07/11] Minimize unnecessary casts in invariants

---
 src/analyses/apron/relationAnalysis.apron.ml  |  2 +-
 src/analyses/apron/relationPriv.apron.ml      |  2 +-
 src/cdomains/apron/apronDomain.apron.ml       |  2 +-
 src/cdomains/apron/relationDomain.apron.ml    |  2 +-
 src/cdomains/apron/sharedFunctions.apron.ml   | 77 ++++++++++++++-----
 .../regression/36-apron/12-traces-min-rpb1.t  |  8 +-
 tests/regression/36-apron/52-queuesize.t      | 32 ++++----
 tests/regression/46-apron2/98-issue-1511b.t   | 48 ++++++------
 ...1-safe-program-example-loop-invariants-1.t | 26 +++----
 ...2-safe-program-example-loop-invariants-2.t |  4 +-
 10 files changed, 119 insertions(+), 84 deletions(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 8395a3d233..12bba88f4b 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -614,7 +614,7 @@ struct
         (* filter one-vars and exact *)
         (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
         if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
-          RD.cil_exp_of_lincons1 ask lincons1
+          RD.cil_exp_of_lincons1 ask e_inv lincons1
           |> Option.map e_inv
           |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)
         else
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 8881e4f9ce..e083988be6 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -730,7 +730,7 @@ struct
               (* filter one-vars and exact *)
               (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
               if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
-                RD.cil_exp_of_lincons1 ask lincons1
+                RD.cil_exp_of_lincons1 ask Fun.id lincons1
                 |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp))
               else
                 None
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index b752b0ef2e..4d2b3393ea 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -216,7 +216,7 @@ sig
   val to_lincons_array : t -> Lincons1.earray
   val of_lincons_array : Lincons1.earray -> t
 
-  val cil_exp_of_lincons1: Queries.ask -> Lincons1.t -> exp option
+  val cil_exp_of_lincons1: Queries.ask -> (exp -> exp) -> Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end
 
diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml
index 4f4645d7eb..258d12c763 100644
--- a/src/cdomains/apron/relationDomain.apron.ml
+++ b/src/cdomains/apron/relationDomain.apron.ml
@@ -139,7 +139,7 @@ end
 module type S3 =
 sig
   include S2
-  val cil_exp_of_lincons1: Queries.ask -> Lincons1.t -> exp option
+  val cil_exp_of_lincons1: Queries.ask -> (exp -> exp) -> Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end
 
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index c08015ba0c..6876c3208f 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -267,11 +267,42 @@ struct
 
   let longlong = TInt(ILongLong,[])
 
-  let check_for_overflows (ask: Queries.ask) exp =
-    if no_overflow ask exp then
-      exp
+  let check_for_overflows_no_further_cast (ask: Queries.ask) (e_inv: exp -> exp) cast_exp exp_plain =
+    if no_overflow ask (e_inv cast_exp) then
+      cast_exp, exp_plain
+    else (
+      M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" CilType.Exp.pretty cast_exp;
+      raise Unsupported_Linexpr1
+    )
+
+  let is_cast_injective_vtype vinfo = IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:longlong
+
+  let rec check_for_overflows (ask: Queries.ask) (e_inv: exp -> exp) exp exp_plain =
+    if no_overflow ask (e_inv exp) then
+      exp, exp_plain
     else
-      (M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" CilType.Exp.pretty exp; raise Unsupported_Linexpr1)
+      match exp with
+      | Lval (Var vinfo, NoOffset) as var when is_cast_injective_vtype vinfo ->
+        let cast_var = Cilfacade.mkCast ~e:var ~newt:longlong in
+        check_for_overflows_no_further_cast ask e_inv cast_var cast_var
+      | BinOp (op, (Const i as c), ((Lval (Var vinfo, NoOffset)) as var), _) when is_cast_injective_vtype vinfo ->
+        let cast_var = Cilfacade.mkCast ~e:var ~newt:longlong in
+        let cast_exp_plain = BinOp (op, c, cast_var, longlong) in
+        let cast_exp = Cilfacade.makeBinOp op c cast_var in
+        check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
+      | BinOp (op, ((Lval (Var vinfo1, NoOffset)) as var1), ((Lval (Var vinfo2, NoOffset)) as var2), _) when is_cast_injective_vtype vinfo1 && is_cast_injective_vtype vinfo2 ->
+        let cast_var = Cilfacade.mkCast ~e:var1 ~newt:longlong in
+        let cast_exp_plain = BinOp (op, cast_var, var2, longlong) in
+        let cast_exp = Cilfacade.makeBinOp op cast_var var2 in
+        check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
+      | BinOp (op, exp1, exp2, _) ->
+        let cast_exp1 = Cilfacade.mkCast ~e:exp1 ~newt:longlong in
+        let cast_exp_plain = BinOp (op, cast_exp1, exp2, longlong) in
+        let cast_exp = Cilfacade.makeBinOp op cast_exp1 exp2 in
+        check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
+      | _ ->
+        M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil expression in overflow preserving manner: %a" CilType.Exp.pretty exp;
+        raise Unsupported_Linexpr1
 
   (* Determines the integer kind (ikind) for a given constant.
      - Defaults to IInt for values that fit int range to minimize the number of LL suffixes in invariants.
@@ -282,7 +313,7 @@ struct
     | _ when Cil.fitsInInt IInt i -> IInt
     | _ when Cil.fitsInInt ILongLong i -> ILongLong
     | _ ->
-      M.warn ~category:Analyzer "Invariant Apron: coefficient does not fit long type: %s" (Z.to_string i);
+      M.warn ~category:Analyzer "Invariant Apron: coefficient does not fit long long type: %s" (Z.to_string i);
       raise Unsupported_Linexpr1
 
   let coeff_to_const ~scalewith (c:Coeff.union_5) =
@@ -307,25 +338,25 @@ struct
       | None -> raise Unsupported_Linexpr1)
     | _ -> raise Unsupported_Linexpr1
 
-  let cil_exp_of_linexpr1_term ~scalewith (ask: Queries.ask) (c: Coeff.t) v =
+  let cil_exp_of_linexpr1_term ~scalewith (ask: Queries.ask) (e_inv: exp -> exp) (c: Coeff.t) v =
     match V.to_cil_varinfo v with
-    | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
-      let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
+    | Some vinfo ->
+      let var = Lval (Var vinfo, NoOffset) in
       let flip, coeff = coeff_to_const ~scalewith c in
-      let prod = check_for_overflows ask (Cilfacade.makeBinOp Mult coeff var) in
-      flip, prod
+      let exp = Cilfacade.makeBinOp Mult coeff var in
+      let exp_plain = BinOp (Mult, coeff, var, Cilfacade.typeOf exp) in
+      let prod, prod_plain = check_for_overflows ask e_inv exp exp_plain in
+      flip, (prod, prod_plain)
     | None ->
       M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v;
       raise Unsupported_Linexpr1
-    | _ ->
-      M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v;
-      raise Unsupported_Linexpr1
 
-  let cil_exp_of_linexpr1 ?scalewith (ask: Queries.ask) (linexpr1:Linexpr1.t) =
-    let terms = ref [coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1)] in
+  let cil_exp_of_linexpr1 ?scalewith (ask: Queries.ask) (e_inv: exp -> exp) (linexpr1:Linexpr1.t) =
+    let flip, coeff = coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1) in
+    let terms = ref [flip, (coeff, coeff)] in
     let append_summand (c:Coeff.union_5) v =
       if not (Coeff.is_zero c) then
-        terms := cil_exp_of_linexpr1_term ~scalewith (ask: Queries.ask) c v :: !terms
+        terms := cil_exp_of_linexpr1_term ~scalewith (ask: Queries.ask) e_inv c v :: !terms
     in
     Linexpr1.iter append_summand linexpr1;
     !terms
@@ -357,19 +388,23 @@ struct
       Linexpr1.iter lcm_coeff linexpr1; !lcm_denom
     with UnsupportedScalar -> Z.one
 
-  let cil_exp_of_lincons1 (ask: Queries.ask) (lincons1:Lincons1.t) =
+  let cil_exp_of_lincons1 (ask: Queries.ask) (e_inv: exp -> exp) (lincons1:Lincons1.t)  =
     let zero = Cil.kinteger IInt 0 in
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
       let common_denominator = lcm_den linexpr1 in
-      let terms = cil_exp_of_linexpr1 ~scalewith:common_denominator (ask: Queries.ask) linexpr1 in
+      let terms = cil_exp_of_linexpr1 ~scalewith:common_denominator (ask: Queries.ask) e_inv linexpr1 in
       let (nterms, pterms) = Tuple2.mapn (List.map snd) (List.partition fst terms) in
       let fold_terms terms =
-        List.fold_left (fun acc term ->
+        List.fold_left (fun acc (term, term_plain) ->
             match acc with
-            | None -> Some (check_for_overflows ask term)
-            | Some exp -> Some (check_for_overflows ask (Cilfacade.makeBinOp PlusA exp term))
+            | None -> Some (check_for_overflows ask e_inv term term_plain)
+            | Some (exp, exp_plain) ->
+              let exp' = Cilfacade.makeBinOp PlusA exp term in
+              let exp_plain' = BinOp (PlusA, exp_plain, term_plain, Cilfacade.typeOf exp') in
+              Some (check_for_overflows ask e_inv exp' exp_plain')
           ) None terms
+        |> Option.map Tuple2.second
         |> Option.default zero
       in
       let lhs = fold_terms pterms in
diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t
index 3f2446710c..65aad3342c 100644
--- a/tests/regression/36-apron/12-traces-min-rpb1.t
+++ b/tests/regression/36-apron/12-traces-min-rpb1.t
@@ -32,7 +32,7 @@
       column: 3
       function: main
     location_invariant:
-      string: (long long )h == (long long )g
+      string: h == g
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -43,7 +43,7 @@
       column: 3
       function: t_fun
     location_invariant:
-      string: (long long )h == (long long )g
+      string: h == g
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -54,7 +54,7 @@
       column: 3
       function: t_fun
     location_invariant:
-      string: (long long )h == (long long )g
+      string: h == g
       type: assertion
       format: C
 
@@ -173,6 +173,6 @@
           format: c_expression
   - entry_type: flow_insensitive_invariant
     flow_insensitive_invariant:
-      string: '! multithreaded || (A_locked || (long long )g == (long long )h)'
+      string: '! multithreaded || (A_locked || g == h)'
       type: assertion
       format: C
diff --git a/tests/regression/36-apron/52-queuesize.t b/tests/regression/36-apron/52-queuesize.t
index cb8eedf9ab..0639d42a05 100644
--- a/tests/regression/36-apron/52-queuesize.t
+++ b/tests/regression/36-apron/52-queuesize.t
@@ -56,7 +56,7 @@ Without diff-box:
       column: 3
       function: push
     location_invariant:
-      string: 2147483647LL >= (long long )capacity
+      string: free >= 0
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -67,7 +67,7 @@ Without diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (long long )used + (long long )free == (long long )capacity
+      string: capacity >= free
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -78,7 +78,7 @@ Without diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (long long )free >= 0LL
+      string: 2147483647 >= capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -89,7 +89,7 @@ Without diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (long long )capacity >= (long long )free
+      string: (long long )used + free == capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -100,7 +100,7 @@ Without diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: 2147483647LL >= (long long )capacity
+      string: free >= 0
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -111,7 +111,7 @@ Without diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: (long long )used + (long long )free == (long long )capacity
+      string: capacity >= free
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -122,7 +122,7 @@ Without diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: (long long )free >= 0LL
+      string: 2147483647 >= capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -133,7 +133,7 @@ Without diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: (long long )capacity >= (long long )free
+      string: (long long )used + free == capacity
       type: assertion
       format: C
 
@@ -193,7 +193,7 @@ With diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (long long )used + (long long )free == (long long )capacity
+      string: free >= 0
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -204,7 +204,7 @@ With diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (long long )free >= 0LL
+      string: capacity >= free
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -215,7 +215,7 @@ With diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (long long )capacity >= (long long )free
+      string: (long long )used + free == capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -226,7 +226,7 @@ With diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: (long long )used + (long long )free == (long long )capacity
+      string: free >= 0
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -237,7 +237,7 @@ With diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: (long long )free >= 0LL
+      string: capacity >= free
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -248,7 +248,7 @@ With diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: (long long )capacity >= (long long )free
+      string: (long long )used + free == capacity
       type: assertion
       format: C
 
@@ -264,7 +264,7 @@ Compare witnesses:
       column: 3
       function: push
     location_invariant:
-      string: 2147483647LL >= (long long )capacity
+      string: 2147483647 >= capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -275,7 +275,7 @@ Compare witnesses:
       column: 3
       function: pop
     location_invariant:
-      string: 2147483647LL >= (long long )capacity
+      string: 2147483647 >= capacity
       type: assertion
       format: C
   ---
diff --git a/tests/regression/46-apron2/98-issue-1511b.t b/tests/regression/46-apron2/98-issue-1511b.t
index 509425ab14..6683780c09 100644
--- a/tests/regression/46-apron2/98-issue-1511b.t
+++ b/tests/regression/46-apron2/98-issue-1511b.t
@@ -16,29 +16,29 @@
     unsupported: 2
     disabled: 0
     total validation entries: 54
-  [Success][Witness] invariant confirmed: ((long long )j + (long long )d) + 2147483648LL >= 0LL (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: ((long long )k + (long long )d) + 2147483647LL >= 0LL (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: ((long long )k + (long long )j) + 2147483646LL >= 0LL (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )d + 2147483648LL >= (long long )j (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )d + 2147483649LL >= (long long )k (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )j + 1LL >= (long long )k (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )j + 2147483647LL >= (long long )d (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )d (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )j (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: 1LL >= (long long )k + (long long )j (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: 2147483647LL >= (long long )j + (long long )d (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + (long long )d (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: ((long long )k + d) + 2147483647 >= 0 (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (j + d) + 2147483648LL >= 0 (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (k + j) + 2147483646 >= 0 (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: 1 >= k + j (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: 2147483647 >= j + d (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + d (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: d + 2147483648LL >= j (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: d + 2147483649LL >= k (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: j + 1 >= k (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: j + 2147483647 >= d (98-issue-1511b.c:22:5)
   [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: ((long long )j + (long long )d) + 2147483648LL >= 0LL (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: ((long long )k + (long long )d) + 2147483647LL >= 0LL (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: ((long long )k + (long long )j) + 2147483646LL >= 0LL (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )d + 2147483648LL >= (long long )j (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )d + 2147483649LL >= (long long )k (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )j + 1LL >= (long long )k (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )j + 2147483647LL >= (long long )d (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )d (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )j (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: 1LL >= (long long )k + (long long )j (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: 2147483647LL >= (long long )j + (long long )d (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + (long long )d (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: k + 2147483646 >= d (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: k + 2147483646 >= j (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: ((long long )k + d) + 2147483647 >= 0 (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (j + d) + 2147483648LL >= 0 (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (k + j) + 2147483646 >= 0 (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: 1 >= k + j (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: 2147483647 >= j + d (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + d (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: d + 2147483648LL >= j (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: d + 2147483649LL >= k (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: j + 1 >= k (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: j + 2147483647 >= d (98-issue-1511b.c:27:5)
   [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: k + 2147483646 >= d (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: k + 2147483646 >= j (98-issue-1511b.c:27:5)
diff --git a/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t b/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t
index 9f23b6394d..58b11ca1ef 100644
--- a/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t
+++ b/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t
@@ -20,7 +20,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )i + 254LL >= (long long )v
+        value: (long long )i + 254 >= v
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -30,7 +30,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )i + 255LL >= (long long )n
+        value: (long long )i + 255 >= n
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -40,7 +40,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )n + (long long )i >= 1
+        value: 510 >= n + (long long )i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -50,7 +50,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )n + 254LL >= (long long )v
+        value: 510 >= v + (long long )i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -60,7 +60,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )n >= (long long )i
+        value: 510 >= v + n
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -70,7 +70,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )v + (long long )i >= 0
+        value: n != (unsigned char)0
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -80,7 +80,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )v + (long long )n >= 1
+        value: n + (long long )i >= 1
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -90,7 +90,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )v + 255LL >= (long long )i
+        value: n + 254 >= v
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -100,7 +100,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )v + 255LL >= (long long )n
+        value: n >= (long long )i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -110,7 +110,7 @@
           line: 17
           column: 3
           function: main
-        value: 510 >= (long long )n + (long long )i
+        value: v + (long long )i >= 0
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -120,7 +120,7 @@
           line: 17
           column: 3
           function: main
-        value: 510 >= (long long )v + (long long )i
+        value: v + 255 >= (long long )i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -130,7 +130,7 @@
           line: 17
           column: 3
           function: main
-        value: 510 >= (long long )v + (long long )n
+        value: v + 255 >= n
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -140,5 +140,5 @@
           line: 17
           column: 3
           function: main
-        value: n != (unsigned char)0
+        value: v + n >= 1
         format: c_expression
diff --git a/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t b/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t
index eb337aabac..122d1de2f7 100644
--- a/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t
+++ b/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t
@@ -20,7 +20,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )i + 255LL >= (long long )v
+        value: (long long )i + 255 >= (long long )v
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -50,7 +50,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )n + 254LL >= (long long )v
+        value: (long long )n + 254 >= (long long )v
         format: c_expression
     - invariant:
         type: loop_invariant

From 7310d98945df12d6f449aac0a4017de07534baca Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 29 Jan 2025 16:31:44 +0200
Subject: [PATCH 08/11] Create a query to ask for overflows for unsigned types

---
 src/analyses/base.ml   | 41 ++++++++++++++++++++++-------------------
 src/domains/queries.ml | 17 ++++++++++++-----
 2 files changed, 34 insertions(+), 24 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index f24ae36b2c..69bb0a9425 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1298,7 +1298,7 @@ struct
       For now we return true if the expression contains a shift left.
   *)
   (* TODO: deduplicate https://github.com/goblint/analyzer/pull/1297#discussion_r1477804502 *)
-  let rec exp_may_signed_overflow man exp =
+  let rec exp_may_overflow man exp ~unsigned =
     let res = match Cilfacade.get_ikind_exp exp with
       | exception (Cilfacade.TypeOfError _) (* Cilfacade.typeOf *)
       | exception (Invalid_argument _) -> (* get_ikind *)
@@ -1360,20 +1360,20 @@ struct
         | Imag e
         | SizeOfE e
         | AlignOfE e
-        | CastE (_, e) -> exp_may_signed_overflow man e
+        | CastE (_, e) -> exp_may_overflow man e ~unsigned:unsigned
         | UnOp (unop, e, _) ->
           (* check if the current operation causes a signed overflow *)
           begin match unop with
             | Neg -> (* an overflow happens when the lower bound of the interval is less than MIN_INT *)
-              Cil.isSigned ik && checkPredicate e (Z.gt)
+              (unsigned || Cil.isSigned ik) && checkPredicate e (Z.gt)
             (* operations that do not result in overflow in C: *)
             | BNot|LNot -> false
           end
           (* look for overflow in subexpression *)
-          || exp_may_signed_overflow man e
+          || exp_may_overflow man e ~unsigned:unsigned
         | BinOp (binop, e1, e2, _) ->
           (* check if the current operation causes a signed overflow *)
-          (Cil.isSigned ik && begin match binop with
+          ((unsigned || Cil.isSigned ik) && begin match binop with
               | PlusA|PlusPI|IndexPI -> checkBinop e1 e2 (GobOption.map2 Z.(+))
               | MinusA|MinusPI|MinusPP -> checkBinop e1 e2 (GobOption.map2 Z.(-))
               | Mult -> checkBinop e1 e2 (GobOption.map2 Z.mul)
@@ -1385,27 +1385,27 @@ struct
               (* Shiftlt can cause overflow and also undefined behaviour in case the second operand is non-positive*)
               | Shiftlt -> true end)
           (* look for overflow in subexpression *)
-          || exp_may_signed_overflow man e1 || exp_may_signed_overflow man e2
+          || exp_may_overflow man e1 ~unsigned:unsigned || exp_may_overflow man e2 ~unsigned:unsigned
         | Question (e1, e2, e3, _) ->
           (* does not result in overflow in C *)
-          exp_may_signed_overflow man e1 || exp_may_signed_overflow man e2 || exp_may_signed_overflow man e3
+          exp_may_overflow man e1 ~unsigned:unsigned || exp_may_overflow man e2 ~unsigned:unsigned || exp_may_overflow man e3 ~unsigned:unsigned
         | Lval lval
         | AddrOf lval
-        | StartOf lval -> lval_may_signed_overflow man lval
+        | StartOf lval -> lval_may_overflow man lval ~unsigned:unsigned
     in
-    if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp exp res; res
-  and lval_may_signed_overflow man (lval : lval) =
+    if M.tracing then M.trace "signed_overflow" "base exp_may_overflow %a. Result = %b" d_plainexp exp res; res
+  and lval_may_overflow man (lval : lval) ~unsigned =
     let (host, offset) = lval in
-    let host_may_signed_overflow = function
+    let host_may_overflow = function
       | Var v -> false
-      | Mem e -> exp_may_signed_overflow man e
+      | Mem e -> exp_may_overflow man e ~unsigned:unsigned
     in
-    let rec offset_may_signed_overflow = function
+    let rec offset_may_overflow = function
       | NoOffset -> false
-      | Index (e, o) -> exp_may_signed_overflow man e || offset_may_signed_overflow o
-      | Field (f, o) -> offset_may_signed_overflow o
+      | Index (e, o) -> exp_may_overflow man e ~unsigned:unsigned || offset_may_overflow o
+      | Field (f, o) -> offset_may_overflow o
     in
-    host_may_signed_overflow host || offset_may_signed_overflow offset
+    host_may_overflow host || offset_may_overflow offset
 
   let query man (type a) (q: a Q.t): a Q.result =
     match q with
@@ -1577,9 +1577,12 @@ struct
     | Q.InvariantGlobal g ->
       let g: V.t = Obj.obj g in
       query_invariant_global man g
-    | Q.MaySignedOverflow e -> (let res = exp_may_signed_overflow man e in
-                                if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp e res; res
-                               )
+    | Q.MaySignedOverflow e ->
+      let res = exp_may_overflow man e ~unsigned:false in
+      if M.tracing then M.trace "signed_overflow" "base exp_may_overflow %a. Result = %b" d_plainexp e res; res
+    | Q.MayOverflow e ->
+      let res = exp_may_overflow man e ~unsigned:true in
+      if M.tracing then M.trace "overflow" "base exp_may_overflow %a. Result = %b" d_plainexp e res; res
     | _ -> Q.Result.top q
 
   let update_variable variable typ value cpa =
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index f43cd77eca..5930793208 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -130,6 +130,7 @@ type _ t =
   | IsEverMultiThreaded: MayBool.t t
   | TmpSpecial: Mval.Exp.t -> ML.t t
   | MaySignedOverflow: exp -> MayBool.t t
+  | MayOverflow: exp -> MayBool.t t
   | GasExhausted: CilType.Fundec.t ->  MustBool.t t
   | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t (** YAML witness entries for a global unknown ([Obj.t] represents [Spec.V.t]) and YAML witness task. *)
   | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t
@@ -205,6 +206,7 @@ struct
     | IsEverMultiThreaded -> (module MayBool)
     | TmpSpecial _ -> (module ML)
     | MaySignedOverflow  _ -> (module MayBool)
+    | MayOverflow  _ -> (module MayBool)
     | GasExhausted _ -> (module MustBool)
     | YamlEntryGlobal _ -> (module YS)
     | GhostVarAvailable _ -> (module MayBool)
@@ -279,6 +281,7 @@ struct
     | IsEverMultiThreaded -> MayBool.top ()
     | TmpSpecial _ -> ML.top ()
     | MaySignedOverflow _ -> MayBool.top ()
+    | MayOverflow _ -> MayBool.top ()
     | GasExhausted _ -> MustBool.top ()
     | YamlEntryGlobal _ -> YS.top ()
     | GhostVarAvailable _ -> MayBool.top ()
@@ -349,11 +352,12 @@ struct
     | Any (TmpSpecial _) -> 56
     | Any (IsAllocVar _) -> 57
     | Any (MaySignedOverflow _) -> 58
-    | Any (GasExhausted _) -> 59
-    | Any (YamlEntryGlobal _) -> 60
-    | Any (MustProtectingLocks _) -> 61
-    | Any (GhostVarAvailable _) -> 62
-    | Any InvariantGlobalNodes -> 63
+    | Any (MayOverflow _) -> 59
+    | Any (GasExhausted _) -> 60
+    | Any (YamlEntryGlobal _) -> 61
+    | Any (MustProtectingLocks _) -> 62
+    | Any (GhostVarAvailable _) -> 63
+    | Any InvariantGlobalNodes -> 64
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -410,6 +414,7 @@ struct
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
       | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2
       | Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2
+      | Any (MayOverflow e1), Any (MayOverflow e2) -> CilType.Exp.compare e1 e2
       | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2
       | Any (GhostVarAvailable v1), Any (GhostVarAvailable v2) -> WitnessGhostVar.compare v1 v2
       (* only argumentless queries should remain *)
@@ -456,6 +461,7 @@ struct
     | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
     | Any (TmpSpecial lv) -> Mval.Exp.hash lv
     | Any (MaySignedOverflow e) -> CilType.Exp.hash e
+    | Any (MayOverflow e) -> CilType.Exp.hash e
     | Any (GasExhausted f) -> CilType.Fundec.hash f
     | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v
     (* IterSysVars:                                                                    *)
@@ -523,6 +529,7 @@ struct
     | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded"
     | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv
     | Any (MaySignedOverflow e) -> Pretty.dprintf "MaySignedOverflow %a" CilType.Exp.pretty e
+    | Any (MayOverflow e) -> Pretty.dprintf "MayOverflow %a" CilType.Exp.pretty e
     | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f
     | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v
     | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes"

From 3062125203b4649c329e330b7d5e8b94486eed6d Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 29 Jan 2025 16:33:42 +0200
Subject: [PATCH 09/11] Update CRAM tests: avoid unnecessary casts for unsigned
 arithmetic without overflows

---
 ...1-safe-program-example-loop-invariants-1.t | 22 ++++++++--------
 ...2-safe-program-example-loop-invariants-2.t | 26 +++++++++----------
 2 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t b/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t
index 58b11ca1ef..de90e76b76 100644
--- a/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t
+++ b/tests/regression/56-witness/71-safe-program-example-loop-invariants-1.t
@@ -20,7 +20,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )i + 254 >= v
+        value: 510 >= n + i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -30,7 +30,7 @@
           line: 17
           column: 3
           function: main
-        value: (long long )i + 255 >= n
+        value: 510 >= v + i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -40,7 +40,7 @@
           line: 17
           column: 3
           function: main
-        value: 510 >= n + (long long )i
+        value: 510 >= v + n
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -50,7 +50,7 @@
           line: 17
           column: 3
           function: main
-        value: 510 >= v + (long long )i
+        value: i + 254 >= v
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -60,7 +60,7 @@
           line: 17
           column: 3
           function: main
-        value: 510 >= v + n
+        value: i + 255 >= n
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -80,7 +80,7 @@
           line: 17
           column: 3
           function: main
-        value: n + (long long )i >= 1
+        value: n + 254 >= v
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -90,7 +90,7 @@
           line: 17
           column: 3
           function: main
-        value: n + 254 >= v
+        value: n + i >= 1
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -100,7 +100,7 @@
           line: 17
           column: 3
           function: main
-        value: n >= (long long )i
+        value: n >= i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -110,7 +110,7 @@
           line: 17
           column: 3
           function: main
-        value: v + (long long )i >= 0
+        value: v + 255 >= i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -120,7 +120,7 @@
           line: 17
           column: 3
           function: main
-        value: v + 255 >= (long long )i
+        value: v + 255 >= n
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -130,7 +130,7 @@
           line: 17
           column: 3
           function: main
-        value: v + 255 >= n
+        value: v + i >= 0
         format: c_expression
     - invariant:
         type: loop_invariant
diff --git a/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t b/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t
index 122d1de2f7..1edfc2cc7a 100644
--- a/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t
+++ b/tests/regression/56-witness/72-safe-program-example-loop-invariants-2.t
@@ -20,7 +20,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )i + 255 >= (long long )v
+        value: (long long )i + 255 >= v
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -30,7 +30,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )i + 4294967295LL >= (long long )n
+        value: (long long )n + 254 >= v
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -40,7 +40,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )n + (long long )i >= 1
+        value: (long long )n + i >= 1
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -50,7 +50,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )n + 254 >= (long long )v
+        value: (long long )v + i >= 0
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -60,7 +60,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )n >= (long long )i
+        value: (long long )v + n >= 1
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -70,7 +70,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )v + (long long )i >= 0
+        value: 4294967550LL >= (long long )v + i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -80,7 +80,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )v + (long long )n >= 1
+        value: 4294967550LL >= (long long )v + n
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -90,7 +90,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )v + 4294967295LL >= (long long )i
+        value: 8589934590LL >= (long long )n + i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -100,7 +100,7 @@
           line: 13
           column: 3
           function: main
-        value: (long long )v + 4294967295LL >= (long long )n
+        value: i + 4294967295LL >= n
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -110,7 +110,7 @@
           line: 13
           column: 3
           function: main
-        value: 4294967550LL >= (long long )v + (long long )i
+        value: n != 0U
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -120,7 +120,7 @@
           line: 13
           column: 3
           function: main
-        value: 4294967550LL >= (long long )v + (long long )n
+        value: n >= i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -130,7 +130,7 @@
           line: 13
           column: 3
           function: main
-        value: 8589934590LL >= (long long )n + (long long )i
+        value: v + 4294967295LL >= i
         format: c_expression
     - invariant:
         type: loop_invariant
@@ -140,7 +140,7 @@
           line: 13
           column: 3
           function: main
-        value: n != 0U
+        value: v + 4294967295LL >= n
         format: c_expression
     - invariant:
         type: loop_invariant

From ad76af79266f44a730bdbf21fd91b4748197115a Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 29 Jan 2025 16:34:13 +0200
Subject: [PATCH 10/11] Avoid unnecessary casts for unsigned arithmetic without
 overflows

---
 src/cdomains/apron/sharedFunctions.apron.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 6876c3208f..add6d2ebb9 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -268,7 +268,7 @@ struct
   let longlong = TInt(ILongLong,[])
 
   let check_for_overflows_no_further_cast (ask: Queries.ask) (e_inv: exp -> exp) cast_exp exp_plain =
-    if no_overflow ask (e_inv cast_exp) then
+    if not (ask.f (MayOverflow (e_inv cast_exp))) then
       cast_exp, exp_plain
     else (
       M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" CilType.Exp.pretty cast_exp;
@@ -278,10 +278,10 @@ struct
   let is_cast_injective_vtype vinfo = IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:longlong
 
   let rec check_for_overflows (ask: Queries.ask) (e_inv: exp -> exp) exp exp_plain =
-    if no_overflow ask (e_inv exp) then
+    if not (ask.f (MayOverflow (e_inv exp))) then
       exp, exp_plain
     else
-      match exp with
+      match exp_plain with
       | Lval (Var vinfo, NoOffset) as var when is_cast_injective_vtype vinfo ->
         let cast_var = Cilfacade.mkCast ~e:var ~newt:longlong in
         check_for_overflows_no_further_cast ask e_inv cast_var cast_var

From 78a738366586ce9d9008f70712480a4bc3f156ca Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 30 Jan 2025 13:02:18 +0200
Subject: [PATCH 11/11] Match both exp and exp_plain when constructing
 invariants

---
 src/cdomains/apron/sharedFunctions.apron.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index add6d2ebb9..3e9beb44c9 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -281,23 +281,23 @@ struct
     if not (ask.f (MayOverflow (e_inv exp))) then
       exp, exp_plain
     else
-      match exp_plain with
-      | Lval (Var vinfo, NoOffset) as var when is_cast_injective_vtype vinfo ->
+      match exp, exp_plain with
+      | Lval (Var vinfo, NoOffset) as var, _ when is_cast_injective_vtype vinfo ->
         let cast_var = Cilfacade.mkCast ~e:var ~newt:longlong in
         check_for_overflows_no_further_cast ask e_inv cast_var cast_var
-      | BinOp (op, (Const i as c), ((Lval (Var vinfo, NoOffset)) as var), _) when is_cast_injective_vtype vinfo ->
+      | BinOp (op, (Const i as c), ((Lval (Var vinfo, NoOffset)) as var), _), _ when is_cast_injective_vtype vinfo ->
         let cast_var = Cilfacade.mkCast ~e:var ~newt:longlong in
         let cast_exp_plain = BinOp (op, c, cast_var, longlong) in
         let cast_exp = Cilfacade.makeBinOp op c cast_var in
         check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
-      | BinOp (op, ((Lval (Var vinfo1, NoOffset)) as var1), ((Lval (Var vinfo2, NoOffset)) as var2), _) when is_cast_injective_vtype vinfo1 && is_cast_injective_vtype vinfo2 ->
+      | BinOp (op, ((Lval (Var vinfo1, NoOffset)) as var1), ((Lval (Var vinfo2, NoOffset)) as var2), _), BinOp (_, _, var2_plain, _) when is_cast_injective_vtype vinfo1 && is_cast_injective_vtype vinfo2 ->
         let cast_var = Cilfacade.mkCast ~e:var1 ~newt:longlong in
-        let cast_exp_plain = BinOp (op, cast_var, var2, longlong) in
+        let cast_exp_plain = BinOp (op, cast_var, var2_plain, longlong) in
         let cast_exp = Cilfacade.makeBinOp op cast_var var2 in
         check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
-      | BinOp (op, exp1, exp2, _) ->
+      | BinOp (op, exp1, exp2, _), BinOp (_, _, exp2_plain, _) ->
         let cast_exp1 = Cilfacade.mkCast ~e:exp1 ~newt:longlong in
-        let cast_exp_plain = BinOp (op, cast_exp1, exp2, longlong) in
+        let cast_exp_plain = BinOp (op, cast_exp1, exp2_plain, longlong) in
         let cast_exp = Cilfacade.makeBinOp op cast_exp1 exp2 in
         check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
       | _ ->