diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 14:58:33 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 14:58:33 +0000 |
| commit | 8ccc7f2f597aff2c8590c4e62552fb53406ad0f8 (patch) | |
| tree | a553844ce1b6960ae5240f65593c085be733e3b2 /backend/RTLtyping.v | |
| parent | 74487f079dd56663f97f9731cea328931857495c (diff) | |
More realistic treatment of jump tables: show the absence of overflow when accessing the table
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1172 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/RTLtyping.v')
| -rw-r--r-- | backend/RTLtyping.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 86f0eaf..d8e2f21 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -116,6 +116,7 @@ Inductive wt_instr : instruction -> Prop := forall arg tbl, env arg = Tint -> (forall s, In s tbl -> valid_successor s) -> + list_length_z tbl * 4 <= Int.max_signed -> wt_instr (Ijumptable arg tbl) | wt_Ireturn: forall optres, @@ -232,6 +233,7 @@ Definition check_instr (i: instruction) : bool := | Ijumptable arg tbl => check_reg arg Tint && List.forallb check_successor tbl + && zle (list_length_z tbl * 4) Int.max_signed | Ireturn optres => match optres, funct.(fn_sig).(sig_res) with | None, None => true @@ -336,8 +338,8 @@ Proof. apply check_successor_correct; auto. (* jumptable *) constructor. apply check_reg_correct; auto. - rewrite List.forallb_forall in H0. intros. apply check_successor_correct; auto. - intros. + rewrite List.forallb_forall in H1. intros. apply check_successor_correct; auto. + eapply proj_sumbool_true. eauto. (* return *) constructor. destruct o; simpl; destruct funct.(fn_sig).(sig_res); try discriminate. |