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 /backend | |
| parent | d28f8d67bf025ff0beb478672813860793f2b2a8 (diff) | |
| download | compcert-kvx-569a32b730608002dbb01088660ecf5bfa19dc02.tar.gz compcert-kvx-569a32b730608002dbb01088660ecf5bfa19dc02.zip | |
oper1_sound
Diffstat (limited to 'backend')
| -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 |