From 7410da727afb82d30a194f780feba300a5ba719d Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Thu, 19 Dec 2024 16:36:43 +0100 Subject: [PATCH] better test --- src/cdomains/apron/sharedFunctions.apron.ml | 11 +++++---- .../77-lin2vareq/36-relations-overflow.c | 24 +++++++++++++++++++ 2 files changed, 30 insertions(+), 5 deletions(-) create mode 100644 tests/regression/77-lin2vareq/36-relations-overflow.c diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index c277999b14..fd6c578e60 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/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 *) 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; +} +