From fd24564480c438da9456d781ec17bfa3ac6277c1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Jan 2020 22:46:55 +0100 Subject: progressing in proofs --- backend/ForwardMoves.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backend/ForwardMoves.v') diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v index 96a19ecd..65d66b16 100644 --- a/backend/ForwardMoves.v +++ b/backend/ForwardMoves.v @@ -300,6 +300,8 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) Iop op (subst_args fmap pc args) dst s | Iload trap chunk addr args dst s => Iload trap chunk addr (subst_args fmap pc args) dst s + | Istore chunk addr args src s => + Istore chunk addr (subst_args fmap pc args) src s | Icall sig ros args dst s => Icall sig ros (subst_args fmap pc args) dst s | Itailcall sig ros args => -- cgit