diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-13 15:58:38 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-26 18:48:06 +0200 |
| commit | 58b59cce492f53ebd9aa960306f07f816c2e279d (patch) | |
| tree | 51e0430893119b307c21976c44ccffba0716d3cd /exportclight | |
| parent | c36514ac4b05f78dd2e02fab3f8886cab8234925 (diff) | |
| download | compcert-58b59cce492f53ebd9aa960306f07f816c2e279d.tar.gz compcert-58b59cce492f53ebd9aa960306f07f816c2e279d.zip | |
Add a built-in function for "select" (strict conditional)
The built-in is called `EF_select` and has type `(int, T, T) -> T` for
a given Cminor type T.
During instruction selection, it is turned into an `Osel` operation if
available, otherwise into an if/then/else.
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/ExportClight.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index b124586a..05cbed71 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -269,6 +269,8 @@ let external_function p = function coqstring text signatur sg (print_list coqstring) clob + | EF_select ty -> + fprintf p "@[<hov 2>(EF_select %a)@]" asttype ty (* Expressions *) |