aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
diff options
context:
space:
mode:
authornicolas.nardino <nicolas.nardino@ens-lyon.fr>2021-06-17 15:38:13 +0200
committernicolas.nardino <nicolas.nardino@ens-lyon.fr>2021-06-17 15:38:13 +0200
commit4413c27d6c6a3d69df34955d9d453c38b32174c7 (patch)
tree17e9dcfd8444dcbb54e6fa64dfbaedce8ed80ce8 /riscV
parent21278bd87e89210bcc287116f6e35fc1b52d0df2 (diff)
downloadcompcert-kvx-4413c27d6c6a3d69df34955d9d453c38b32174c7.tar.gz
compcert-kvx-4413c27d6c6a3d69df34955d9d453c38b32174c7.zip
Add option to set thresold and support for riscv
Diffstat (limited to 'riscV')
-rw-r--r--riscV/Machregsaux.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/riscV/Machregsaux.ml b/riscV/Machregsaux.ml
index 840943e7..e3e47946 100644
--- a/riscV/Machregsaux.ml
+++ b/riscV/Machregsaux.ml
@@ -18,3 +18,5 @@ let class_of_type = function
| AST.Tint | AST.Tlong -> 0
| AST.Tfloat | AST.Tsingle -> 1
| AST.Tany32 | AST.Tany64 -> assert false
+
+let nr_regs = [| 26; 32|]