diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-13 10:53:15 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-13 10:53:15 +0100 |
| commit | 8f972659841ad38f6f548161b5ca3cfcbdd135cb (patch) | |
| tree | ef33c46495536c075ae940d9e08cf89302eaf83e /mppa_k1c/Asmblock.v | |
| parent | 605f0a1b6a6d4e5e9ada867baebc3e56736fe920 (diff) | |
| download | compcert-kvx-8f972659841ad38f6f548161b5ca3cfcbdd135cb.tar.gz compcert-kvx-8f972659841ad38f6f548161b5ca3cfcbdd135cb.zip | |
Enlevé la dépendance mémoire de Pcbu
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 9938b386..621ed8a7 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -1390,8 +1390,8 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) end | Pcbu bt r l => match cmpu_for_btest bt with - | (Some c, Int) => eval_branch f l rs m (Val.cmpu_bool (Mem.valid_pointer m) c rs#r (Vint (Int.repr 0))) - | (Some c, Long) => eval_branch f l rs m (Val.cmplu_bool (Mem.valid_pointer m) c rs#r (Vlong (Int64.repr 0))) + | (Some c, Int) => eval_branch f l rs m (Val_cmpu_bool c rs#r (Vint (Int.repr 0))) + | (Some c, Long) => eval_branch f l rs m (Val_cmplu_bool c rs#r (Vlong (Int64.repr 0))) | (None, _) => Stuck end |