summaryrefslogtreecommitdiff
path: root/cfrontend/Initializers.v
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-07 13:38:31 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-07 13:38:31 +0000
commit2594c23c95d22f838952b0b335231ba81a657b0d (patch)
tree5e964de0b29e7f2906c453aa4690a01086c08a3f /cfrontend/Initializers.v
parent25b9b003178002360d666919f2e49e7f5f4a36e2 (diff)
Initializers: handle By_copy accesses (e.g. for &(glob.field))
C2C: insert the correct Evalof for structs; clean up unused memcpy stuff test/regression: run with interpreter test/regression: add test cas &(glob.field) to initializers.c git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1815 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Initializers.v')
-rw-r--r--cfrontend/Initializers.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index e9c40a2..9690ba8 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -58,8 +58,8 @@ Fixpoint constval (a: expr) : res val :=
end
| Evalof l ty =>
match access_mode ty with
- | By_reference => constval l
- | _ => Error(msg "dereference operation")
+ | By_reference | By_copy => constval l
+ | _ => Error(msg "dereferencing of an l-value")
end
| Eaddrof l ty =>
constval l