diff options
Diffstat (limited to 'ia32/Asmgenproof1.v')
| -rw-r--r-- | ia32/Asmgenproof1.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 4effe7c9..05b3176a 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -1312,6 +1312,10 @@ Transparent destroyed_by_op. (* lea *) exploit transl_addressing_mode_32_correct; eauto. intros EA. TranslOp. rewrite nextinstr_inv; auto with asmgen. rewrite Pregmap.gss. rewrite normalize_addrmode_32_correct; auto. +(* mullhs *) + apply SAME. TranslOp. destruct H1. Simplifs. +(* mullhu *) + apply SAME. TranslOp. destruct H1. Simplifs. (* divl *) apply SAME. exploit (divls_modls_exists (rs RAX) (rs RCX)). left; congruence. |