diff --git a/src/analyses/base.ml b/src/analyses/base.ml index f24ae36b2c..2529398939 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1613,7 +1613,7 @@ struct let set ~(man: _ man) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store = let update_variable x t y z = if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a" x.vname VD.pretty y CPA.pretty z; - let r = update_variable x t y z in (* refers to defintion that is outside of set *) + let r = update_variable x t y z in (* refers to definition that is outside of set *) if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\nresults in\n%a" x.vname VD.pretty y CPA.pretty z CPA.pretty r; r in diff --git a/src/domain/disjointDomain.ml b/src/domain/disjointDomain.ml index d8e59c4ba7..3e02c1d3a0 100644 --- a/src/domain/disjointDomain.ml +++ b/src/domain/disjointDomain.ml @@ -184,14 +184,25 @@ sig val may_be_equal: elt -> elt -> bool end -module ProjectiveSetPairwiseMeet (E: Printable.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct +module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct include ProjectiveSet (E) (B) (R) let meet m1 m2 = let meet_buckets b1 b2 acc = B.fold (fun e1 acc -> + let r1 = R.of_elt e1 in B.fold (fun e2 acc -> - if B.may_be_equal e1 e2 then + (* If they have the same representative, we use the normal meet within this bucket *) + if R.equal r1 (R.of_elt e2) then + try + let m = E.meet e1 e2 in + if not (E.is_bot m) then + add m acc + else + acc + with Lattice.Uncomparable -> + failwith (GobPretty.sprintf "Elements %a and %a are in same bucket, but meet throws!" E.pretty e1 E.pretty e2) + else if B.may_be_equal e1 e2 then add e1 (add e2 acc) else acc diff --git a/tests/regression/13-privatized/89-write-lacking-precision.c b/tests/regression/13-privatized/89-write-lacking-precision.c new file mode 100644 index 0000000000..bb35cdf6dc --- /dev/null +++ b/tests/regression/13-privatized/89-write-lacking-precision.c @@ -0,0 +1,31 @@ +// PARAM: --set ana.base.privatization write +#include +struct a { + char* b; +}; + +struct a *c; +struct a h = {""}; +struct a i = {"string"}; + +void* d(void* args) { + if (c->b) { + // Handled by privatization as a write + // Without fix (#1468) causes both h.b and i.b to become unknown string + __goblint_check(strlen(h.b) == 0); // Check h.b is still known + } +} + +int main() { + int top; + + if(top) { + c = &h; + } else { + c = &i; + } + + pthread_t t; + pthread_create(&t, 0, d, 0); + return 0; +} diff --git a/tests/regression/27-inv_invariants/23-meet-ptrs.c b/tests/regression/27-inv_invariants/23-meet-ptrs.c new file mode 100644 index 0000000000..ae089c2c3b --- /dev/null +++ b/tests/regression/27-inv_invariants/23-meet-ptrs.c @@ -0,0 +1,51 @@ +//PARAM: --enable ana.int.interval +#include +#include +#include + +int more_intricate() { + int arr[20]; + + int top; + + int i = 2; + int j = 8; + if(top) { + i = 8; + j = 9; + } + + int* imprecise1 = &arr[i]; // &arr[2..8] + int* imprecise2 = &arr[j]; // &arr[8..9] + + if(imprecise1 == imprecise2) { + __goblint_check(imprecise1 == &arr[8]); + __goblint_check(imprecise2 == &arr[8]); //TODO (Refinement should happen in both directions!) + } + + if(imprecise1 == &arr[j]) { + __goblint_check(imprecise1 == &arr[8]); + } + +} + + +int main() { + int arr[20]; + + int top; + + int i = 2; + if(top) { + i = 8; + } + + int* imprecise = &arr[i]; + + if(imprecise == &arr[2]) { + __goblint_check(imprecise == &arr[2]); + } + + more_intricate(); + return 0; +}