diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-27 16:25:40 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-27 16:25:40 +0100 |
| commit | 25f47289ff5d9b497d45d3f4efbf4c5df56829a9 (patch) | |
| tree | 76220bee7e9409a2051e6d410633f8c0f08abb3e /mppa_k1c/Asmvliw.v | |
| parent | 8550881e22693a5cd5078980f3e9c23bf6f63424 (diff) | |
| download | compcert-kvx-25f47289ff5d9b497d45d3f4efbf4c5df56829a9.tar.gz compcert-kvx-25f47289ff5d9b497d45d3f4efbf4c5df56829a9.zip | |
Avancement dans Asmblockdeps.v
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 0490e502..d3349344 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -151,8 +151,8 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) := instruction ([nextblock]) or branching to a label ([goto_label]). *) (* TODO: factoriser ? *) -Definition par_nextblock size_b (rsr rsw: regset) := - rsw#PC <- (Val.offset_ptr rsr#PC size_b). +Definition par_nextblock size_b (rs: regset) := + rs#PC <- (Val.offset_ptr rs#PC size_b). (* TODO: factoriser ? *) Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) := @@ -240,7 +240,8 @@ end. Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m: mem): outcome := match parexec_wio_body bdy rs rs m m with | Next rsw mw => - let rsw := par_nextblock size_b rs rsw in + let rs := par_nextblock size_b rs in + let rsw := par_nextblock size_b rsw in parexec_control f ext rs rsw mw | Stuck => Stuck end. |