From 054d3581e37075b8e2c32ce69311b3d60f6d43f7 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 5 May 2017 10:16:34 +0200 Subject: Bring RISC-V port up to date Commit 7873af3 introduced changes in the Conventions1.v interface. This commit implements those changes for RISC-V. --- riscV/Conventions1.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'riscV/Conventions1.v') diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index 922f878a..7ce7f7ee 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -74,6 +74,8 @@ Definition destroyed_at_call := Definition dummy_int_reg := R6. (**r Used in [Coloring]. *) Definition dummy_float_reg := F0 . (**r Used in [Coloring]. *) +Definition callee_save_type := mreg_type. + Definition is_float_reg (r: mreg) := match r with | R5 | R6 | R7 | R8 | R9 | R10 | R11 @@ -149,10 +151,10 @@ Lemma loc_result_pair: | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true - /\ Archi.splitlong = true + /\ Archi.ptr64 = false end. Proof. - intros. change Archi.splitlong with (negb Archi.ptr64). + intros. unfold loc_result; destruct (sig_res sg) as [[]|]; auto. unfold mreg_type; destruct Archi.ptr64; auto. split; auto. congruence. -- cgit