diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 20:26:32 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 20:26:32 +0200 |
| commit | 93fd5df1bff8b22b3513a07a765b0a72f1505243 (patch) | |
| tree | 005f21ad3fe253b52612e09f4e1ccae2811c0d87 /backend/Selection.v | |
| parent | 2dca62f38463b0ebce24fff50666c846df50488e (diff) | |
| download | compcert-kvx-93fd5df1bff8b22b3513a07a765b0a72f1505243.tar.gz compcert-kvx-93fd5df1bff8b22b3513a07a765b0a72f1505243.zip | |
some more on builtins
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. *) |