aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cabs.v
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-01-24 10:29:30 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-01-24 10:29:30 +0100
commitd60b593c8b1d19a4adfdadaeeaa93aa10b9dba53 (patch)
tree838eef3aa4f09efd467971a51e6c76d49ebb8a59 /cparser/Cabs.v
parent47e818992372c1480b1052b64728a33d758637cf (diff)
downloadcompcert-kvx-d60b593c8b1d19a4adfdadaeeaa93aa10b9dba53.tar.gz
compcert-kvx-d60b593c8b1d19a4adfdadaeeaa93aa10b9dba53.zip
New version to support designators.
The c standard allows member designators for offsetof. The current implementation works by recursively combining the offset of each of the member designators. For array access the size of the subtypes is multiplied by the index and for members the offset of the member is calculated. Bug 20765
Diffstat (limited to 'cparser/Cabs.v')
-rw-r--r--cparser/Cabs.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Cabs.v b/cparser/Cabs.v
index 355c748e..b3e4ffda 100644
--- a/cparser/Cabs.v
+++ b/cparser/Cabs.v
@@ -142,7 +142,7 @@ with expression :=
(* Non-standard *)
| EXPR_ALIGNOF : expression -> expression
| TYPE_ALIGNOF : (list spec_elem * decl_type) -> expression
- | BUILTIN_OFFSETOF : (list spec_elem * decl_type) -> string -> expression
+ | BUILTIN_OFFSETOF : (list spec_elem * decl_type) -> list initwhat -> expression
with constant :=
(* The string is the textual representation of the constant in