diff options
Diffstat (limited to 'mppa_k1c/ValueAOp.v')
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 00e8a1d8..adc27010 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -204,7 +204,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omadd, v1::v2::v3::nil => add v1 (mul v2 v3) | Omaddimm n, v1::v2::nil => add v1 (mul v2 (I n)) | Omsub, v1::v2::v3::nil => sub v1 (mul v2 v3) - | Omsubimm n, v1::v2::nil => sub v1 (mul v2 (I n)) | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 | Ohighlong, v1::nil => hiword v1 @@ -254,7 +253,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omaddl, v1::v2::v3::nil => addl v1 (mull v2 v3) | Omaddlimm n, v1::v2::nil => addl v1 (mull v2 (L n)) | Omsubl, v1::v2::v3::nil => subl v1 (mull v2 v3) - | Omsublimm n, v1::v2::nil => subl v1 (mull v2 (L n)) | Onegf, v1::nil => negf v1 | Oabsf, v1::nil => absf v1 | Oaddf, v1::v2::nil => addf v1 v2 |