diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-29 16:11:27 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-29 16:11:27 +0100 |
| commit | 0dc6f0aadfa95c722324b10c56768900760337a0 (patch) | |
| tree | 44a2d92e3d8c669f2da0a7aaf9d62d794e7f4314 /mppa_k1c/Asmvliw.v | |
| parent | 5f38e0401747a59a821852fdefb7b588a818bdcf (diff) | |
| download | compcert-kvx-0dc6f0aadfa95c722324b10c56768900760337a0.tar.gz compcert-kvx-0dc6f0aadfa95c722324b10c56768900760337a0.zip | |
Preuve de Jumptable dans Asmblockdeps.v
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index a6e9f04b..d553c612 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -211,6 +211,15 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) Next (rsw#RA <- (rsr#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw | Picall r => Next (rsw#RA <- (rsr#PC) #PC <- (rsr#r)) mw + | Pjumptable r tbl => + match rsr#r with + | Vint n => + match list_nth_z tbl (Int.unsigned n) with + | None => Stuck + | Some lbl => par_goto_label f lbl rsr (rsw #GPR62 <- Vundef #GPR63 <- Vundef) mw + end + | _ => Stuck + end | Pgoto s => Next (rsw#PC <- (Genv.symbol_address ge s Ptrofs.zero)) mw | Pigoto r => @@ -230,7 +239,6 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) | (None, _) => Stuck end - (** Pseudo-instructions *) | Pbuiltin ef args res => Stuck (**r treated specially below *) |