From fe7dd6cc46055dd95cf4c1c1f1936a9756876b2d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 18 Feb 2019 14:50:06 +0100
Subject: [PATCH] [kernel] Marks arrays as having their address taken when
their address is taken.
---
src/kernel_internals/typing/cabs2cil.ml | 5 +----
1 file changed, 1 insertion(+), 4 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 6cd61cd0df7..9ee2e6f4abd 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
--
GitLab