diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-05 17:15:21 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-05 17:18:07 +0200 |
| commit | caaaffd31f63f1239a2371f418ff448651752ff8 (patch) | |
| tree | 5e9931bcbdea9e1cae21748bc73fa8ccfbfb09ac /test | |
| parent | 8f750f2d4d68192d92b6363490e8a8e577f55584 (diff) | |
| download | compcert-kvx-caaaffd31f63f1239a2371f418ff448651752ff8.tar.gz compcert-kvx-caaaffd31f63f1239a2371f418ff448651752ff8.zip | |
Improve portability of the test for annotations inclightgen
__builtin_ais_annot is not supported for macOS nor for Cygwin.
Diffstat (limited to 'test')
| -rw-r--r-- | test/clightgen/Makefile | 2 | ||||
| -rw-r--r-- | test/clightgen/annotations.c | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile index 0607e2fa..bf4a044b 100644 --- a/test/clightgen/Makefile +++ b/test/clightgen/Makefile @@ -22,6 +22,8 @@ SRC+=aes.c almabench.c binarytrees.c bisect.c chomp.c fannkuch.c fft.c \ SRC+=arrays.c eval.c gmllexer.c gmlparser.c intersect.c light.c main.c \ matrix.c memory.c object.c render.c simplify.c surface.c vector.c +CFLAGS=-DSYSTEM_$(SYSTEM) + all: $(SRC:.c=.vo) test: diff --git a/test/clightgen/annotations.c b/test/clightgen/annotations.c index 56fc1700..e91c7fbc 100644 --- a/test/clightgen/annotations.c +++ b/test/clightgen/annotations.c @@ -1,6 +1,8 @@ int f(int x, long y) { +#if !defined(SYSTEM_macosx) && !defined(SYSTEM_cygwin) __builtin_ais_annot("x is %e1, y is %e2", x, y); +#endif __builtin_annot("x is %1, y is %2", x, y); return __builtin_annot_intval("x was here: %1", x); } |