diff options
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 69d3d0cc..c2477e66 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -160,6 +160,7 @@ Definition arith_eval (ao: arith_op) (l: list value) := | OArithRRR n, [Val v1; Val v2] => match n with | Pfcompw c => Some (Val (compare_single c v1 v2)) + | Pfcompl c => Some (Val (compare_float c v1 v2)) | Paddw => Some (Val (Val.add v1 v2)) | Psubw => Some (Val (Val.sub v1 v2)) |