aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selectionaux.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-07 21:34:14 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-07 21:34:14 +0200
commit249482aed76d209ff203f9afeeb3f10db004e8c0 (patch)
tree80efa32a68a7b993ef94751e38acb4b49f849b7d /backend/Selectionaux.ml
parent5a3d4adc631f5b5d3dc4585b7b28ea18b6faf633 (diff)
downloadcompcert-kvx-249482aed76d209ff203f9afeeb3f10db004e8c0.tar.gz
compcert-kvx-249482aed76d209ff203f9afeeb3f10db004e8c0.zip
start implementing expect as expr
Diffstat (limited to 'backend/Selectionaux.ml')
-rw-r--r--backend/Selectionaux.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml
index 26a79fd7..5a8bde8c 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -39,6 +39,7 @@ let cost_unop = function
| Osingleoflong | Osingleoflongu -> assert false
let cost_binop = function
+ | Oexpect _ -> 0
| Oadd | Osub -> 1
| Omul -> 2
| Odiv | Odivu | Omod | Omodu -> assert false