diff options
Diffstat (limited to 'kvx/NeedOp.v')
| -rw-r--r-- | kvx/NeedOp.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v index f636336d..4578b4e8 100644 --- a/kvx/NeedOp.v +++ b/kvx/NeedOp.v @@ -18,6 +18,7 @@ Require Import AST Integers Floats. Require Import Values Memory Globalenvs. Require Import Op RTL. Require Import NeedDomain. +Require Import Lia. (** Neededness analysis for RISC-V operators *) @@ -405,8 +406,8 @@ Lemma operation_is_redundant_sound: vagree v arg1' nv. Proof. intros. destruct op; cbn in *; try discriminate; inv H1; FuncInv; subst. -- apply sign_ext_redundant_sound; auto. omega. -- apply sign_ext_redundant_sound; auto. omega. +- apply sign_ext_redundant_sound; auto. lia. +- apply sign_ext_redundant_sound; auto. lia. - apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. Qed. |