aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2021-01-30 15:53:04 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2021-01-30 15:53:04 +0100
commit716687e12509a873e469e38250ffd57ba5d011f1 (patch)
tree64cf293583b62ea5d7b05e0d1304ee74d1fe8bd2
parent18a2f80686c651dde5964098c8b76e5aa94e6340 (diff)
downloadcompcert-kvx-716687e12509a873e469e38250ffd57ba5d011f1.tar.gz
compcert-kvx-716687e12509a873e469e38250ffd57ba5d011f1.zip
fix OpWeights
-rw-r--r--riscV/OpWeights.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
index 75a913c6..2b0496fc 100644
--- a/riscV/OpWeights.ml
+++ b/riscV/OpWeights.ml
@@ -104,7 +104,7 @@ module SweRV_EH1 =
| Omul | Omulhs | Omulhu
| Omull | Omullhs | Omullhu -> [| 1 ; 0 ; 1 |]
| Odiv | Odivu | Odivl | Odivlu -> [| 0 ; 0; 0 |]
- | _ -> [| 1; 0; 0; 0 |];;
+ | _ -> [| 1; 0; 0 |];;
let non_pipelined_resources_of_op (op : operation) (nargs : int) =
match op with