diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-01 22:33:11 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-01 22:33:11 +0200 |
| commit | 14d2059195b5c66cd7e77184b0e76e95147aaaa9 (patch) | |
| tree | b3842c7c7bee2ae1d40ed9be8b389a5a13645a82 /mppa_k1c/Op.v | |
| parent | 57ddece94f4c4b44e8e3127c6f5f72aaa5962250 (diff) | |
| download | compcert-kvx-14d2059195b5c66cd7e77184b0e76e95147aaaa9.tar.gz compcert-kvx-14d2059195b5c66cd7e77184b0e76e95147aaaa9.zip | |
load xs / store xs seem to work
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index b9d9cc43..5e80589b 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -705,9 +705,10 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oinsfl _ _ => (Tlong :: Tlong :: nil, Tlong) end. +(* FIXME: two Tptr ?! *) Definition type_of_addressing (addr: addressing) : list typ := match addr with - | Aindexed2XS _ => Tptr :: Tptr :: Tptr :: nil + | Aindexed2XS _ => Tptr :: Tptr :: nil | Aindexed2 => Tptr :: Tptr :: nil | Aindexed _ => Tptr :: nil | Aglobal _ _ => nil |