diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-26 19:30:24 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-26 19:30:24 +0200 |
| commit | ae3ff874f99fcde33901ac13f4ee9ea23aa984e5 (patch) | |
| tree | 1e05ad24d293f66002436fab12ce1ec097337442 /riscV/Machregs.v | |
| parent | bfb8a3c330ae3f7cdaa64fd668a65cd102bbe749 (diff) | |
| download | compcert-kvx-ae3ff874f99fcde33901ac13f4ee9ea23aa984e5.tar.gz compcert-kvx-ae3ff874f99fcde33901ac13f4ee9ea23aa984e5.zip | |
riscV/Machregs: no printable name was associated to register X31
Diffstat (limited to 'riscV/Machregs.v')
| -rw-r--r-- | riscV/Machregs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/Machregs.v b/riscV/Machregs.v index c7d558ed..c21ea97a 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -151,7 +151,7 @@ Definition register_names := ("F16", F16) :: ("F17", F17) :: ("F18", F18) :: ("F19", F19) :: ("F20", F20) :: ("F21", F21) :: ("F22", F22) :: ("F23", F23) :: ("F24", F24) :: ("F25", F25) :: ("F26", F26) :: ("F27", F27) :: - ("F27", F27) :: ("F28", F28) :: ("F29", F29) :: ("F30", F30) :: + ("F28", F28) :: ("F29", F29) :: ("F30", F30) :: ("F31", F31) :: nil. Definition register_by_name (s: string) : option mreg := |