diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-27 17:55:14 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-27 17:55:14 +0100 |
commit | 569a32b730608002dbb01088660ecf5bfa19dc02 (patch) | |
tree | 36f9b385aabcb88c597140bd08d28bf787d9b481 | |
parent | d28f8d67bf025ff0beb478672813860793f2b2a8 (diff) | |
download | compcert-kvx-569a32b730608002dbb01088660ecf5bfa19dc02.tar.gz compcert-kvx-569a32b730608002dbb01088660ecf5bfa19dc02.zip |
oper1_sound
-rw-r--r-- | backend/CSE2.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index 61abbcdf..87460f90 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -499,7 +499,16 @@ Proof. rewrite PTree.gss. rewrite Regmap.gss. simpl. - replace ( + rewrite args_replace_dst by auto. + assumption. + } + rewrite Regmap.gso by congruence. + unfold sem_reg. + rewrite PTree.gso by congruence. + rewrite Regmap.gso in KILL by congruence. + exact KILL. +Qed. + (* Definition apply_instr instr x := match instr with |