aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux/bitsliced-aes
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-27 10:00:01 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-27 10:00:01 +0100
commitf5beb55d283078afc2ce782201aef464c10b2e8f (patch)
tree424627801f62c431c8181652b3ac810a59a98267 /test/monniaux/bitsliced-aes
parent86d7e48d92d602e2349032883b7b753bbea81a3c (diff)
downloadcompcert-kvx-f5beb55d283078afc2ce782201aef464c10b2e8f.tar.gz
compcert-kvx-f5beb55d283078afc2ce782201aef464c10b2e8f.zip
switch off ternary if not CompCert
Diffstat (limited to 'test/monniaux/bitsliced-aes')
-rw-r--r--test/monniaux/bitsliced-aes/bs.c18
1 files changed, 4 insertions, 14 deletions
diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c
index 1fc046d1..46dee525 100644
--- a/test/monniaux/bitsliced-aes/bs.c
+++ b/test/monniaux/bitsliced-aes/bs.c
@@ -11,21 +11,11 @@ static inline word_t compcert_ternary(word_t x, word_t v0, word_t v1) {
return compcert_ternary_signedl(x, v0, v1);
}
-/* Original
- #define TERNARY0(cmp,v1) ((cmp) ? (v1) : 0) */
-/* with bitmask
-#define TERNARY0(cmp,v1) (-(cmp != 0) & (v1))
-*/
-/* with function call to ternary
-#define TERNARY0(cmp,v1) compcert_ternary(cmp, 0, v1)
-*/
-/*
-#define TERNARY0(x, v1) ((unsigned long) ((long) (-(((long) (x))!=0)) & (v1)))
-#define TERNARY(x, v0, v1) \
- (((long) (-(((long) (x))==0)) & ((long) (v0))) | \
- ((long) (-(((long) (x))!=0)) & ((long) (v1))))
-*/
+#if defined(__COMPCERT__)
#define TERNARY(x, v0, v1) compcert_ternary((x), (v0), (v1))
+#else
+#define TERNARY(x, v0, v1) ((x) ? (v1) : (v0))
+#endif
#if (defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__) ||\
defined(__amd64__) || defined(__amd32__)|| defined(__amd16__)