diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-24 23:16:07 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-24 23:16:07 +0200 |
| commit | ffaf5a655456e045f116fcd6b52e4faae9c8a7d4 (patch) | |
| tree | 7aed00e816b546ef40c18a02d66b47999eb8455a /mppa_k1c/Asmblock.v | |
| parent | d872a6aea877e642c31ccb671d6ec1eb7501b57b (diff) | |
| download | compcert-kvx-ffaf5a655456e045f116fcd6b52e4faae9c8a7d4.tar.gz compcert-kvx-ffaf5a655456e045f116fcd6b52e4faae9c8a7d4.zip | |
relecture
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index ba14c451..4f825bf5 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -576,7 +576,6 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := Section RELSEM. -Variable ge: genv. (** The semantics is purely small-step and defined as a function from the current state (a register set + a memory state) @@ -713,6 +712,9 @@ FIXME: replace parameter "m" by a function corresponding to the resul of "(Mem.v *) +Variable ge: genv. + + Definition exec_arith_instr (ai: ar_instruction) (rs: bregset) (m: mem) : bregset := match ai with | PArithR n d => |