summaryrefslogtreecommitdiff
path: root/arm
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-08-05 14:40:34 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-08-05 14:40:34 +0000
commitbdc7b815d033f84e5538a1c8db87d3c061b1ca4c (patch)
treebc3ca91f80b4193335cdcc07e7003c9527b48350 /arm
parent213bf38509f4f92545d4c5749c25a55b9a9dda36 (diff)
Added 'going wrong' behaviors
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm')
-rw-r--r--arm/Asmgenproof.v2
-rw-r--r--arm/Constpropproof.v2
-rw-r--r--arm/Selectionproof.v2
3 files changed, 3 insertions, 3 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index f9f4cd0..7b1fd62 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -1173,7 +1173,7 @@ Proof.
Qed.
Theorem transf_program_correct:
- forall (beh: program_behavior),
+ forall (beh: program_behavior), not_wrong beh ->
Machconcr.exec_program prog beh -> Asm.exec_program tprog beh.
Proof.
unfold Machconcr.exec_program, Asm.exec_program; intros.
diff --git a/arm/Constpropproof.v b/arm/Constpropproof.v
index 7c7b878..08c5baf 100644
--- a/arm/Constpropproof.v
+++ b/arm/Constpropproof.v
@@ -947,7 +947,7 @@ Qed.
[Smallstep.simulation_step_preservation]. *)
Theorem transf_program_correct:
- forall (beh: program_behavior),
+ forall (beh: program_behavior), not_wrong beh ->
exec_program prog beh -> exec_program tprog beh.
Proof.
unfold exec_program; intros.
diff --git a/arm/Selectionproof.v b/arm/Selectionproof.v
index 967e229..cf7613b 100644
--- a/arm/Selectionproof.v
+++ b/arm/Selectionproof.v
@@ -1446,7 +1446,7 @@ Proof.
Qed.
Theorem transf_program_correct:
- forall (beh: program_behavior),
+ forall (beh: program_behavior), not_wrong beh ->
Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh.
Proof.
unfold CminorSel.exec_program, Cminor.exec_program; intros.