diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 09:27:11 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 09:27:11 +0200 |
| commit | 981adc51dd17dbb97572e7c27423628b5c9eada4 (patch) | |
| tree | 257aac27a72420ff7d8f1672fff8fea82becab7b /mppa_k1c/Asmvliw.v | |
| parent | 8163278174362fb8269804a7958f6e9e7878a511 (diff) | |
| parent | 92b48e2aa6d24d1ad487c1d2a3644a57966c765e (diff) | |
| download | compcert-kvx-981adc51dd17dbb97572e7c27423628b5c9eada4.tar.gz compcert-kvx-981adc51dd17dbb97572e7c27423628b5c9eada4.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-peephole
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index fb1575f9..248b8660 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -203,9 +203,7 @@ Inductive ftest: Type := (** Offsets for load and store instructions. An offset is either an immediate integer or the low part of a symbol. *) -Inductive offset : Type := - | Ofsimm (ofs: ptrofs) - | Ofslow (id: ident) (ofs: ptrofs). +Definition offset : Type := ptrofs. (** We model a subset of the K1c instruction set. In particular, we do not support floats yet. @@ -1141,15 +1139,7 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset := | PArithARRI64 n d s i => rsw#d <- (arith_eval_arri64 n rsr#d rsr#s i) end. -Definition eval_offset (ofs: offset) : res ptrofs := - match ofs with - | Ofsimm n => OK n - | Ofslow id delta => - match (Genv.symbol_address ge id delta) with - | Vptr b ofs => OK ofs - | _ => Error (msg "Asmblock.eval_offset") - end - end. +Definition eval_offset (ofs: offset) : res ptrofs := OK ofs. (** * load/store *) |