diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-07 13:38:31 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-02-07 13:38:31 +0000 |
| commit | 2594c23c95d22f838952b0b335231ba81a657b0d (patch) | |
| tree | 5e964de0b29e7f2906c453aa4690a01086c08a3f /cfrontend/Initializersproof.v | |
| parent | 25b9b003178002360d666919f2e49e7f5f4a36e2 (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/Initializersproof.v')
| -rw-r--r-- | cfrontend/Initializersproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 4d287bc..057933e 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -445,7 +445,7 @@ Proof. (* val *) destruct v; monadInv CV; constructor. (* rval *) - inv H1; rewrite H2 in CV; try congruence. eauto. + inv H1; rewrite H2 in CV; try congruence. eauto. eauto. (* addrof *) eauto. (* unop *) |