better test

Author: DrMichaelPetter

src/cdomains/apron/sharedFunctions.apron.ml

@@ -170,11 +170,12 @@ struct
                   | exception Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported)
                   | true -> texpr1 e
                   | false -> (* Cast is not injective - we now try to establish suitable ranges manually  *)
-                    GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
-                    (* try to evaluate e by EvalInt Query *)
-                    let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported)  in
-                    (* convert response to a constant *)
-                    let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res in
+                    (* retrieving a valuerange for a non-injective cast works by a query to the value-domain with subsequent value extraction from domtuple - which should be speculative, since it is not program code *)
+                    let const,res = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
+                      (* try to evaluate e by EvalInt Query *)
+                      let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported)  in
+                      (* convert response to a constant *)
+                      IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res, res in
                     match const with
                     | Some c -> Cst (Coeff.s_of_z c) (* Got a constant value -> use it straight away *)
                     (* I gotten top, we can not guarantee injectivity *)

tests/regression/77-lin2vareq/36-relations-overflow.c

@@ -0,0 +1,24 @@
+//SKIP PARAM:  --enable ana.int.interval  --set sem.int.signed_overflow assume_none  --set ana.activated[+] lin2vareq
+
+#include <goblint.h>
+
+int nondet() {
+  int x;
+  return x;
+}
+int SIZE = 1;
+int rand;
+
+int main() {
+  unsigned int n=2,i=8;
+  n = i%(SIZE+2); //NOWARN
+
+  rand=nondet();
+
+  if (rand>5 && rand<10) {
+    n= i%(rand+2); //NOWARN
+  }
+
+  return 0;
+}
+