aboutsummaryrefslogtreecommitdiffstats
path: root/test
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-06-04 12:15:16 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-06-04 12:15:16 +0200
commit1fc26cf05b90c167d2f02599cc75b9df26e4d623 (patch)
tree160b9c44268a5b96ae1cde0e3a9589692d56ffaf /test
parent5feecb99712de3604f284e5934aed73f2b606659 (diff)
downloadcompcert-kvx-1fc26cf05b90c167d2f02599cc75b9df26e4d623.tar.gz
compcert-kvx-1fc26cf05b90c167d2f02599cc75b9df26e4d623.zip
remove old "ternary" stuff
Diffstat (limited to 'test')
-rw-r--r--test/monniaux/binary_search/binary_search.c15
-rw-r--r--test/monniaux/bitsliced-aes/bs.c6
-rw-r--r--test/monniaux/bitsliced-tea/bstea.h11
-rw-r--r--test/monniaux/picosat-965/Makefile2
-rw-r--r--test/monniaux/ternary.h23
5 files changed, 10 insertions, 47 deletions
diff --git a/test/monniaux/binary_search/binary_search.c b/test/monniaux/binary_search/binary_search.c
index 24d1b122..4051ebf0 100644
--- a/test/monniaux/binary_search/binary_search.c
+++ b/test/monniaux/binary_search/binary_search.c
@@ -2,7 +2,6 @@
#include <stdlib.h>
#include <inttypes.h>
#include "../clock.h"
-#include "../ternary.h"
typedef int data;
typedef unsigned index;
@@ -31,8 +30,8 @@ int my_bsearch2 (data *a, index n, data x) {
index k = (i + j) / 2;
index kp1 = k+1, km1 = k-1;
data ak = a[k];
- i = TERNARY32(ak < x, kp1, i);
- j = TERNARY32(ak > x, km1, j);
+ i = ak < x ? kp1 : i;
+ j = ak > x ? km1 : j;
if (ak == x) {
return k;
}
@@ -47,8 +46,8 @@ int my_bsearch3 (data *a, index n, data x) {
index kp1 = k+1, km1 = k-1;
data ak = a[k];
_Bool lt = ak < x, gt = ak > x;
- i = TERNARY32(lt, kp1, i);
- j = TERNARY32(gt, km1, j);
+ i = lt ? kp1 : i;
+ j = gt ? km1 : j;
if (ak == x) {
return k;
}
@@ -63,8 +62,8 @@ int my_bsearch4 (data *a, index n, data x) {
index kp1 = k+1, km1 = k-1;
data ak = a[k];
_Bool lt = ak < x, gt = ak > x;
- i = TERNARY32(lt, kp1, i);
- j = TERNARY32(gt, km1, j);
+ i = lt ? kp1 : i;
+ j = gt ? km1 : j;
if (ak == x) {
goto end;
}
@@ -81,7 +80,7 @@ void random_ascending_fill(data *a, index n) {
for(index i=0; i<n; i++) {
a[i] = v;
v++;
- v = TERNARY32(r & 0x40000000, v+1, v);
+ v = (r & 0x40000000) ? (v+1) : v;
r = r * 97 + 5;
}
}
diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c
index 3132e1d9..a172aca5 100644
--- a/test/monniaux/bitsliced-aes/bs.c
+++ b/test/monniaux/bitsliced-aes/bs.c
@@ -1,13 +1,9 @@
#include <string.h>
#include "bs.h"
-#include "../ternary.h"
/* TEMPORARY */
-#define TERNARY(x, v0, v1) ((x) ? (v0) : (v1))
-/*
-#define TERNARY(x, v0, v1) TERNARY64(x, v1, v0)
-*/
+#define TERNARY(x, v0, v1) ((x) ? (v1) : (v0))
#if (defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__) ||\
defined(__amd64__) || defined(__amd32__)|| defined(__amd16__)
diff --git a/test/monniaux/bitsliced-tea/bstea.h b/test/monniaux/bitsliced-tea/bstea.h
index 9ca4f776..15607464 100644
--- a/test/monniaux/bitsliced-tea/bstea.h
+++ b/test/monniaux/bitsliced-tea/bstea.h
@@ -5,17 +5,8 @@
#include <limits.h>
#include "bstea_wordsize.h"
-#include "../ternary.h"
-/*
+
#define TERNARY(x, v1, v0) ((x) ? (v1) : (v0))
-*/
-#if __BSTEA_WORDSIZE==64
-#define TERNARY(x, v1, v0) TERNARY64(x, v1, v0)
-#elif __BSTEA_WORDSIZE==32
-#define TERNARY(x, v1, v0) TERNARY32(x, v1, v0)
-#else
-#error What is the bit size !?
-#endif
#define TEA_ROUNDS 32
diff --git a/test/monniaux/picosat-965/Makefile b/test/monniaux/picosat-965/Makefile
index d3322bcb..e13087de 100644
--- a/test/monniaux/picosat-965/Makefile
+++ b/test/monniaux/picosat-965/Makefile
@@ -7,7 +7,7 @@ ALL_CFLAGS = -DNALARM -DNZIP -DNGETRUSAGE -DNDEBUG
K1C_CFLAGS += $(EMBEDDED_CFLAGS)
K1C_CCOMPFLAGS += $(EMBEDDED_CFLAGS)
CCOMPFLAGS += -fbitfields
-K1C_CCOMPFLAGS += -fbitfields
+K1C_CCOMPFLAGS += -fbitfields -fno-if-conversion
K1C_CFLAGS += $(ALL_CFLAGS)
K1C_CCOMPFLAGS += $(ALL_CFLAGS)
diff --git a/test/monniaux/ternary.h b/test/monniaux/ternary.h
deleted file mode 100644
index 43cdbd12..00000000
--- a/test/monniaux/ternary.h
+++ /dev/null
@@ -1,23 +0,0 @@
-#include <stdint.h>
-
-static inline int32_t ternary_int32(int32_t a, int32_t b, int32_t c) {
- return (((-((a) == 0)) & (c)) | ((-((a) != 0)) & (b)));
-}
-static inline uint32_t ternary_uint32(uint32_t a, uint32_t b, uint32_t c) {
- return ternary_int32(a, b, c);
-}
-
-static inline int64_t ternary_int64(int64_t a, int64_t b, int64_t c) {
- return (((-((a) == 0)) & (c)) | ((-((a) != 0)) & (b)));
-}
-static inline uint64_t ternary_uint64(uint64_t a, uint64_t b, uint64_t c) {
- return ternary_int64(a, b, c);
-}
-
-#if defined(__COMPCERT__) && defined(__K1C__)
-#define TERNARY32(a, b, c) ternary_uint32((a), (b), (c))
-#define TERNARY64(a, b, c) ternary_uint64((a), (b), (c))
-#else
-#define TERNARY32(a, b, c) ((a) ? (b) : (c))
-#define TERNARY64(a, b, c) ((a) ? (b) : (c))
-#endif