Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

2 files changed, 19 insertions, 15 deletions

diff --git a/arm/Builtins1.v b/arm/Builtins1.v
index f6e643d2..53c83d7e 100644
--- a/arm/Builtins1.v
+++ b/arm/Builtins1.v
@@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
   match b with end.
 
-Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
   match b with end.
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index c5277e8d..7016c1ee 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -104,13 +104,12 @@ Definition is_float_reg (r: mreg): bool :=
   representation with a single LDM instruction. *)
 
 Definition loc_result (s: signature) : rpair mreg :=
-  match s.(sig_res) with
-  | None => One R0
-  | Some (Tint | Tany32) => One R0
-  | Some (Tfloat | Tsingle | Tany64) => One F0
-  | Some Tlong => if Archi.big_endian
-                  then Twolong R0 R1
-                  else Twolong R1 R0
+  match proj_sig_res s with
+  | Tint | Tany32 => One R0
+  | Tfloat | Tsingle | Tany64 => One F0
+  | Tlong => if Archi.big_endian
+             then Twolong R0 R1
+             else Twolong R1 R0
   end.
 
 (** The result registers have types compatible with that given in the signature. *)
@@ -119,7 +118,7 @@ Lemma loc_result_type:
   forall sig,
   subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
 Proof.
-  intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto.
+  intros. unfold loc_result. destruct (proj_sig_res sig); destruct Archi.big_endian; auto.
 Qed.
 
 (** The result locations are caller-save registers *)
@@ -129,7 +128,7 @@ Lemma loc_result_caller_save:
   forall_rpair (fun r => is_callee_save r = false) (loc_result s).
 Proof.
   intros.
-  unfold loc_result. destruct (sig_res s) as [[]|]; destruct Archi.big_endian; simpl; auto.
+  unfold loc_result. destruct (proj_sig_res s); destruct Archi.big_endian; simpl; auto.
 Qed.
 
 (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -139,14 +138,13 @@ Lemma loc_result_pair:
   match loc_result sg with
   | One _ => True
   | Twolong r1 r2 =>
-        r1 <> r2 /\ sg.(sig_res) = Some Tlong
+        r1 <> r2 /\ proj_sig_res sg = Tlong
      /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
      /\ Archi.ptr64 = false
   end.
 Proof.
-  intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto.
-  intuition congruence.
-  intuition congruence.
+  intros; unfold loc_result; destruct (proj_sig_res sg); auto.
+  destruct Archi.big_endian; intuition congruence.
 Qed.
 
 (** The location of the result depends only on the result part of the signature *)
@@ -154,7 +152,7 @@ Qed.
 Lemma loc_result_exten:
   forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
 Proof.
-  intros. unfold loc_result. rewrite H; auto.
+  intros. unfold loc_result, proj_sig_res. rewrite H; auto.
 Qed.
 
 (** ** Location of function arguments *)
@@ -643,3 +641,9 @@ Proof.
   unfold loc_arguments.
   destruct Archi.abi; reflexivity.
 Qed.
+
+(** ** Normalization of function results *)
+
+(** No normalization needed. *)
+
+Definition return_value_needs_normalization (t: rettype) := false.