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 /backend/CSE.v | |
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 'backend/CSE.v')
-rw-r--r-- | backend/CSE.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index 6d3f6f33..30cf5e21 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -486,7 +486,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb | _ => empty_numbering end - | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ => + | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ + | EF_debug _ _ _ | EF_select _ => set_res_unknown before res end | Icond cond args ifso ifnot => |