Merge branch 'master' into merge_master_8.13.1

PARTIAL MERGE (PARTLY BROKEN).

See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE

WARNING:
 interface of va_args and assembly sections have changed

11 files changed, 90 insertions, 89 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 293df274..8c902074 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -1004,7 +1004,7 @@ Ltac Equalities :=
   split. auto. intros. destruct B; auto. subst. auto.
 (* trace length *)
   red; intros; inv H; simpl.
-  omega.
+  lia.
   inv H3; eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 (* initial states *)
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 104bfc94..83bce915 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -545,7 +545,7 @@ module FixupHF = struct
       end
 
   let fixup_arguments dir sg =
-    if sg.sig_cc.cc_vararg then
+    if sg.sig_cc.cc_vararg <> None then
       FixupEABI.fixup_arguments dir sg
     else begin
       let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in
@@ -555,7 +555,7 @@ module FixupHF = struct
     end
 
   let fixup_result dir sg =
-    if sg.sig_cc.cc_vararg then
+    if sg.sig_cc.cc_vararg <> None then
       FixupEABI.fixup_result dir sg
 end
 
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index fd70c9ad..67cfe0ae 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -68,7 +68,7 @@ Lemma transf_function_no_overflow:
   forall f tf,
   transf_function f = OK tf -> list_length_z (fn_code tf) <= Ptrofs.max_unsigned.
 Proof.
-  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. omega.
+  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. lia.
 Qed.
 
 Lemma exec_straight_exec:
@@ -122,13 +122,13 @@ Proof.
   case (is_label lbl a).
   intro EQ; injection EQ; intro; subst c'.
   exists (pos + 1). split. auto. split.
-  replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor.
-  rewrite list_length_z_cons. generalize (list_length_z_pos c). omega.
+  replace (pos + 1 - pos) with (0 + 1) by lia. constructor. constructor.
+  rewrite list_length_z_cons. generalize (list_length_z_pos c). lia.
   intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]].
   exists pos'. split. auto. split.
-  replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega.
+  replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by lia.
   constructor. auto.
-  rewrite list_length_z_cons. omega.
+  rewrite list_length_z_cons. lia.
 Qed.
 
 (** The following lemmas show that the translation from Mach to ARM
@@ -379,8 +379,8 @@ Proof.
   split. unfold goto_label. rewrite P. rewrite H1. auto.
   split. rewrite Pregmap.gss. constructor; auto.
   rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
-  auto. omega.
-  generalize (transf_function_no_overflow _ _ H0). omega.
+  auto. lia.
+  generalize (transf_function_no_overflow _ _ H0). lia.
   intros. apply Pregmap.gso; auto.
 Qed.
 
@@ -910,11 +910,11 @@ Opaque loadind.
   simpl; reflexivity. reflexivity.
   }
   (* After the function prologue is the code for the function body *)
