diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-02-01 17:52:33 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-02-01 17:53:12 +0100 |
| commit | 8844e567fdc7f68c378f727a63278d94c2dd51bf (patch) | |
| tree | 0a25cb72af3575fd09e4d6e83630034b0b707943 /test/monniaux/jpeg-6b/jconfig.h | |
| parent | 35244064bbb2a853fb5c08898e8a74a7ec489aaa (diff) | |
| download | compcert-kvx-8844e567fdc7f68c378f727a63278d94c2dd51bf.tar.gz compcert-kvx-8844e567fdc7f68c378f727a63278d94c2dd51bf.zip | |
it still seems to work
Diffstat (limited to 'test/monniaux/jpeg-6b/jconfig.h')
| -rw-r--r-- | test/monniaux/jpeg-6b/jconfig.h | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/test/monniaux/jpeg-6b/jconfig.h b/test/monniaux/jpeg-6b/jconfig.h index 56345384..e42ea31b 100644 --- a/test/monniaux/jpeg-6b/jconfig.h +++ b/test/monniaux/jpeg-6b/jconfig.h @@ -28,12 +28,24 @@ */ #define HAVE_PROTOTYPES +#ifdef __COMPCERT__ extern long long __compcert_i64_sdiv(long long a, long long b); -extern unsigned __compcert_i32_umod(unsigned a, unsigned b); +extern long long __compcert_i64_smod(long long a, long long b); + +#define INT_UMOD(a, b) __compcert_i64_smod(a, b) +#define INT_UDIV(a, b) __compcert_i64_sdiv(a, b) +#define INT_DIV(a, b) __compcert_i64_sdiv(a, b) +#define LONG_DIV(a, b) __compcert_i64_sdiv(a, b) -#define LONG_SDIV(x, y) __compcert_i64_sdiv(x, y) -#define INT_UMOD(x, y) __compcert_i32_umod(x, y) #define KILL_TAIL_CALL() { int x=1; } +#else +#define INT_UMOD(a, b) ((a) % (b)) +#define INT_UDIV(a, b) ((a) / (b)) +#define INT_DIV(a, b) ((a) / (b)) +#define LONG_DIV(a, b) ((a) / (b)) + +#define KILL_TAIL_CALL() { } +#endif /* Does your compiler support the declaration "unsigned char" ? * How about "unsigned short" ? |