From 2845adfef0fade707ee0f150fe71e2c774bba693 Mon Sep 17 00:00:00 2001 From: Rebecca Ghidini Date: Wed, 3 Jan 2024 19:06:27 +0100 Subject: [PATCH] bug fix --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 8 ++++---- tests/regression/77-lin2vareq/11-overflow_ignored.c | 6 ++++++ 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index fd0ebf3e92..3d4af9e5cd 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -248,20 +248,20 @@ struct match t.d with | None -> t | Some t_d -> let d = EArray.copy t_d in - let subtract_const_from_var_for_single_equality const index element = + let subtract_const_from_var_for_single_equality index element = let (eq_var_opt, off2) = d.(index) in if index = var then match eq_var_opt with | None -> d.(index) <- (None, Z.(off2 + const)) - | Some eq_var -> begin if eq_var <> index then d.(index) <- (None, Z.(off2 + const)) end + | Some eq_var -> begin if eq_var <> index then d.(index) <- (eq_var_opt, Z.(off2 + const)) end else begin match eq_var_opt with | Some eq_var -> - if eq_var = var then d.(index) <- (Some eq_var, Z.(off2 - const)) + if eq_var = var then d.(index) <- (eq_var_opt, Z.(off2 - const)) | None -> () end in - EArray.iteri (subtract_const_from_var_for_single_equality const) d; {d = Some d; env = t.env} + EArray.iteri (subtract_const_from_var_for_single_equality) d; {d = Some d; env = t.env} end diff --git a/tests/regression/77-lin2vareq/11-overflow_ignored.c b/tests/regression/77-lin2vareq/11-overflow_ignored.c index a575aca6bc..2d226bc75f 100644 --- a/tests/regression/77-lin2vareq/11-overflow_ignored.c +++ b/tests/regression/77-lin2vareq/11-overflow_ignored.c @@ -11,6 +11,12 @@ int main() { __goblint_check(x == k + 1); // SUCCESS + for (int i = 0; i < 7; i++) { + x++; + k++; + } + + __goblint_check(x == k + 1); // SUCCESS return 0; }