-  exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
+  exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor.
   intros (ofsbody & U & V).
   (* Conclusions *)
   left; exists (State rs4 m3'); split.
-  eapply exec_straight_steps_1; eauto. omega. constructor.
+  eapply exec_straight_steps_1; eauto. lia. constructor.
   econstructor; eauto. rewrite U. econstructor; eauto. 
   apply agree_nextinstr.
   apply agree_undef_regs2 with rs2.
@@ -941,7 +941,7 @@ Opaque loadind.
 
 - (* return *)
   inv STACKS. simpl in *.
-  right. split. omega. split. auto.
+  right. split. lia. split. auto.
   rewrite <- ATPC in H5. econstructor; eauto. congruence.
 Qed.
 
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index cdac697e..7a707f32 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -40,14 +40,14 @@ Lemma ireg_of_not_R14:
 Proof.
   intros. erewrite <- ireg_of_eq; eauto with asmgen.
 Qed.
-Hint Resolve ireg_of_not_R14: asmgen.
+Global Hint Resolve ireg_of_not_R14: asmgen.
 
 Lemma ireg_of_not_R14':
   forall m r, ireg_of m = OK r -> r <> IR14.
 Proof.
   intros. generalize (ireg_of_not_R14 _ _ H). congruence.
 Qed.
-Hint Resolve ireg_of_not_R14': asmgen.
+Global Hint Resolve ireg_of_not_R14': asmgen.
 
 (** [undef_flags] and [nextinstr_nf] *)
 
@@ -75,7 +75,7 @@ Proof.
   intros; red; intros; subst; discriminate.
 Qed.
 
-Hint Resolve data_if_preg if_preg_not_PC: asmgen.
+Global Hint Resolve data_if_preg if_preg_not_PC: asmgen.
 
 Lemma nextinstr_nf_inv:
   forall r rs, if_preg r = true -> (nextinstr_nf rs)#r = rs#r.
@@ -352,15 +352,15 @@ Proof.
   apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl.
   econstructor; split.
   eapply exec_straight_two. simpl; reflexivity. simpl; reflexivity. auto. auto.
-  split; intros; Simpl. simpl. f_equal. rewrite Int.zero_ext_and by omega.
+  split; intros; Simpl. simpl. f_equal. rewrite Int.zero_ext_and by lia.
   rewrite Int.and_assoc. change 65535 with (two_p 16 - 1). rewrite Int.and_idem.
   apply Int.same_bits_eq; intros.
   rewrite Int.bits_or, Int.bits_and, Int.bits_shl, Int.testbit_repr by auto.
-  rewrite Ztestbit_two_p_m1 by omega. change (Int.unsigned (Int.repr 16)) with 16.
+  rewrite Ztestbit_two_p_m1 by lia. change (Int.unsigned (Int.repr 16)) with 16.
   destruct (zlt i 16).
   rewrite andb_true_r, orb_false_r; auto.
-  rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega.
-  change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by omega. f_equal; omega.
+  rewrite andb_false_r; simpl. rewrite Int.bits_shru by lia.
+  change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by lia. f_equal; lia.
 }
   destruct (Nat.leb l1 l2).
 { (* mov - orr* *)
@@ -696,10 +696,10 @@ Lemma int_not_lt:
 Proof.
   intros. unfold Int.lt. rewrite int_signed_eq. unfold proj_sumbool.
   destruct (zlt (Int.signed y) (Int.signed x)).
-  rewrite zlt_false. rewrite zeq_false. auto. omega. omega.
+  rewrite zlt_false. rewrite zeq_false. auto. lia. lia.
   destruct (zeq (Int.signed x) (Int.signed y)).
-  rewrite zlt_false. auto. omega.
-  rewrite zlt_true. auto. omega.
+  rewrite zlt_false. auto. lia.
+  rewrite zlt_true. auto. lia.
 Qed.
 
 Lemma int_lt_not:
@@ -713,10 +713,10 @@ Lemma int_not_ltu:
 Proof.
   intros. unfold Int.ltu, Int.eq.
   destruct (zlt (Int.unsigned y) (Int.unsigned x)).
-  rewrite zlt_false. rewrite zeq_false. auto. omega. omega.
+  rewrite zlt_false. rewrite zeq_false. auto. lia. lia.
   destruct (zeq (Int.unsigned x) (Int.unsigned y)).
-  rewrite zlt_false. auto. omega.
-  rewrite zlt_true. auto. omega.
+  rewrite zlt_false. auto. lia.
+  rewrite zlt_true. auto. lia.
 Qed.
 
 Lemma int_ltu_not:
@@ -1296,16 +1296,16 @@ Local Transparent destroyed_by_op.
     rewrite Int.unsigned_repr. apply zlt_true.
     assert (Int.unsigned i <> 0).
     { red; intros; elim H. rewrite <- (Int.repr_unsigned i). rewrite H1; reflexivity. }
-    omega.
+    lia.
     change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0.
-    generalize Int.wordsize_max_unsigned; omega.
+    generalize Int.wordsize_max_unsigned; lia.
   }
   assert (LTU'': Int.ltu i Int.iwordsize = true).
   {
     generalize (Int.ltu_inv _ _ LTU). intros.
     unfold Int.ltu. rewrite Int.unsigned_repr_wordsize. apply zlt_true.
     change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0.
-    omega.
+    lia.
   }
   set (j := Int.sub Int.iwordsize i) in *.
   set (rs1 := nextinstr_nf (rs#IR14 <- (Val.shr (Vint i0) (Vint (Int.repr 31))))).
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index a4f5c29c..cd0afb7a 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -451,7 +451,7 @@ Proof.
   Int.bit_solve. destruct (zlt i0 n0).
   replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
   rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
-  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
+  rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto.
   rewrite Int.bits_not by auto. apply negb_involutive.
   rewrite H6 by auto. auto.
   econstructor; split; eauto. auto.
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index fe49a781..0ddd882f 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -309,7 +309,7 @@ Remark loc_arguments_hf_charact:
   In p (loc_arguments_hf tyl ir fr ofs) -> forall_rpair (loc_argument_charact ofs) p.
 Proof.
   assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_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_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact ofs1) p).
   { destruct p; simpl; intuition eauto. }
   induction tyl; simpl loc_arguments_hf; intros.
