diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-02 09:04:03 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-02 09:04:03 +0200 |
| commit | fd2c2a0bdf723dce559567324711a3127ce0582e (patch) | |
| tree | f03b21a14cba984854142016733802c3ca8866b1 /mppa_k1c/Machregs.v | |
| parent | 8fb2d1a49443767ce353520ea045383430a2655e (diff) | |
| parent | 5cdc3d29983c65d1ac1d3393103037fdd87d7829 (diff) | |
| download | compcert-kvx-fd2c2a0bdf723dce559567324711a3127ce0582e.tar.gz compcert-kvx-fd2c2a0bdf723dce559567324711a3127ce0582e.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary
Diffstat (limited to 'mppa_k1c/Machregs.v')
| -rw-r--r-- | mppa_k1c/Machregs.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 2b3fb1aa..f494c67d 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -152,8 +152,7 @@ Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mre Definition destroyed_by_cond (cond: condition): list mreg := nil. -(* Definition destroyed_by_jumptable: list mreg := R5 :: nil. *) -Definition destroyed_by_jumptable: list mreg := nil. +Definition destroyed_by_jumptable: list mreg := R62 :: R63 :: nil. Fixpoint destroyed_by_clobber (cl: list string): list mreg := match cl with |