diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-29 14:14:46 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-29 14:14:46 +0100 |
| commit | aabfd379b2d58afc5b89dfa2d753e56354c1fccb (patch) | |
| tree | bf4a110500b85541a61a63a746076c7c2e6968d8 /aarch64/Asmgen.v | |
| parent | 350c39da5179b5b3d79357240d2bf9debc458b49 (diff) | |
| download | compcert-kvx-aabfd379b2d58afc5b89dfa2d753e56354c1fccb.tar.gz compcert-kvx-aabfd379b2d58afc5b89dfa2d753e56354c1fccb.zip | |
Bugfix in Asmgen
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 5038245a..fcd12eef 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -223,7 +223,7 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction := do r1'' <- ireg_of_preg r1'; do r2'' <- ireg_of_preg r2'; OK (Asm.Pcsel rd' r1'' r2'' c) - | FR' r1', IR' r2' => do rd' <- freg_of_preg rd; + | FR' r1', FR' r2' => do rd' <- freg_of_preg rd; do r1'' <- freg_of_preg r1'; do r2'' <- freg_of_preg r2'; OK (Asm.Pfsel rd' r1'' r2'' c) |