From c4cc75dc6abcb0eee6f3288e96fea4aec540fd68 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 5 Sep 2019 11:19:22 +0200 Subject: more proofs going through --- backend/Lineartyping.v | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'backend/Lineartyping.v') 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. -- cgit