aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Initializersproof.v
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2016-03-20 18:00:43 +0100
committerXavier Leroy <xavierleroy@users.noreply.github.com>2016-03-20 18:00:43 +0100
commit1fdca8371317e656cb08eaec3adb4596d6447e9b (patch)
tree8a5d390a4d38f4d840f516fb917eb824311a93a0 /cfrontend/Initializersproof.v
parent1396a4051caef0957ede026f3b8fab5a9b10b6bc (diff)
parent478ae4c3aeb1a31b0eec9ab7eb8fe20ec2671614 (diff)
downloadcompcert-kvx-1fdca8371317e656cb08eaec3adb4596d6447e9b.tar.gz
compcert-kvx-1fdca8371317e656cb08eaec3adb4596d6447e9b.zip
Merge pull request #93 from AbsInt/separate-compilation
This pull request implements "approach A" to separate compilation in CompCert from the paper Lightweight verification of separate compilation by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis, POPL 2016, pages 178-190 In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program. This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
Diffstat (limited to 'cfrontend/Initializersproof.v')
-rw-r--r--cfrontend/Initializersproof.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index e6fcad8c..d5f39d7d 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -649,7 +649,7 @@ Qed.
Lemma transl_init_single_size:
forall ty a data,
transl_init_single ge ty a = OK data ->
- Genv.init_data_size data = sizeof ge ty.
+ init_data_size data = sizeof ge ty.
Proof.
intros. monadInv H. destruct x0.
- monadInv EQ2.
@@ -666,7 +666,7 @@ Proof.
inv EQ2; auto.
Qed.
-Notation idlsize := Genv.init_data_list_size.
+Notation idlsize := init_data_list_size.
Remark padding_size:
forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm.