diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-07-30 11:33:51 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-07-30 11:33:51 +0200 |
| commit | 5b4560bd853cbcf1ef195da1b625f37609ec00ec (patch) | |
| tree | 985a9b244ccb9a9a7b3370f72a841d170ad824c0 /mppa_k1c/Asmblock.v | |
| parent | 211382d21013c038c3c716454fcfa5a375dba8ba (diff) | |
| download | compcert-kvx-5b4560bd853cbcf1ef195da1b625f37609ec00ec.tar.gz compcert-kvx-5b4560bd853cbcf1ef195da1b625f37609ec00ec.zip | |
(#139) - Quelques renommages
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index ddb7ce7d..0a25e81a 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -286,7 +286,7 @@ Definition exec_store_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: (** * basic instructions *) -Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := parexec_basic_instr ge bi rs rs m m. +Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := bstep ge bi rs rs m m. Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := match body with |