diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-31 09:26:36 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-31 09:26:36 +0200 |
| commit | dc8b24fa2dd7ede561dd75458899cf42e9be09d2 (patch) | |
| tree | 3389a4f3f07af151b5a30c0e23ed46c4cafdd98b /mppa_k1c/Op.v | |
| parent | 7c790ecd1c32b529a5e5e5977ce84cfade8e1eb6 (diff) | |
| parent | ccd2fa5638e50b5fd8308b4b0c26531f911ff087 (diff) | |
| download | compcert-kvx-dc8b24fa2dd7ede561dd75458899cf42e9be09d2.tar.gz compcert-kvx-dc8b24fa2dd7ede561dd75458899cf42e9be09d2.zip | |
Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 35fbb596..815d3958 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -100,23 +100,23 @@ Inductive operation : Type := | Onandimm (n: int) (**r [rd = ~(r1 & n)] *) | Oor (**r [rd = r1 | r2] *) | Oorimm (n: int) (**r [rd = r1 | n] *) - | Onor (**r [rd = r1 | r2] *) - | Onorimm (n: int) (**r [rd = r1 | n] *) + | Onor (**r [rd = ~(r1 | r2)] *) + | Onorimm (n: int) (**r [rd = ~(r1 | n)] *) | Oxor (**r [rd = r1 ^ r2] *) | Oxorimm (n: int) (**r [rd = r1 ^ n] *) | Onxor (**r [rd = ~(r1 ^ r2)] *) | Onxorimm (n: int) (**r [rd = ~(r1 ^ n)] *) | Onot (**r [rd = ~r1] *) - | Oandn (**r [rd = (~r1) ^ r2] *) - | Oandnimm (n: int) (**r [rd = (~r1) ^ n] *) + | Oandn (**r [rd = (~r1) & r2] *) + | Oandnimm (n: int) (**r [rd = (~r1) & n] *) | Oorn (**r [rd = (~r1) | r2] *) | Oornimm (n: int) (**r [rd = (~r1) | n] *) | Oshl (**r [rd = r1 << r2] *) | Oshlimm (n: int) (**r [rd = r1 << n] *) - | Oshr (**r [rd = r1 >> r2] (signed) *) - | Oshrimm (n: int) (**r [rd = r1 >> n] (signed) *) - | Oshru (**r [rd = r1 >> r2] (unsigned) *) - | Oshruimm (n: int) (**r [rd = r1 >> n] (unsigned) *) + | Oshr (**r [rd = r1 >>s r2] (signed) *) + | Oshrimm (n: int) (**r [rd = r1 >>s n] (signed) *) + | Oshru (**r [rd = r1 >>u r2] (unsigned) *) + | Oshruimm (n: int) (**r [rd = r1 >>x n] (unsigned) *) | Oshrximm (n: int) (**r [rd = r1 / 2^n] (signed) *) | Ororimm (n: int) (**r rotate right immediate *) | Omadd (**r [rd = rd + r1 * r2] *) @@ -158,8 +158,8 @@ Inductive operation : Type := | Onxorl (**r [rd = ~(r1 ^ r2)] *) | Onxorlimm (n: int64) (**r [rd = ~(r1 ^ n)] *) | Onotl (**r [rd = ~r1] *) - | Oandnl (**r [rd = (~r1) ^ r2] *) - | Oandnlimm (n: int64) (**r [rd = (~r1) ^ n] *) + | Oandnl (**r [rd = (~r1) & r2] *) + | Oandnlimm (n: int64) (**r [rd = (~r1) & n] *) | Oornl (**r [rd = (~r1) | r2] *) | Oornlimm (n: int64) (**r [rd = (~r1) | n] *) | Oshll (**r [rd = r1 << r2] *) |