Merge branch 'master' into affineeq-refine

Author: DrMichaelPetter

src/analyses/basePriv.ml

@@ -1255,11 +1255,11 @@ struct
     else
       st
 
-  let threadenter =
+  let threadenter ask st =
     if Param.side_effect_global_init then
-      startstate_threadenter startstate
+      startstate_threadenter startstate ask st
     else
-      old_threadenter
+      {(old_threadenter ask st) with priv = W.empty ()}
 end
 
 module LockCenteredD =

src/cdomains/apron/sharedFunctions.apron.ml

@@ -170,10 +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  *)
-                    (* 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/13-privatized/96-mine-W-threadenter.c

@@ -0,0 +1,32 @@
+// PARAM: --set ana.base.privatization mine-W-noinit --enable ana.int.enums
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+void *t_fun2(void *arg) {
+  pthread_mutex_lock(&A);
+  pthread_mutex_unlock(&A); // used to spuriously publish g = 8
+  return NULL;
+}
+
+int main() {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded
+
+  pthread_mutex_lock(&A);
+  g = 8;
+  pthread_create(&id2, NULL, t_fun2, NULL); // used to pass g = 8 and W: A -> {g} to t_fun2
+  g = 0;
+  pthread_mutex_unlock(&A);
+
+  pthread_mutex_lock(&A);
+  __goblint_check(g == 0);
+  pthread_mutex_unlock(&A);
+  return 0;
+}

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;
+}
+