diff options
Diffstat (limited to 'aarch64/ValueAOp.v')
-rw-r--r-- | aarch64/ValueAOp.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/aarch64/ValueAOp.v b/aarch64/ValueAOp.v index e0d98c85..e6a60d4e 100644 --- a/aarch64/ValueAOp.v +++ b/aarch64/ValueAOp.v @@ -96,8 +96,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omul, v1::v2::nil => mul v1 v2 | Omuladd, v1::v2::v3::nil => add v1 (mul v2 v3) | Omulsub, v1::v2::v3::nil => sub v1 (mul v2 v3) - | Odiv, v1::v2::nil => divs v1 v2 - | Odivu, v1::v2::nil => divu v1 v2 + | Odiv, v1::v2::nil => divs_total v1 v2 + | Odivu, v1::v2::nil => divu_total v1 v2 | Oand, v1::v2::nil => and v1 v2 | Oandshift s a, v1::v2::nil => and v1 (eval_static_shift s v2 a) | Oandimm n, v1::nil => and v1 (I n) @@ -145,8 +145,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omullsub, v1::v2::v3::nil => subl v1 (mull v2 v3) | Omullhs, v1::v2::nil => mullhs v1 v2 | Omullhu, v1::v2::nil => mullhu v1 v2 - | Odivl, v1::v2::nil => divls v1 v2 - | Odivlu, v1::v2::nil => divlu v1 v2 + | Odivl, v1::v2::nil => divls_total v1 v2 + | Odivlu, v1::v2::nil => divlu_total v1 v2 | Oandl, v1::v2::nil => andl v1 v2 | Oandlshift s a, v1::v2::nil => andl v1 (eval_static_shiftl s v2 a) | Oandlimm n, v1::nil => andl v1 (L n) @@ -191,20 +191,20 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoffloat, v1::nil => singleoffloat v1 | Ofloatofsingle, v1::nil => floatofsingle v1 - | Ointoffloat, v1::nil => intoffloat v1 - | Ointuoffloat, v1::nil => intuoffloat v1 + | Ointoffloat, v1::nil => intoffloat_total v1 + | Ointuoffloat, v1::nil => intuoffloat_total v1 | Ofloatofint, v1::nil => floatofint v1 | Ofloatofintu, v1::nil => floatofintu v1 - | Ointofsingle, v1::nil => intofsingle v1 - | Ointuofsingle, v1::nil => intuofsingle v1 + | Ointofsingle, v1::nil => intofsingle_total v1 + | Ointuofsingle, v1::nil => intuofsingle_total v1 | Osingleofint, v1::nil => singleofint v1 | Osingleofintu, v1::nil => singleofintu v1 - | Olongoffloat, v1::nil => longoffloat v1 - | Olonguoffloat, v1::nil => longuoffloat v1 + | Olongoffloat, v1::nil => longoffloat_total v1 + | Olonguoffloat, v1::nil => longuoffloat_total v1 | Ofloatoflong, v1::nil => floatoflong v1 | Ofloatoflongu, v1::nil => floatoflongu v1 - | Olongofsingle, v1::nil => longofsingle v1 - | Olonguofsingle, v1::nil => longuofsingle v1 + | Olongofsingle, v1::nil => longofsingle_total v1 + | Olonguofsingle, v1::nil => longuofsingle_total v1 | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 |