diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-09-15 12:32:26 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-09-15 12:37:02 +0200 |
| commit | 6f2b5713f8e378e6e074f35a537e86a497c64e35 (patch) | |
| tree | 87d80f8a4dd0de1f0594fc67c48ff26a58c68056 /ia32/Machregs.v | |
| parent | 9124c9231c11effae6e32d73c6c8af7c4032f928 (diff) | |
| download | compcert-6f2b5713f8e378e6e074f35a537e86a497c64e35.tar.gz compcert-6f2b5713f8e378e6e074f35a537e86a497c64e35.zip | |
Add interference for indirect calls.
Avoids problems with overwritting the registe containing the
function address.
Bug 19779
Diffstat (limited to 'ia32/Machregs.v')
| -rw-r--r-- | ia32/Machregs.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v index fb80a1fd..3a6ae674 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -55,7 +55,7 @@ Proof. Qed. Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - + Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete @@ -166,6 +166,9 @@ Definition destroyed_at_function_entry: list mreg := (* must include [destroyed_by_setstack ty] *) DX :: FP0 :: nil. +Definition destroyed_at_indirect_call: list mreg := + nil. + Definition destroyed_by_setstack (ty: typ): list mreg := match ty with | Tfloat | Tsingle => FP0 :: nil @@ -210,6 +213,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin + destroyed_at_indirect_call destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame mregs_for_operation mregs_for_builtin. |