diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-17 08:59:15 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-17 08:59:15 +0000 |
| commit | e9704f237a400630ba45ee65779123b054dc1d6c (patch) | |
| tree | 0366049e9fc00aa99299dabbd08454c3c2b06177 /arm/Asmgenproof.v | |
| parent | f692ee29c1ea8748120ca1a4cbb4cd7f1eb2531e (diff) | |
| download | compcert-kvx-e9704f237a400630ba45ee65779123b054dc1d6c.tar.gz compcert-kvx-e9704f237a400630ba45ee65779123b054dc1d6c.zip | |
Update ARM port.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2254 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/Asmgenproof.v')
| -rw-r--r-- | arm/Asmgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index aede0da4..68990409 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -693,7 +693,7 @@ Opaque loadind. exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. econstructor; split. eapply exec_straight_trans. eexact P. apply exec_straight_one. - simpl. rewrite R; auto with asmgen. unfold Mach.chunk_of_type in A. rewrite A. + simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. split. Simpl. split. Simpl. @@ -896,7 +896,7 @@ Opaque loadind. rewrite <- H5 at 2; unfold fn_code. apply exec_straight_two with rs2 m2'. unfold exec_instr. rewrite C. fold sp. - rewrite <- (sp_val _ _ _ AG). unfold Mach.chunk_of_type in F. rewrite F. auto. + rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. simpl. auto. simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). rewrite Int.add_zero_l. simpl. unfold chunk_of_type in P. simpl in P. |