diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index fd52d099bf..ccc83e7d18 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -112,14 +112,18 @@ struct r ) | Mem (Lval lv), off -> - let lvals = eval_lv ~man st (Mem (Lval lv), off) in - let res = AD.fold (fun a acc -> + (* Underlying lvals (may have offsets themselves), e.g., for struct members NOT including any offset appended to outer Mem *) + let lvals = eval_lv ~man st (Mem (Lval lv), NoOffset) in + (* Additional offset of value being refined in Addr Offset type *) + let original_offset = convert_offset ~man st off in + let res = AD.fold (fun base_a acc -> Option.bind acc (fun acc -> - match a with - | Addr (base, _) as orig -> - let (a:VD.t) = Address (AD.singleton (AD.Addr.of_var base)) in - if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty a; - let st = set' lv a st in + match base_a with + | Addr _ -> + let (lval_a:VD.t) = Address (AD.singleton base_a) in + if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty lval_a; + let st = set' lv lval_a st in + let orig = AD.Addr.add_offset base_a original_offset in let old_val = get ~man st (AD.singleton orig) None in let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *) (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *) diff --git a/tests/regression/03-practical/36-struct-ptr.c b/tests/regression/03-practical/36-struct-ptr.c new file mode 100644 index 0000000000..e96a7f7966 --- /dev/null +++ b/tests/regression/03-practical/36-struct-ptr.c @@ -0,0 +1,20 @@ +#include +struct aws_al { + unsigned long current_size; +}; + +struct aws_pq { + int pred; + struct aws_al container; +}; + +int main() { + struct aws_pq queue = { 0, { 0}}; + struct aws_al *const list = &queue.container; + + if (list->current_size == 0UL) { + if (list->current_size == 0UL) { + __goblint_check(1); //REACHABLE + } + } +}