Remove _Float16 hack from VSTlib, no longer needed with CompCert 3.15

PrincetonUniversity · Feb 10, 2025 · 7583810 · 7583810
1 parent 9091d31
commit 7583810
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 14 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 -DCOMPCERT $< -o $@ 
+	clightgen -flongdouble -normalize $< -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  -DCOMPCERT $<
+	clightgen -I$(INCLUDE) -normalize $<
 
 tests: test/incr
 

diff --git a/lib/proof/src/math_extern.c b/lib/proof/src/math_extern.c
@@ -1,9 +1,3 @@
-#ifdef COMPCERT
-/* still Starting with CompCert 3.15 (and VST 2.15), don't need this hack
-   any more, but still here for VSTlib compatibility with older versions
-   of CompCert/VST */
-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,9 +1,3 @@
-#ifdef COMPCERT
-/* still Starting with CompCert 3.15 (and VST 2.15), don't need this hack
-   any more, but still here for VSTlib compatibility with older versions
-   of CompCert/VST */
-typedef float _Float16;  /* _Float16 is a MacOS thing that CompCert doesn't support */
-#endif
 #include <math.h>
 
 double f(double t) {