diff options
Diffstat (limited to 'backend/Selection.v')
| -rw-r--r-- | backend/Selection.v | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 27c5bd10..e63cbce3 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -268,9 +268,20 @@ Definition sel_switch_long := lowlong. Definition sel_builtin optid ef args := - Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef)). + match ef with + | EF_builtin name sign => + (if String.string_dec name "__builtin_ternary_uint" + then Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef)) + else Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef))) + | _ => + Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef)) + end. (** Conversion from Cminor statements to Cminorsel statements. *) |