From da533d94fe178b4f5c3f292dff4c5e73bf82132f Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Mon, 21 Aug 2023 15:14:59 -0700 Subject: [PATCH] fix C compilation of CBOR with proper SteelC include --- src/cbor/Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/cbor/Makefile b/src/cbor/Makefile index eb7ccece6..8d6c67cd1 100644 --- a/src/cbor/Makefile +++ b/src/cbor/Makefile @@ -63,6 +63,7 @@ verify-all: $(ALL_CHECKED_FILES) KRML = $(KRML_HOME)/krml \ -ccopt "-Ofast" \ -drop 'FStar.Tactics.\*' -drop FStar.Tactics -drop 'FStar.Reflection.\*' \ + -I $(STEEL_HOME)/include/steel -add-include '"steel_c.h"' \ -tmpdir out \ -bundle 'CBOR.SteelC+CBOR.SteelST+CBOR.Spec.Constants=CBOR.\*,Steel.\*,C,LowStar.\*,LowParse.\*[rename=CBOR]' \ -skip-linking \ @@ -77,7 +78,7 @@ extract: $(ALL_KRML_FILES) $(KRML) $(ALL_KRML_FILES) test: extract - $(CC) -Wall -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/generic -I out -c cbor_unverified.c + $(CC) -Wall -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/generic -I $(STEEL_HOME)/include/steel -I out -c cbor_unverified.c .PHONY: all verify-all clean %.fst-in %.fsti-in lowparse extract test