Fix for math-library compatibility on MacOS (#798)

PrincetonUniversity · Dec 6, 2024 · 426c7f4 · 426c7f4
1 parent 8688af9
commit 426c7f4
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 2 deletions.
diff --git a/lib/CoqMakefile.local b/lib/CoqMakefile.local
@@ -4,7 +4,7 @@ CFLAGS=-I$(INCLUDE)
 CC=gcc
 
 proof/math_extern.v: $(SRC)/math_extern.c
-	clightgen -flongdouble -normalize $< -o $@ 
+	clightgen -flongdouble -normalize -DCOMPCERT $< -o $@ 
 
 proof/malloc_extern.v: $(SRC)/malloc_extern.c
 	clightgen -normalize $< -o $@ 
@@ -23,7 +23,7 @@ test/incr.v: test/incr.c
 test/incr_main.v: test/incr_main.c
 	clightgen -I$(INCLUDE) -normalize $<
 test/testmath.v: test/testmath.c
-	clightgen -I$(INCLUDE) -normalize $<
+	clightgen -I$(INCLUDE) -normalize  -DCOMPCERT $<
 
 tests: test/incr
 

diff --git a/lib/proof/src/math_extern.c b/lib/proof/src/math_extern.c
@@ -1,3 +1,6 @@
+#ifdef COMPCERT
+typedef float _Float16;  /* _Float16 is a MacOS thing that CompCert doesn't support */
+#endif
 #include <math.h>
 
 /* Note regard 'long double':

diff --git a/lib/test/testmath.c b/lib/test/testmath.c
@@ -1,3 +1,6 @@
+#ifdef COMPCERT
+typedef float _Float16;  /* _Float16 is a MacOS thing that CompCert doesn't support */
+#endif
 #include <math.h>
 
 double f(double t) {