diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 12:27:43 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 12:27:43 +0200 |
| commit | 35febfa5b231a71234a1b32c128169352e96eaca (patch) | |
| tree | 5401681c76c8e45e9c1e6128d313851582e6fc9f /arm/Asmgenproof.v | |
| parent | 046c24d29796a3bb130c94fe464e54e8a7aa2eb3 (diff) | |
| download | compcert-kvx-35febfa5b231a71234a1b32c128169352e96eaca.tar.gz compcert-kvx-35febfa5b231a71234a1b32c128169352e96eaca.zip | |
fixes for ARM
Diffstat (limited to 'arm/Asmgenproof.v')
| -rw-r--r-- | arm/Asmgenproof.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 25f91d23..92ae524f 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -303,6 +303,7 @@ Proof. eapply tail_nolabel_trans. 2: eapply loadind_label; eauto. unfold loadind_int; TailNoLabel. eapply transl_op_label; eauto. unfold transl_load, transl_memory_access_int, transl_memory_access_float in H. + destruct t; try discriminate. destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. unfold transl_store, transl_memory_access_int, transl_memory_access_float in H. destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. @@ -618,6 +619,12 @@ Opaque loadind. split. eapply agree_set_undef_mreg; eauto. congruence. simpl; congruence. +- (* Mload notrap1 *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + +- (* Mload notrap *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + - (* Mstore *) assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. |