diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-06 16:53:46 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-06 16:53:46 +0100 |
| commit | acb41b1af6e5e4c933e3be1b17f6e5012eca794d (patch) | |
| tree | db57a6b2543871312a952ffa2e462e35aef674e0 /riscV/OpWeights.ml | |
| parent | 29ba37cc21cedc09b20bbd8adfa0ec52c48365c0 (diff) | |
| download | compcert-kvx-acb41b1af6e5e4c933e3be1b17f6e5012eca794d.tar.gz compcert-kvx-acb41b1af6e5e4c933e3be1b17f6e5012eca794d.zip | |
cond and branches expanded
Diffstat (limited to 'riscV/OpWeights.ml')
| -rw-r--r-- | riscV/OpWeights.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml index 75a913c6..09760db9 100644 --- a/riscV/OpWeights.ml +++ b/riscV/OpWeights.ml @@ -56,7 +56,19 @@ module Rocket = | Ccompl _ | Ccomplu _ | Ccomplimm _ - | Ccompluimm _ -> 1 + | Ccompluimm _ + | CEbeqw _ + | CEbnew _ + | CEbltw _ + | CEbltuw _ + | CEbgew _ + | CEbgeuw _ + | CEbeql _ + | CEbnel _ + | CEbltl _ + | CEbltul _ + | CEbgel _ + | CEbgeul _ -> 1 | Ccompf _ | Cnotcompf _ -> 6 | Ccompfs _ |