diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-13 18:11:19 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-13 18:11:19 +0000 |
| commit | a5ffc59246b09a389e5f8cbc2f217e323e76990f (patch) | |
| tree | e1bc7cc54518aad7c20645f187cee8110de8cff9 /backend/Reloadtyping.v | |
| parent | 4daccd62b92b23016d3f343d5691f9c164a8a951 (diff) | |
| download | compcert-a5ffc59246b09a389e5f8cbc2f217e323e76990f.tar.gz compcert-a5ffc59246b09a389e5f8cbc2f217e323e76990f.zip | |
Revised handling of annotation statements, and more generally built-in functions, and more generally external functions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Reloadtyping.v')
| -rw-r--r-- | backend/Reloadtyping.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 60be59b9..eba5ad62 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -33,9 +33,7 @@ Require Import Reloadproof. generate well-typed instruction sequences, given sufficient typing and well-formedness hypotheses over the locations involved. *) -Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove - wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lbuiltin - wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty. +Hint Constructors wt_instr: reloadty. Remark wt_code_cons: forall f i c, wt_instr f i -> wt_code f c -> wt_code f (i :: c). @@ -292,9 +290,12 @@ Proof. destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. auto 10 with reloadty. + destruct (ef_reloads ef) as [] _eqn. + assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence. assert (map mreg_type (regs_for args) = map Loc.type args). apply wt_regs_for. apply arity_ok_enough. congruence. assert (mreg_type (reg_for res) = Loc.type res). eauto with reloadty. + auto 10 with reloadty. auto with reloadty. |