diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-18 09:58:14 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-18 09:58:14 +0200 |
commit | 4663ad4b31e351e29a4d8d034ad4a961a48263f1 (patch) | |
tree | d21554c60ed607bf8fdd1476431f9707bf882604 /backend/Bounds.v | |
parent | 10def48b639b8e83ae6cc8bf9c14da8c12e98370 (diff) | |
parent | 5d017f110f6c23c29a182465ab7832a944c0ba26 (diff) | |
download | compcert-4663ad4b31e351e29a4d8d034ad4a961a48263f1.tar.gz compcert-4663ad4b31e351e29a4d8d034ad4a961a48263f1.zip |
Merge branch 'master' into json_export
Diffstat (limited to 'backend/Bounds.v')
-rw-r--r-- | backend/Bounds.v | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v index 7528b66e..04c1328d 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -87,8 +87,6 @@ Section BOUNDS. Variable f: function. -Parameter mregs_of_clobber: list ident -> list mreg. - (** In the proof of the [Stacking] pass, we only need to bound the registers written by an instruction. Therefore, this function returns these registers, ignoring registers used only as @@ -103,7 +101,6 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil - | Lbuiltin (EF_inline_asm txt typs clob) args res => res ++ mregs_of_clobber clob | Lbuiltin ef args res => res ++ destroyed_by_builtin ef | Lannot ef args => nil | Llabel lbl => nil @@ -354,9 +351,7 @@ Proof. (* call *) eapply size_arguments_bound; eauto. (* builtin *) - apply H1. destruct e; apply in_or_app; auto. - change (destroyed_by_builtin (EF_inline_asm text sg clobbers)) with (@nil mreg) in H2. - simpl in H2; tauto. + apply H1. apply in_or_app; auto. (* annot *) apply H0. rewrite slots_of_locs_charact; auto. Qed. |