diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 0caf45f08d..3e715519fb 100644 --- a/src/analyses/basePriv.ml +++ b/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 = diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 112e327530..fd6c578e60 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/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 *) diff --git a/tests/regression/13-privatized/96-mine-W-threadenter.c b/tests/regression/13-privatized/96-mine-W-threadenter.c new file mode 100644 index 0000000000..ec9903b653 --- /dev/null +++ b/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 +#include + +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; +} diff --git a/tests/regression/77-lin2vareq/36-relations-overflow.c b/tests/regression/77-lin2vareq/36-relations-overflow.c new file mode 100644 index 0000000000..12997a5a3f --- /dev/null +++ b/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 + +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; +} +