@@ -319,40 +319,40 @@ Proof.
   destruct (zlt ir 4); destruct H.
   subst. apply ireg_param_caller_save.
   eapply IHtyl; eauto.
-  subst. split; [omega | auto].
-  eapply Y; eauto. omega.
+  subst. split; [lia | auto].
+  eapply Y; eauto. lia.
 - (* float *)
   destruct (zlt fr 8); destruct H.
   subst. apply freg_param_caller_save.
   eapply IHtyl; eauto.
-  subst. split. apply Z.le_ge. apply align_le. omega. auto.
-  eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; omega. omega.
+  subst. split. apply Z.le_ge. apply align_le. lia. auto.
+  eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; lia. lia.
 - (* long *)
   set (ir' := align ir 2) in *.
-  assert (ofs <= align ofs 2) by (apply align_le; omega).
+  assert (ofs <= align ofs 2) by (apply align_le; lia).
   destruct (zlt ir' 4).
   destruct H. subst p. split; apply ireg_param_caller_save.
   eapply IHtyl; eauto.
-  destruct H. subst p. split; destruct Archi.big_endian; (split; [ omega | auto ]).
-  eapply Y. eapply IHtyl; eauto. omega.
+  destruct H. subst p. split; destruct Archi.big_endian; (split; [ lia | auto ]).
+  eapply Y. eapply IHtyl; eauto. lia.
 - (* single *)
   destruct (zlt fr 8); destruct H.
   subst. apply freg_param_caller_save.
   eapply IHtyl; eauto.
-  subst. split; [omega|auto].
-  eapply Y; eauto. omega.
+  subst. split; [lia|auto].
+  eapply Y; eauto. lia.
 - (* any32 *)
   destruct (zlt ir 4); destruct H.
   subst. apply ireg_param_caller_save.
   eapply IHtyl; eauto.
-  subst. split; [omega | auto].
-  eapply Y; eauto. omega.
+  subst. split; [lia | auto].
+  eapply Y; eauto. lia.
 - (* any64 *)
   destruct (zlt fr 8); destruct H.
   subst. apply freg_param_caller_save.
   eapply IHtyl; eauto.
-  subst. split. apply Z.le_ge. apply align_le. omega. auto.
-  eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; omega. omega.
+  subst. split. apply Z.le_ge. apply align_le. lia. auto.
+  eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; lia. lia.
 Qed.
 
 Remark loc_arguments_sf_charact:
@@ -360,7 +360,7 @@ Remark loc_arguments_sf_charact:
   In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Z.max 0 ofs)) p.
 Proof.
   assert (X: forall ofs1 ofs2 l, loc_argument_charact (Z.max 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Z.max 0 ofs1) l).
-  { destruct l; simpl; intros; auto. destruct sl; auto. intuition xomega. }
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition extlia. }
   assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Z.max 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Z.max 0 ofs1)) p).
   { destruct p; simpl; intuition eauto. }
   induction tyl; simpl loc_arguments_sf; intros.
