aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asmgenproof1.v
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-12-08 09:32:48 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-12-08 09:32:48 +0100
commit766968b709e5248a6aac6fdb92f6228be05fc70c (patch)
tree792c7fc4651dd0bf98b6697305e0eb3a006be854 /powerpc/Asmgenproof1.v
parenta100edde18de43cf933c0d53467e196541436e13 (diff)
parentcb93a301fd2ddae3071ae0838290b201496d90ef (diff)
downloadcompcert-kvx-766968b709e5248a6aac6fdb92f6228be05fc70c.tar.gz
compcert-kvx-766968b709e5248a6aac6fdb92f6228be05fc70c.zip
Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3
Diffstat (limited to 'powerpc/Asmgenproof1.v')
-rw-r--r--powerpc/Asmgenproof1.v12
1 files changed, 0 insertions, 12 deletions
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 1b797999..850e95c7 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1500,18 +1500,6 @@ Opaque Val.add.
- replace v with (Val.maketotal (Val.intoffloat (rs x))).
TranslOpSimpl.
rewrite H1; auto.
- (* Ointuoffloat *)
-- replace v with (Val.maketotal (Val.intuoffloat (rs x))).
- TranslOpSimpl.
- rewrite H1; auto.
- (* Ofloatofint *)
-- replace v with (Val.maketotal (Val.floatofint (rs x))).
- TranslOpSimpl.
- rewrite H1; auto.
- (* Ofloatofintu *)
-- replace v with (Val.maketotal (Val.floatofintu (rs x))).
- TranslOpSimpl.
- rewrite H1; auto.
(* Ocmp *)
- destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto.
exists rs'; auto with asmgen.