From 7de591569308917c9ffcd4626c94872e390811a2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 11:49:21 +0200 Subject: INJnop --- backend/Injectproof.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'backend/Injectproof.v') diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 51d049b1..7ce401cb 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -742,7 +742,11 @@ Section INJECTOR. (State ts tf sp (Pos.succ pc) trs' m) /\ match_regs (f : function) trs trs'. Proof. - destruct ii as [op args res | chunk addr args res]; simpl; intros. + destruct ii as [ |op args res | chunk addr args res]; simpl; intros. + - exists trs. + split. + * apply exec_Inop; assumption. + * apply match_regs_refl. - repeat rewrite andb_true_iff in VALID. rewrite negb_true_iff in VALID. destruct VALID as (MAX_REG & NOTRAP & LENGTH). -- cgit