diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 11:19:22 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 11:19:22 +0200 |
| commit | c4cc75dc6abcb0eee6f3288e96fea4aec540fd68 (patch) | |
| tree | e63d0437c3f3cb43eb26cced8ad94acc62e82dad /backend/Lineartyping.v | |
| parent | 7042070a3668ae149ec6a490b8e7c1a6aa82d6fe (diff) | |
| download | compcert-kvx-c4cc75dc6abcb0eee6f3288e96fea4aec540fd68.tar.gz compcert-kvx-c4cc75dc6abcb0eee6f3288e96fea4aec540fd68.zip | |
more proofs going through
Diffstat (limited to 'backend/Lineartyping.v')
| -rw-r--r-- | backend/Lineartyping.v | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 1fe23a9d..da66b6ff 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -76,7 +76,7 @@ Definition wt_instr (i: instruction) : bool := let (targs, tres) := type_of_operation op in subtype tres (mreg_type res) end - | Lload chunk addr args dst => + | Lload trap chunk addr args dst => subtype (type_of_chunk chunk) (mreg_type dst) | Ltailcall sg ros => zeq (size_arguments sg) 0 @@ -332,6 +332,20 @@ Local Opaque mreg_type. apply wt_setreg. eapply Val.has_subtype; eauto. destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto. apply wt_undef_regs; auto. +- (* load notrap1 *) + simpl in *; InvBooleans. + econstructor; eauto. + apply wt_setreg. eapply Val.has_subtype; eauto. + unfold default_notrap_load_value. + constructor. + apply wt_undef_regs; auto. +- (* load notrap2 *) + simpl in *; InvBooleans. + econstructor; eauto. + apply wt_setreg. eapply Val.has_subtype; eauto. + unfold default_notrap_load_value. + constructor. + apply wt_undef_regs; auto. - (* store *) simpl in *; InvBooleans. econstructor. eauto. eauto. eauto. |