diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 10:53:48 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 10:53:48 +0200 |
| commit | 89a54eee40305a61d1c1c0b9c5e6ba039592507b (patch) | |
| tree | 83cf2236e0cc161551cc025af531803547654270 /mppa_k1c/Asm.v | |
| parent | 8bdfa912a9ba8cee569cb40bf2ec4c584095e402 (diff) | |
| download | compcert-kvx-89a54eee40305a61d1c1c0b9c5e6ba039592507b.tar.gz compcert-kvx-89a54eee40305a61d1c1c0b9c5e6ba039592507b.zip | |
MPPA - Onegf
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index b988a156..db2f9ee2 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -286,8 +286,8 @@ Inductive instruction : Type := *)| Pfsd (rd: freg) (ra: ireg) (ofs: offset) (**r store 64-bit float *) (*| Pfsd_a (rd: freg) (ra: ireg) (ofs: offset) (**r store any64 *) - | Pfnegd (rd: freg) (rs: freg) (**r negation *) - | Pfabsd (rd: freg) (rs: freg) (**r absolute value *) +*)| Pfnegd (rd: freg) (rs: freg) (**r negation *) +(*| Pfabsd (rd: freg) (rs: freg) (**r absolute value *) | Pfaddd (rd: freg) (rs1 rs2: freg) (**r addition *) | Pfsubd (rd: freg) (rs1 rs2: freg) (**r subtraction *) @@ -898,9 +898,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (*| Pfsd_a s a ofs => exec_store Many64 rs m s a ofs - | Pfnegd d s => +*)| Pfnegd d s => Next (nextinstr (rs#d <- (Val.negf rs#s))) m - | Pfabsd d s => +(*| Pfabsd d s => Next (nextinstr (rs#d <- (Val.absf rs#s))) m | Pfaddd d s1 s2 => |