diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-14 11:05:36 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-14 11:05:36 +0100 |
commit | 9c6fac6cd52b824aaefac66089bf5c71e27845be (patch) | |
tree | a3724f9a2109d6de563606a231ad7c59a5b693de /riscV/Asmgenproof.v | |
parent | 804e8174a944e3d8983c077502e57113ecdda6dd (diff) | |
download | compcert-kvx-9c6fac6cd52b824aaefac66089bf5c71e27845be.tar.gz compcert-kvx-9c6fac6cd52b824aaefac66089bf5c71e27845be.zip |
rv32: 3-instruction signed divide-by-two sequence (as opposed to 4)
Diffstat (limited to 'riscV/Asmgenproof.v')
-rw-r--r-- | riscV/Asmgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 5ec57886..1f3f80d7 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -285,7 +285,7 @@ Opaque Int.eq. - apply opimm32_label; intros; exact I. - apply opimm32_label; intros; exact I. - apply opimm32_label; intros; exact I. -- destruct (Int.eq n Int.zero); TailNoLabel. +- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. |