diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-05-05 10:16:34 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-05-05 10:16:34 +0200 |
| commit | 054d3581e37075b8e2c32ce69311b3d60f6d43f7 (patch) | |
| tree | d4fa847fdd4e3e7016729c91ce5418a66077bdb9 /riscV/Conventions1.v | |
| parent | 2bbb20db14cba7c2a460f58ae84c2526e3bb35aa (diff) | |
| download | compcert-kvx-054d3581e37075b8e2c32ce69311b3d60f6d43f7.tar.gz compcert-kvx-054d3581e37075b8e2c32ce69311b3d60f6d43f7.zip | |
Bring RISC-V port up to date
Commit 7873af3 introduced changes in the Conventions1.v interface. This commit implements those changes for RISC-V.
Diffstat (limited to 'riscV/Conventions1.v')
| -rw-r--r-- | riscV/Conventions1.v | 6 |
1 files changed, 4 insertions, 2 deletions
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. |