diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-09 08:32:36 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-09 08:32:36 +0200 |
| commit | c764ff8433d8d4b31228d8313aa1043cb9196d21 (patch) | |
| tree | c9c2fd260f2b06050bca4f1ef36238c8e3d89377 /aarch64/Asmblock.v | |
| parent | e28bf3a20d7448373ba9cc63bd0ac2566dafe027 (diff) | |
| download | compcert-kvx-c764ff8433d8d4b31228d8313aa1043cb9196d21.tar.gz compcert-kvx-c764ff8433d8d4b31228d8313aa1043cb9196d21.zip | |
Switch back to specific registers for specific (inlined) instruction
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 1abe7d90..5cabf324 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -445,7 +445,7 @@ Inductive ar_instruction : Type := (* PArithFR0 *) | Pfmovi (fsz : fsize) (rd : freg) (r1 : ireg0) (**r copy int reg to FP reg *) (* PArithCPPP *) - | Pcsel (rd r1 r2 : preg) (c : testcond) (**r int/float conditional move *) + | Pcsel (rd r1 r2 : ireg) (c : testcond) (**r int/float conditional move *) (* PArithAFFF *) | Pfnmul (fsz : fsize) (rd r1 r2 : freg) (**r multiply-negate *) . |