summaryrefslogtreecommitdiff
path: root/cfrontend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-08-18 09:58:24 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-08-18 09:58:24 +0000
commit6f9b68c8de22fe540bfe85c2fabec4b967c6a80d (patch)
treebcdc970a7cd51c9edc74cfe2d428b7d2f7205b61 /cfrontend
parentdcaf93a7432304b3479ed191607aa4cd2966baf3 (diff)
Removed useless constraints on return type at Sreturn instructions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/Clight.v1
-rw-r--r--cfrontend/Cminorgenproof.v2
-rw-r--r--cfrontend/Csem.v2
-rw-r--r--cfrontend/Csharpminor.v2
-rw-r--r--cfrontend/Cshmgenproof.v6
-rw-r--r--cfrontend/Cstrategy.v43
-rw-r--r--cfrontend/SimplExprproof.v5
7 files changed, 25 insertions, 36 deletions
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 4cc97ab..4f4123e 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -533,7 +533,6 @@ Inductive step: state -> trace -> state -> Prop :=
E0 (State f Sskip k e le m)
| step_return_0: forall f k e le m m',
- f.(fn_return) = Tvoid ->
Mem.free_list m (blocks_of_env e) = Some m' ->
step (State f (Sreturn None) k e le m)
E0 (Returnstate Vundef (call_cont k) m')
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index e28228a..5b2ad9b 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -2965,7 +2965,7 @@ Proof.
eapply external_call_nextblock_incr; eauto.
eapply external_call_nextblock_incr; eauto.
-(* return none *)
+(* return *)
inv MK. simpl.
left; econstructor; split.
apply plus_one. econstructor; eauto.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 2858e64..3f29915 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -1092,12 +1092,10 @@ Inductive sstep: state -> trace -> state -> Prop :=
E0 (State f (Sfor Sskip a2 a3 s) k e m)
| step_return_0: forall f k e m m',
- f.(fn_return) = Tvoid ->
Mem.free_list m (blocks_of_env e) = Some m' ->
sstep (State f (Sreturn None) k e m)
E0 (Returnstate Vundef (call_cont k) m')
| step_return_1: forall f x k e m,
- f.(fn_return) <> Tvoid ->
sstep (State f (Sreturn (Some x)) k e m)
E0 (ExprState f x (Kreturn k) e m)
| step_return_2: forall f v1 ty k e m v2 m',
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 1a362e3..2f05678 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -512,12 +512,10 @@ Inductive step: state -> trace -> state -> Prop :=
E0 (State f (seq_of_lbl_stmt (select_switch n cases)) k e le m)
| step_return_0: forall f k e le m m',
- f.(fn_return) = None ->
Mem.free_list m (blocks_of_env e) = Some m' ->
step (State f (Sreturn None) k e le m)
E0 (Returnstate Vundef (call_cont k) m')
| step_return_1: forall f a k e le m v m',
- f.(fn_return) <> None ->
eval_expr e le m a v ->
Mem.free_list m (blocks_of_env e) = Some m' ->
step (State f (Sreturn (Some a)) k e le m)
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 02fab6f..4784e1e 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -1691,7 +1691,7 @@ Proof.
(* return none *)
monadInv TR. inv MTR.
econstructor; split.
- apply plus_one. constructor. monadInv TRF. simpl. rewrite H. auto.
+ apply plus_one. constructor.
eapply match_env_free_blocks; eauto.
econstructor; eauto.
eapply match_cont_call_cont. eauto.
@@ -1699,9 +1699,11 @@ Proof.
(* return some *)
monadInv TR. inv MTR.
econstructor; split.
- apply plus_one. constructor. monadInv TRF. simpl.
+ apply plus_one. constructor.
+(* monadInv TRF. simpl.
unfold opttyp_of_type. destruct (Clight.fn_return f); try congruence.
inv H0. inv H3. inv H3.
+*)
eapply make_cast_correct. eapply transl_expr_correct; eauto. eauto.
eapply match_env_free_blocks; eauto.
econstructor; eauto.
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 3d81899..ad99162 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -1971,11 +1971,13 @@ Lemma bigstep_to_steps:
/\(forall e m s t m' out,
exec_stmt e m s t m' out ->
forall f k,
+(*
match out with
| Out_return None => fn_return f = Tvoid
| Out_return (Some(v, ty)) => fn_return f <> Tvoid
| _ => True
end ->
+*)
exists S,
star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S)
/\(forall m fd args t m' res,
@@ -2176,7 +2178,7 @@ Proof.
(* return some *)
econstructor; split.
- eapply star_left. right; apply step_return_1. auto.
+ eapply star_left. right; apply step_return_1.
eapply H0. traceEq.
econstructor; eauto.
@@ -2194,7 +2196,7 @@ Proof.
constructor.
(* while stop *)
- destruct (H3 f (Kwhile2 a s k)) as [S1 [A1 B1]]. inv H4; auto.
+ destruct (H3 f (Kwhile2 a s k)) as [S1 [A1 B1]].
set (S2 :=
match out' with
| Out_break => State f Sskip k e m2
@@ -2212,7 +2214,7 @@ Proof.
unfold S2. inversion H4; subst. constructor. inv B1; econstructor; eauto.
(* while loop *)
- destruct (H3 f (Kwhile2 a s k)) as [S1 [A1 B1]]. inv H4; auto.
+ destruct (H3 f (Kwhile2 a s k)) as [S1 [A1 B1]].
destruct (H6 f k) as [S2 [A2 B2]]; auto.
exists S2; split.
eapply star_left. right; apply step_while.
@@ -2226,7 +2228,7 @@ Proof.
auto.
(* dowhile false *)
- destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. inv H1; auto.
+ destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]].
exists (State f Sskip k e m2); split.
eapply star_left. right; constructor.
eapply star_trans. eexact A1.
@@ -2238,7 +2240,7 @@ Proof.
constructor.
(* dowhile stop *)
- destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. inv H1; auto.
+ destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]].
set (S2 :=
match out1 with
| Out_break => State f Sskip k e m1
@@ -2254,7 +2256,7 @@ Proof.
unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto.
(* dowhile loop *)
- destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. inv H1; auto.
+ destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]].
destruct (H6 f k) as [S2 [A2 B2]]; auto.
exists S2; split.
eapply star_left. right; constructor.
@@ -2269,7 +2271,7 @@ Proof.
(* for start *)
assert (a1 = Sskip \/ a1 <> Sskip). destruct a1; auto; right; congruence.
- destruct H4.
+ destruct H3.
subst a1. inv H. apply H2; auto.
destruct (H0 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]; auto. inv B1.
destruct (H2 f k) as [S2 [A2 B2]]; auto.
@@ -2288,7 +2290,7 @@ Proof.
constructor.
(* for stop *)
- destruct (H3 f (Kfor3 a2 a3 s k)) as [S1 [A1 B1]]. inv H4; auto.
+ destruct (H3 f (Kfor3 a2 a3 s k)) as [S1 [A1 B1]].
set (S2 :=
match out1 with
| Out_break => State f Sskip k e m2
@@ -2306,7 +2308,7 @@ Proof.
unfold S2. inversion H4; subst. constructor. inv B1; econstructor; eauto.
(* for loop *)
- destruct (H3 f (Kfor3 a2 a3 s k)) as [S1 [A1 B1]]. inv H4; auto.
+ destruct (H3 f (Kfor3 a2 a3 s k)) as [S1 [A1 B1]].
destruct (H6 f (Kfor4 a2 a3 s k)) as [S2 [A2 B2]]; auto. inv B2.
destruct (H8 f k) as [S3 [A3 B3]]; auto.
exists S3; split.
@@ -2326,7 +2328,7 @@ Proof.
auto.
(* switch *)
- destruct (H2 f (Kswitch2 k)) as [S1 [A1 B1]]. destruct out; auto.
+ destruct (H2 f (Kswitch2 k)) as [S1 [A1 B1]].
set (S2 :=
match out with
| Out_normal => State f Sskip k e m2
@@ -2350,8 +2352,6 @@ Proof.
(* call internal *)
destruct (H3 f k) as [S1 [A1 B1]].
- red in H4. destruct out; auto. destruct o as [[v' ty'] | ].
- tauto. destruct (fn_return f); tauto.
eapply star_left. right; eapply step_internal_function; eauto.
eapply star_right. eexact A1.
inv B1; simpl in H4; try contradiction.
@@ -2403,11 +2403,6 @@ Lemma exec_stmt_to_steps:
forall e m s t m' out,
exec_stmt e m s t m' out ->
forall f k,
- match out with
- | Out_return None => fn_return f = Tvoid
- | Out_return (Some(v, ty)) => fn_return f <> Tvoid
- | _ => True
- end ->
exists S,
star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S.
Proof (proj1 (proj2 (proj2 (proj2 bigstep_to_steps)))).
@@ -2465,8 +2460,6 @@ Proof.
induction 1; intros; simpl; auto with arith. exploit leftcontext_size; eauto. auto with arith.
Qed.
-Axiom ADMITTED: forall (P: Prop), P.
-
Lemma evalinf_funcall_steps:
forall m fd args t k,
evalinf_funcall m fd args t ->
@@ -2662,7 +2655,7 @@ Proof.
reflexivity. reflexivity.
eapply COS; eauto. traceEq.
(* return some *)
- eapply forever_N_plus. apply plus_one; right; constructor. apply ADMITTED.
+ eapply forever_N_plus. apply plus_one; right; constructor.
eapply COE with (C := fun x => x); eauto. constructor. traceEq.
(* while test *)
eapply forever_N_plus. apply plus_one; right; constructor.
@@ -2675,7 +2668,7 @@ Proof.
reflexivity. reflexivity.
eapply COS; eauto. traceEq.
(* while loop *)
- destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kwhile2 a s0 k)) as [S1 [A1 B1]]; auto. inv H3; auto.
+ destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kwhile2 a s0 k)) as [S1 [A1 B1]]; auto.
eapply forever_N_plus.
eapply plus_left. right; constructor.
eapply star_trans. eapply eval_expression_to_steps; eauto.
@@ -2688,7 +2681,7 @@ Proof.
eapply forever_N_plus. apply plus_one; right; constructor.
eapply COS; eauto. traceEq.
(* dowhile test *)
- destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto. inv H1; auto.
+ destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto.
eapply forever_N_plus.
eapply plus_left. right; constructor.
eapply star_trans. eexact A1.
@@ -2696,7 +2689,7 @@ Proof.
reflexivity. reflexivity.
eapply COE with (C := fun x => x); eauto. constructor. traceEq.
(* dowhile loop *)
- destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto. inv H1; auto.
+ destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto.
eapply forever_N_plus.
eapply plus_left. right; constructor.
eapply star_trans. eexact A1.
@@ -2728,7 +2721,7 @@ Proof.
reflexivity. reflexivity.
eapply COS; eauto. traceEq.
(* for next *)
- destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kfor3 a2 a3 s0 k)) as [S1 [A1 B1]]; auto. inv H3; auto.
+ destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kfor3 a2 a3 s0 k)) as [S1 [A1 B1]]; auto.
eapply forever_N_plus.
eapply plus_left. right; apply step_for.
eapply star_trans. eapply eval_expression_to_steps; eauto.
@@ -2738,7 +2731,7 @@ Proof.
reflexivity. reflexivity. reflexivity. reflexivity.
eapply COS; eauto. traceEq.
(* for loop *)
- destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kfor3 a2 a3 s0 k)) as [S1 [A1 B1]]; auto. inv H3; auto.
+ destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kfor3 a2 a3 s0 k)) as [S1 [A1 B1]]; auto.
destruct (exec_stmt_to_steps _ _ _ _ _ _ H4 f (Kfor4 a2 a3 s0 k)) as [S2 [A2 B2]]; auto. inv B2.
eapply forever_N_plus.
eapply plus_left. right; apply step_for.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 603e273..cff182d 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -1699,12 +1699,11 @@ Proof.
econstructor; eauto. constructor; auto.
(* return none *)
- inv H8. econstructor; split.
+ inv H7. econstructor; split.
left. apply plus_one. econstructor; eauto.
- rewrite <- H. apply function_return_preserved; auto.
constructor. apply match_cont_call; auto.
(* return some 1 *)
- inv H7. inv H1. econstructor; split.
+ inv H6. inv H0. econstructor; split.
left; eapply plus_left. constructor. apply push_seq. traceEq.
econstructor; eauto. constructor. auto.
(* return some 2 *)