diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-22 18:40:31 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-22 18:40:31 +0200 |
| commit | bdf9fe65ecb41bca4700eab3109da274a1b47d4b (patch) | |
| tree | 8605769efd82667406268b7faa479cce404ec242 /aarch64 | |
| parent | 958988385d5956577fbad819b6466b36df6a4d1c (diff) | |
| download | compcert-kvx-bdf9fe65ecb41bca4700eab3109da274a1b47d4b.tar.gz compcert-kvx-bdf9fe65ecb41bca4700eab3109da274a1b47d4b.zip | |
Remove trailing whitespace
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asmgenproof.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 55ff066f..f0b45013 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -90,11 +90,11 @@ Proof. Qed. Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop := - | is_nth_label l: - list_nth_z (header bb) n = Some l -> + | is_nth_label l: + list_nth_z (header bb) n = Some l -> i = Asm.Plabel l -> is_nth_inst bb n i - | is_nth_basic bi: + | is_nth_basic bi: list_nth_z (body bb) (n - list_length_z (header bb)) = Some bi -> basic_to_instruction bi = OK i -> is_nth_inst bb n i @@ -105,7 +105,7 @@ Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop := is_nth_inst bb n i. Lemma find_instr_bblock pos n lb tlb bb: - find_bblock pos lb = Some bb -> + find_bblock pos lb = Some bb -> unfold lb = OK tlb -> 0 <= n < size bb -> exists i, is_nth_inst bb n i /\ Asm.find_instr (pos+n) tlb = Some i. @@ -596,9 +596,9 @@ Proof. - apply senv_preserved. - eexact transf_initial_states. - eexact transf_final_states. - - (* TODO step_simulation *) + - (* TODO step_simulation *) unfold match_states. - simpl; intros; subst; eexists; split; eauto. + simpl; intros; subst; eexists; split; eauto. eapply step_simulation; eauto. Qed. |