diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-06-16 06:56:02 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-06-16 06:56:02 +0000 |
commit | b40e056328e183522b50c68aefdbff057bca29cc (patch) | |
tree | b05fd2f0490e979e68ea06e1931bfcfba9b35771 /cfrontend/Initializersproof.v | |
parent | 0648e79b98cc8d79e1942d15dbf05ba7b9eaaa8c (diff) | |
download | compcert-b40e056328e183522b50c68aefdbff057bca29cc.tar.gz compcert-b40e056328e183522b50c68aefdbff057bca29cc.zip |
Merge of the "princeton" branch:
- Define type "block" as "positive" instead of "Z".
- Strengthen mem_unchanged_on so that the permissions are identical,
instead of possibly increasing.
- Move mem_unchanged_on from Events to Memory.Mem.
- Define it in terms of mem_contents rather than in terms of Mem.load.
- ExportClight: try to name temporaries introduced by SimplExpr
- SimplExpr: avoid reusing temporaries between different functions,
instead, thread a single generator through all functions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Initializersproof.v')
-rw-r--r-- | cfrontend/Initializersproof.v | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 2f29514b..f3de05c1 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -334,17 +334,13 @@ Qed. (** * Soundness of the compile-time evaluator *) (** A global environment [ge] induces a memory injection mapping - our symbolic pointers [Vptr (Zpos id) ofs] to run-time pointers + our symbolic pointers [Vptr id ofs] to run-time pointers [Vptr b ofs] where [Genv.find_symbol ge id = Some b]. *) Definition inj (b: block) := - match b with - | Zpos id => - match Genv.find_symbol ge id with - | Some b' => Some (b', 0) - | None => None - end - | _ => None + match Genv.find_symbol ge b with + | Some b' => Some (b', 0) + | None => None end. Lemma mem_empty_not_valid_pointer: @@ -512,11 +508,11 @@ Proof. destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. (* pointer *) - unfold inj in H. destruct b1; try discriminate. - assert (data = Init_addrof p ofs1 /\ chunk = Mint32). + unfold inj in H. + assert (data = Init_addrof b1 ofs1 /\ chunk = Mint32). destruct ty; inv EQ2; inv H2. destruct i; inv H5. intuition congruence. auto. - destruct H4; subst. destruct (Genv.find_symbol ge p); inv H. + destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H. rewrite Int.add_zero in H3. auto. (* undef *) discriminate. @@ -538,7 +534,6 @@ Proof. destruct ty; inv EQ2; reflexivity. destruct ty; try discriminate. destruct f0; inv EQ2; reflexivity. - destruct b; try discriminate. destruct ty; try discriminate. destruct i0; inv EQ2; reflexivity. inv EQ2; reflexivity. |