aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-04-03 21:00:46 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-04-03 21:00:46 +0200
commit4032ed3192424a23dbb0a4f3bd2a539b22625168 (patch)
treed1991d95bafffbdbd0e01ed9a8dc273dd5eaa571 /test/monniaux
parent015a05d8661504388ea1109f740eb16220311f93 (diff)
downloadcompcert-kvx-4032ed3192424a23dbb0a4f3bd2a539b22625168.tar.gz
compcert-kvx-4032ed3192424a23dbb0a4f3bd2a539b22625168.zip
problem in ValueAOp
Diffstat (limited to 'test/monniaux')
-rw-r--r--test/monniaux/bitsliced-aes/bs.c11
-rw-r--r--test/monniaux/ternary_builtin/ternary_builtin.c8
2 files changed, 7 insertions, 12 deletions
diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c
index 063f36f5..9a24643c 100644
--- a/test/monniaux/bitsliced-aes/bs.c
+++ b/test/monniaux/bitsliced-aes/bs.c
@@ -2,17 +2,8 @@
#include <string.h>
#include "bs.h"
-
-static inline long compcert_ternary_signedl(long x, long v0, long v1) {
- return ((-(x==0)) & v0) | ((-(x!=0)) & v1);
-}
-
-static inline word_t compcert_ternary(word_t x, word_t v0, word_t v1) {
- return compcert_ternary_signedl(x, v0, v1);
-}
-
#if defined(__K1C__)
-#define TERNARY(x, v0, v1) compcert_ternary((x), (v0), (v1))
+#define TERNARY(x, v0, v1) __builtin_ternary_ulong((x), (v1), (v0))
#else
#define TERNARY(x, v0, v1) ((x) ? (v1) : (v0))
#endif
diff --git a/test/monniaux/ternary_builtin/ternary_builtin.c b/test/monniaux/ternary_builtin/ternary_builtin.c
index 98497387..1295581c 100644
--- a/test/monniaux/ternary_builtin/ternary_builtin.c
+++ b/test/monniaux/ternary_builtin/ternary_builtin.c
@@ -1,10 +1,14 @@
#include <stdio.h>
-int essai(int x, unsigned y, unsigned z) {
+unsigned essai(int x, unsigned y, unsigned z) {
return __builtin_ternary_uint(x, y, z);
}
+unsigned long essai2(int x, unsigned long y, unsigned long z) {
+ return __builtin_ternary_ulong(x, y, z);
+}
+
int main() {
- printf("%d\n", essai(0, 42, 69));
+ printf("%ld\n", essai2(0, 42, 69));
return 0;
}