diff options
Diffstat (limited to 'backend/LTLintyping.v')
| -rw-r--r-- | backend/LTLintyping.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 9f3f5896..6013a17d 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -76,6 +76,11 @@ Inductive wt_instr : instruction -> Prop := List.map Loc.type args = type_of_condition cond -> locs_acceptable args -> wt_instr (Lcond cond args lbl) + | wt_Ljumptable: + forall arg tbl, + Loc.type arg = Tint -> + loc_acceptable arg -> + wt_instr (Ljumptable arg tbl) | wt_Lreturn: forall optres, option_map Loc.type optres = funsig.(sig_res) -> |