diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-08-13 16:40:26 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-13 16:41:48 +0100 |
| commit | b4aa578616acaab35e8c5c8ca7f58cc971d0baf5 (patch) | |
| tree | ebff45c35639d74fd4e0ccac5be17995d429630e /src/translation/HTLgenspec.v | |
| parent | 8e0838b04a76f64342b570e22a1c0447c85ecd64 (diff) | |
| download | vericert-kvx-b4aa578616acaab35e8c5c8ca7f58cc971d0baf5.tar.gz vericert-kvx-b4aa578616acaab35e8c5c8ca7f58cc971d0baf5.zip | |
Finished all the proofsv1.0.0
Removed support for case statements temporarily.
Diffstat (limited to 'src/translation/HTLgenspec.v')
| -rw-r--r-- | src/translation/HTLgenspec.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 93d5612..541f9fa 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -147,11 +147,11 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - Z.pos n <= Int.max_unsigned -> translate_arr_access mem addr args stk s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) - (state_goto st n) -| tr_instr_Ijumptable : + (state_goto st n). +(*| tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> - tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)). + tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*) Hint Constructors tr_instr : htlspec. Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) @@ -446,7 +446,7 @@ Proof. - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. congruence. - - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. + (*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*) Qed. Hint Resolve transf_instr_freshreg_trans : htlspec. @@ -551,12 +551,12 @@ Proof. eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + (*+ destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + inversion H2. * inversion H14. constructor. congruence. * apply in_map with (f := fst) in H14. contradiction. - + *) + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + inversion H2. |