diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-09-17 17:06:28 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-04-27 11:53:24 +0100 |
commit | 9a3143dad1b119250d0553562a436f5f5f57269b (patch) | |
tree | a3a874d262e7dec83f7575fd3f1a72b8342d10f6 /verilog/Conventions1.v | |
parent | 01c2e94a38f91af008e21a7be998da2db34ade03 (diff) | |
download | compcert-9a3143dad1b119250d0553562a436f5f5f57269b.tar.gz compcert-9a3143dad1b119250d0553562a436f5f5f57269b.zip |
Replace omega by lia
Diffstat (limited to 'verilog/Conventions1.v')
-rw-r--r-- | verilog/Conventions1.v | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/verilog/Conventions1.v b/verilog/Conventions1.v index fdd94239..592acd72 100644 --- a/verilog/Conventions1.v +++ b/verilog/Conventions1.v @@ -248,14 +248,14 @@ Remark loc_arguments_32_charact: In p (loc_arguments_32 tyl ofs) -> forall_rpair (loc_argument_32_charact ofs) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_32_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_32_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } induction tyl as [ | ty tyl]; simpl loc_arguments_32; intros. - contradiction. - destruct H. -+ destruct ty; subst p; simpl; omega. ++ destruct ty; subst p; simpl; lia. + apply IHtyl in H. generalize (typesize_pos ty); intros. destruct p; simpl in *. -* eapply X; eauto; omega. -* destruct H; split; eapply X; eauto; omega. +* eapply X; eauto; lia. +* destruct H; split; eapply X; eauto; lia. Qed. Remark loc_arguments_64_charact: @@ -263,7 +263,7 @@ Remark loc_arguments_64_charact: In p (loc_arguments_64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_64_charact ofs) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_64_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_64_charact ofs1) p). { destruct p; simpl; intuition eauto. } assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). @@ -280,8 +280,8 @@ Opaque list_nth_z. { intros. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H1. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } assert (B: forall ty, In p match list_nth_z float_param_regs fr with | Some ireg => One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs @@ -291,8 +291,8 @@ Opaque list_nth_z. { intros. destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H1. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } destruct a; eauto. Qed. @@ -340,3 +340,8 @@ Definition return_value_needs_normalization (t: rettype) : bool := | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true | _ => false end. + +(** Function parameters are passed in normalized form and do not need + to be re-normalized at function entry. *) + +Definition parameter_needs_normalization (t: rettype) := false. |