From 93fd5df1bff8b22b3513a07a765b0a72f1505243 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 20:26:32 +0200 Subject: some more on builtins --- backend/Selection.v | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) (limited to 'backend/Selection.v') 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. *) -- cgit