diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-07-24 11:42:09 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-07-24 11:42:09 +0200 |
| commit | a4570fed198034e535d0d6d99e23cfbb1d40b926 (patch) | |
| tree | e4e5a9dc845fc0972622ae05fd9084234ed9a44d /backend/RTLtyping.v | |
| parent | 95f918c38b1e59f40ae7af455ec2c6746289375e (diff) | |
| parent | b5c4192c73d7b02e0c90354e26b35a84ee141083 (diff) | |
| download | compcert-kvx-a4570fed198034e535d0d6d99e23cfbb1d40b926.tar.gz compcert-kvx-a4570fed198034e535d0d6d99e23cfbb1d40b926.zip | |
Merge branch 'kvx-work' into rtl-tunneling
Diffstat (limited to 'backend/RTLtyping.v')
| -rw-r--r-- | backend/RTLtyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 15ed6d8a..6048f895 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -858,7 +858,7 @@ Lemma wt_exec_Iload_notrap: forall env f chunk addr args dst s rs, wt_instr f env (Iload NOTRAP chunk addr args dst s) -> wt_regset env rs -> - wt_regset env (rs#dst <- (default_notrap_load_value chunk)). + wt_regset env (rs#dst <- Vundef). Proof. intros. eapply wt_regset_assign; eauto. simpl. trivial. |