diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-07 21:34:14 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-07 21:34:14 +0200 |
| commit | 249482aed76d209ff203f9afeeb3f10db004e8c0 (patch) | |
| tree | 80efa32a68a7b993ef94751e38acb4b49f849b7d /backend/Cminortyping.v | |
| parent | 5a3d4adc631f5b5d3dc4585b7b28ea18b6faf633 (diff) | |
| download | compcert-kvx-249482aed76d209ff203f9afeeb3f10db004e8c0.tar.gz compcert-kvx-249482aed76d209ff203f9afeeb3f10db004e8c0.zip | |
start implementing expect as expr
Diffstat (limited to 'backend/Cminortyping.v')
| -rw-r--r-- | backend/Cminortyping.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v index 92ec45f2..8945cecf 100644 --- a/backend/Cminortyping.v +++ b/backend/Cminortyping.v @@ -64,6 +64,7 @@ Definition type_binop (op: binary_operation) : typ * typ * typ := | Ocmpf _ => (Tfloat, Tfloat, Tint) | Ocmpfs _ => (Tsingle, Tsingle, Tint) | Ocmpl _ | Ocmplu _ => (Tlong, Tlong, Tint) + | Oexpect ty => (ty, ty, ty) end. Module RTLtypes <: TYPE_ALGEBRA. |