diff options
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 3dce24cf..e10290fd 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -185,9 +185,15 @@ Proof. (* Ccompu *) - unfold transl_comp; TailNoLabel. (* Ccompimm *) - - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel. + - destruct (Int.eq n Int.zero); TailNoLabel. + unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel. (* Ccompuimm *) - - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel. + - unfold transl_opt_compuimm. + remember (select_comp n c0) as selcomp; destruct selcomp. + + destruct c; TailNoLabel; contradict Heqselcomp; unfold select_comp; + destruct (Int.eq n Int.zero); destruct c0; discriminate. + + unfold loadimm32; + destruct (make_immed32 n); TailNoLabel; unfold transl_comp; TailNoLabel. (* Ccompl *) - unfold transl_compl; TailNoLabel. (* Ccomplu *) |