diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-27 08:29:24 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-27 08:29:24 +0200 |
| commit | 24b3245cd70f1342b95d08182d6d193382f0c59e (patch) | |
| tree | baf3777cd0c75119a9113d200a495bff42b628db /aarch64/Asmgenproof.v | |
| parent | 7a2137b50bd494033a2dcda76be44e6a32e12208 (diff) | |
| download | compcert-kvx-24b3245cd70f1342b95d08182d6d193382f0c59e.tar.gz compcert-kvx-24b3245cd70f1342b95d08182d6d193382f0c59e.zip | |
Move position of n in formulation of find_instr_bblock
This way exec_header_simulation does not break (without any changes).
Depending on the base case of find_instr_bblock this may need to change
again.
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index b4765978..76f18079 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -633,15 +633,15 @@ Proof. Admitted. Lemma find_instr_bblock: - forall lb pos n bb tlb + forall n lb pos bb tlb (FINDBB: find_bblock pos lb = Some bb) (UNFOLD: unfold lb = OK tlb) (SIZE: 0 <= n < size bb), exists i, is_nth_inst bb n i /\ Asm.find_instr (pos+n) tlb = Some i. Proof. induction lb. - - intros ? ? ? ? FINDBB. inversion FINDBB. - - intros pos n bb tlb FINDBB UNFOLD SIZE. + - intros. inversion FINDBB. + - intros pos bb tlb FINDBB UNFOLD SIZE. destruct pos. + admit. + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB. @@ -650,7 +650,7 @@ Proof. apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD' & TLB)). inversion TLB. - generalize (IHlb _ n _ _ FINDBB UNFOLD'). intros IH. + generalize (IHlb _ _ _ FINDBB UNFOLD'). intros IH. destruct IH as (? & (IH_is_nth & IH_find_instr)); eauto. eexists; split. * apply IH_is_nth. |