diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 20:09:19 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 20:11:48 +0200 |
| commit | 677771949bd62f7f5bbcf99bba6b6f816f07a6c2 (patch) | |
| tree | 597b2ccc5867bc2bbb083c4e13f792671b2042c1 /arm/SelectOp.vp | |
| parent | 36e64ee96ded0c94c83da6fb12202c276e66ba45 (diff) | |
| parent | b7e0d70de2ace6f0a22f9f65cc244d875ee48496 (diff) | |
| download | compcert-kvx-677771949bd62f7f5bbcf99bba6b6f816f07a6c2.tar.gz compcert-kvx-677771949bd62f7f5bbcf99bba6b6f816f07a6c2.zip | |
Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-if-conversion
Diffstat (limited to 'arm/SelectOp.vp')
| -rw-r--r-- | arm/SelectOp.vp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index f3f01730..e3ef3eaf 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -383,6 +383,16 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) := Definition compfs (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). +Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) := + if match ty with + | Tint => true + | Tfloat => true + | Tsingle => true + | _ => false + end + then Some (Eop (Osel cond ty) (e1 ::: e2 ::: args)) + else None. + (** ** Integer conversions *) Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. |