@@ -370,44 +370,44 @@ Proof.
   destruct H.
   destruct (zlt ofs 0); subst p.
   apply ireg_param_caller_save.
-  split; [xomega|auto].
-  eapply Y; eauto. omega.
+  split; [extlia|auto].
+  eapply Y; eauto. lia.
 - (* float *)
   set (ofs' := align ofs 2) in *.
-  assert (ofs <= ofs') by (apply align_le; omega).
+  assert (ofs <= ofs') by (apply align_le; lia).
   destruct H.
   destruct (zlt ofs' 0); subst p.
   apply freg_param_caller_save.
-  split; [xomega|auto].
-  eapply Y. eapply IHtyl; eauto. omega.
+  split; [extlia|auto].
+  eapply Y. eapply IHtyl; eauto. lia.
 - (* long *)
   set (ofs' := align ofs 2) in *.
-  assert (ofs <= ofs') by (apply align_le; omega).
+  assert (ofs <= ofs') by (apply align_le; lia).
   destruct H.
   destruct (zlt ofs' 0); subst p.
   split; apply ireg_param_caller_save.
-  split; destruct Archi.big_endian; (split; [xomega|auto]).
-  eapply Y. eapply IHtyl; eauto. omega.
+  split; destruct Archi.big_endian; (split; [extlia|auto]).
+  eapply Y. eapply IHtyl; eauto. lia.
 - (* single *)
   destruct H.
   destruct (zlt ofs 0); subst p.
   apply freg_param_caller_save.
-  split; [xomega|auto].
-  eapply Y; eauto. omega.
+  split; [extlia|auto].
+  eapply Y; eauto. lia.
 - (* any32 *)
   destruct H.
   destruct (zlt ofs 0); subst p.
   apply ireg_param_caller_save.
-  split; [xomega|auto].
-  eapply Y; eauto. omega.
+  split; [extlia|auto].
+  eapply Y; eauto. lia.
 - (* any64 *)
   set (ofs' := align ofs 2) in *.
-  assert (ofs <= ofs') by (apply align_le; omega).
+  assert (ofs <= ofs') by (apply align_le; lia).
   destruct H.
   destruct (zlt ofs' 0); subst p.
   apply freg_param_caller_save.
-  split; [xomega|auto].
-  eapply Y. eapply IHtyl; eauto. omega.
+  split; [extlia|auto].
+  eapply Y. eapply IHtyl; eauto. lia.
 Qed.
 
 Lemma loc_arguments_acceptable:
@@ -427,7 +427,7 @@ Proof.
   destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto.
 Qed.
 
-Hint Resolve loc_arguments_acceptable: locs.
+Global Hint Resolve loc_arguments_acceptable: locs.
 
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
@@ -436,8 +436,9 @@ Proof.
   destruct Archi.abi; reflexivity.
 Qed.
 
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
 
 (** No normalization needed. *)
 
 Definition return_value_needs_normalization (t: rettype) := false.
+Definition parameter_needs_normalization (t: rettype) := false.
diff --git a/arm/NeedOp.v b/arm/NeedOp.v
index c70c7e40..23e8f047 100644
--- a/arm/NeedOp.v
+++ b/arm/NeedOp.v
@@ -198,8 +198,8 @@ Lemma operation_is_redundant_sound:
   vagree v arg1' nv.
 Proof.
   intros. destruct op; simpl 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.
diff --git a/arm/Op.v b/arm/Op.v
index ff5fe815..68f6662d 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -558,10 +558,10 @@ End SOUNDNESS.
 Program Definition mk_shift_amount (n: int) : shift_amount :=
   {| s_amount := Int.modu n Int.iwordsize; s_range := _ |}.
 Next Obligation.
-  assert (0 <= Z.modulo (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega.
+  assert (0 <= Z.modulo (Int.unsigned n) 32 < 32). apply Z_mod_lt. lia.
   unfold Int.ltu, Int.modu. change (Int.unsigned Int.iwordsize) with 32.
-  rewrite Int.unsigned_repr. apply zlt_true. omega.
-  assert (32 < Int.max_unsigned). compute; auto. omega.
+  rewrite Int.unsigned_repr. apply zlt_true. lia.
+  assert (32 < Int.max_unsigned). compute; auto. lia.
 Qed.
 
 Lemma mk_shift_amount_eq:
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 56534c04..e4e606bc 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -757,7 +757,7 @@ Qed.
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
 Proof.
   red; intros until x. unfold cast8unsigned.
-  rewrite Val.zero_ext_and. apply eval_andimm. omega.
+  rewrite Val.zero_ext_and. apply eval_andimm. lia.
 Qed.
 
 Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
@@ -770,7 +770,7 @@ Qed.
 Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
 Proof.
   red; intros until x. unfold cast8unsigned.
-  rewrite Val.zero_ext_and. apply eval_andimm. omega.
+  rewrite Val.zero_ext_and. apply eval_andimm. lia.
 Qed.
 
 Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v
index 462d83ad..f6e01e0c 100644
--- a/arm/Stacklayout.v
+++ b/arm/Stacklayout.v
@@ -72,12 +72,12 @@ Local Opaque Z.add Z.mul sepconj range.
   set (ocs := ol + 4 * b.(bound_local));
   set (ostkdata := align (size_callee_save_area b ocs) 8).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= olink) by (unfold olink; omega).
-  assert (olink <= ora) by (unfold ora; omega).
-  assert (ora + 4 <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; omega).
+  assert (0 <= olink) by (unfold olink; lia).
+  assert (olink <= ora) by (unfold ora; lia).
+  assert (ora + 4 <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by apply size_callee_save_area_incr.
-  assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; omega).
+  assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; lia).
 (* Reorder as:
      outgoing
      back link
@@ -89,11 +89,11 @@ Local Opaque Z.add Z.mul sepconj range.
   rewrite sep_swap34.
 (* Apply range_split and range_split2 repeatedly *)
   unfold fe_ofs_arg.
-  apply range_split. omega.
-  apply range_split. omega.
-  apply range_split_2. fold ol; omega. omega.
-  apply range_split. omega.
-  apply range_drop_right with ostkdata. omega.
+  apply range_split. lia.
+  apply range_split. lia.
+  apply range_split_2. fold ol; lia. lia.
+  apply range_split. lia.
+  apply range_drop_right with ostkdata. lia.
   eapply sep_drop2. eexact H.
 Qed.
 
@@ -109,13 +109,13 @@ Proof.
   set (ocs := ol + 4 * b.(bound_local));
   set (ostkdata := align (size_callee_save_area b ocs) 8).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= olink) by (unfold olink; omega).
-  assert (olink <= ora) by (unfold ora; omega).
-  assert (ora + 4 <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; omega).
+  assert (0 <= olink) by (unfold olink; lia).
+  assert (olink <= ora) by (unfold ora; lia).
+  assert (ora + 4 <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by apply size_callee_save_area_incr.
-  assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; omega).
-  split. omega. apply align_le; omega.
+  assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; lia).
+  split. lia. apply align_le; lia.
 Qed.
 
 Lemma frame_env_aligned:
@@ -134,7 +134,7 @@ Proof.
   set (ocs := ol + 4 * b.(bound_local));
   set (ostkdata := align (size_callee_save_area b ocs) 8).
   split. apply Z.divide_0_r.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
   unfold ora, olink; auto using Z.divide_mul_l, Z.divide_add_r, Z.divide_refl.
 Qed.
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 839530c6..9269dd29 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -150,9 +150,9 @@ struct
     | Section_data(i, true) ->
          failwith "_Thread_local unsupported on this platform"
     | Section_data(i, false) | Section_small_data(i) ->
-      if i then ".data" else common_section ()
+        variable_section ~sec:".data" ~bss:".bss" i
     | Section_const i | Section_small_const i ->
-      if i || (not !Clflags.option_fcommon) then ".section	.rodata" else "COMM"
+        variable_section ~sec:".section	.rodata" i
     | Section_string -> ".section	.rodata"
     | Section_literal -> ".text"
     | Section_jumptable -> ".text"