diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-07-24 11:49:14 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-07-24 11:49:14 +0200 |
| commit | 1fbe45e2d1f02ef6e8fb6fe7545728a744e047b8 (patch) | |
| tree | 9d8f9e378c88671a0c331b7dcd0cd1014cda3e25 /backend | |
| parent | a4570fed198034e535d0d6d99e23cfbb1d40b926 (diff) | |
| download | compcert-kvx-1fbe45e2d1f02ef6e8fb6fe7545728a744e047b8.tar.gz compcert-kvx-1fbe45e2d1f02ef6e8fb6fe7545728a744e047b8.zip | |
remove default_notrap_load_value
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/RTLTunnelingproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 14a2c037..51ef0f7a 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -531,7 +531,7 @@ Proof. + eapply exec_Iload_notrap1. * exploit instruction_type_preserved; (simpl; eauto)||congruence. * rewrite <- H1. apply eval_addressing_preserved. apply symbols_preserved. - + apply match_states_intro; try assumption. apply set_reg_lessdef. unfold default_notrap_load_value. apply Val.lessdef_undef. apply RS. + + apply match_states_intro; try assumption. apply set_reg_lessdef. apply Val.lessdef_undef. apply RS. - (* Iload NOTRAP2 *) exploit eval_addressing_lessdef; try eassumption. apply reglist_lessdef; apply RS. |