diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 6cd61cd0df72fb115ee8edbb12bbbf1ab8c7bd68..b09617ac5eb3413608e822429cb55b652cb349cb 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1185,10 +1185,7 @@ let mkAddrOfAndMark loc ((b, off) as lval) : exp = begin match lastOffset off with | NoOffset -> (match b with - | Var vi -> - (* Do not mark arrays as having their address taken. *) - if not (isArrayType vi.vtype) then - vi.vaddrof <- true + | Var vi -> vi.vaddrof <- true | _ -> ()) | Index _ -> () | Field(fi,_) -> fi.faddrof <- true @@ -1196,15 +1193,12 @@ let mkAddrOfAndMark loc ((b, off) as lval) : exp = mkAddrOf ~loc lval (* Call only on arrays *) -let mkStartOfAndMark loc ((_b, _off) as lval) : exp = +let mkStartOfAndMark loc ((b, _off) as lval) : exp = (* Mark the vaddrof flag if b is a variable *) - (* Do not mark arrays as having their address taken. - (match b with - | Var vi -> vi.vaddrof <- true - | _ -> ()); - *) - let res = new_exp ~loc (StartOf lval) in - res + (match b with + | Var vi -> vi.vaddrof <- true + | _ -> ()); + new_exp ~loc (StartOf lval) (* Keep a set of self compinfo for composite types *) let compInfoNameEnv : (string, compinfo) H.t = H.create 113