Nettoyage du traitement des signatures au return dans LTL et LTLin

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@690 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 16 insertions, 11 deletions

diff --git a/backend/LTL.v b/backend/LTL.v
index e99e016e..a082e122 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -140,7 +140,8 @@ Definition set_result_reg (s: signature) (or: option loc) (ls: locset) :=
 
 Inductive stackframe : Set :=
   | Stackframe:
-      forall (res: loc)         (**r where to store the result *)
+      forall (sig: signature)   (**r signature of call *)
+             (res: loc)         (**r where to store the result *)
              (f: function)      (**r calling function *)
              (sp: val)          (**r stack pointer in calling function *)
              (ls: locset)       (**r location state in calling function *)
@@ -164,7 +165,6 @@ Inductive state : Set :=
       state
   | Returnstate:
       forall (stack: list stackframe) (**r call stack *)
-             (sig: signature)         (**r signature of returning function *)
              (ls: locset)             (**r location state at point of return *)
              (m: mem),                (**r memory state *)
       state.
@@ -172,7 +172,13 @@ Inductive state : Set :=
 Definition parent_locset (stack: list stackframe) : locset :=
   match stack with
   | nil => Locmap.init Vundef
-  | Stackframe res f sp ls pc :: stack' => ls
+  | Stackframe sg res f sp ls pc :: stack' => ls
+  end.
+
+Definition parent_callsig (stack: list stackframe) : signature :=
+  match stack with
+  | nil => mksignature nil (Some Tint)
+  | Stackframe sg res f sp ls pc :: stack' => sg
   end.
 
 Variable ge: genv.
@@ -261,7 +267,7 @@ Inductive step: state -> trace -> state -> Prop :=
       funsig f' = sig ->
       let rs1 := parmov args (loc_arguments sig) rs in
       step (State s f sp pc rs m)
-        E0 (Callstate (Stackframe res f sp rs1 pc' :: s) f' rs1 m)
+        E0 (Callstate (Stackframe sig res f sp rs1 pc' :: s) f' rs1 m)
   | exec_Ltailcall:
       forall s f stk pc rs m sig ros args f',
       (fn_code f)!pc = Some(Ltailcall sig ros args) ->
@@ -299,7 +305,7 @@ Inductive step: state -> trace -> state -> Prop :=
       let rs1 := set_result_reg f.(fn_sig) or rs in
       let rs2 := return_regs (parent_locset s) rs1 in
       step (State s f (Vptr stk Int.zero) pc rs m)
-        E0 (Returnstate s f.(fn_sig) rs2 (Mem.free m stk))
+        E0 (Returnstate s rs2 (Mem.free m stk))
   | exec_function_internal:
       forall s f rs m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
@@ -314,12 +320,11 @@ Inductive step: state -> trace -> state -> Prop :=
       let rs1 :=
         Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in
       step (Callstate s (External ef) rs m)
-         t (Returnstate s ef.(ef_sig) rs1 m)
+         t (Returnstate s rs1 m)
   | exec_return:
       forall res f sp rs0 pc s sig rs m,
       let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in
-      step (Returnstate (Stackframe res f sp rs0 pc :: s) 
-                        sig rs m)
+      step (Returnstate (Stackframe sig res f sp rs0 pc :: s) rs m)
         E0 (State s f sp pc rs1 m).
 
 End RELSEM.
@@ -339,9 +344,9 @@ Inductive initial_state (p: program): state -> Prop :=
       initial_state p (Callstate nil f (Locmap.init Vundef) m0).
 
 Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall sig rs m r,
-      rs (R (loc_result sig)) = Vint r ->
-      final_state (Returnstate nil sig rs m) r.
+  | final_state_intro: forall rs m r,
+      rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r ->
+      final_state (Returnstate nil rs m) r.
 
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
   program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.