aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-06-25 11:33:54 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-06-25 11:33:54 +0200
commit56498b6437ea8deb89a4e1fadbbfec490b8341aa (patch)
tree0da64182d9cd7c596812098c3450ec424c4b4f12 /riscV
parent5798f56b8a8630e43dbed84a824811a5626a1503 (diff)
downloadcompcert-kvx-56498b6437ea8deb89a4e1fadbbfec490b8341aa.tar.gz
compcert-kvx-56498b6437ea8deb89a4e1fadbbfec490b8341aa.zip
adding mayundef resource_bounds (not changing perfs)
Diffstat (limited to 'riscV')
-rw-r--r--riscV/OpWeights.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
index 0a1d9ad4..a5ece6d5 100644
--- a/riscV/OpWeights.ml
+++ b/riscV/OpWeights.ml
@@ -66,7 +66,8 @@ module Rocket = struct
| OEmayundef _ -> 0
| _ -> 1
- let resources_of_op (op : operation) (nargs : int) = resource_bounds
+ let resources_of_op (op : operation) (nargs : int) =
+ match op with OEmayundef _ -> [| 0 |] | _ -> resource_bounds
let non_pipelined_resources_of_op (op : operation) (nargs : int) =
match op with