aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authornicolas.nardino <nicolas.nardino@ens-lyon.fr>2021-06-17 17:00:57 +0200
committernicolas.nardino <nicolas.nardino@ens-lyon.fr>2021-06-17 17:00:57 +0200
commitfae8d9b5c5f93d5eda36f800eb0ca1837b237cba (patch)
tree90a2a33ee6dfba2cd14d9dc023ccb510e3ba627c
parent4413c27d6c6a3d69df34955d9d453c38b32174c7 (diff)
downloadcompcert-kvx-fae8d9b5c5f93d5eda36f800eb0ca1837b237cba.tar.gz
compcert-kvx-fae8d9b5c5f93d5eda36f800eb0ca1837b237cba.zip
fix riscv/Machregsaux.mli
-rw-r--r--riscV/Machregsaux.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/riscV/Machregsaux.mli b/riscV/Machregsaux.mli
index 01b0f9fd..cf6d7b71 100644
--- a/riscV/Machregsaux.mli
+++ b/riscV/Machregsaux.mli
@@ -15,3 +15,5 @@
val is_scratch_register: string -> bool
val class_of_type: AST.typ -> int
+
+val nr_regs: int array