From 88448ee297d8894ecfb09d7925663cf6eb12cf01 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 22 Mar 2019 15:44:07 +0100 Subject: Jump tables now work. There is still an "Admitted" subcase in a proof. --- mppa_k1c/Machregs.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'mppa_k1c/Machregs.v') diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 4de37af4..60142797 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -152,8 +152,7 @@ Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mre Definition destroyed_by_cond (cond: condition): list mreg := nil. -(* Definition destroyed_by_jumptable: list mreg := R5 :: nil. *) -Definition destroyed_by_jumptable: list mreg := nil. +Definition destroyed_by_jumptable: list mreg := R62 :: R63 :: nil. Fixpoint destroyed_by_clobber (cl: list string): list mreg := match cl with -- cgit