Add dist

.gitignore

@@ -1,4 +1,6 @@
 obj
-dist
 .depend
 *.exe
+*.d
+*.o
+*.a

dist/Makefile.basic

@@ -0,0 +1,56 @@
+# A basic Makefile that KaRaMeL copies in the output directory; this is not
+# guaranteed to work and will only work well for very simple projects. This
+# Makefile uses:
+# - the custom C files passed to your krml invocation
+# - the custom C flags passed to your krml invocation
+# - the -o option passed to your krml invocation
+
+include Makefile.include
+
+ifeq (,$(KRML_HOME))
+  $(error please define KRML_HOME to point to the root of your KaRaMeL git checkout)
+endif
+
+CFLAGS 	+= -I. -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/minimal
+CFLAGS 	+= -Wall -Wextra -Werror -std=c11 -Wno-unused-variable \
+  -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-function \
+  -Wno-unused-parameter -Wno-infinite-recursion \
+  -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE
+ifeq ($(OS),Windows_NT)
+CFLAGS 	+= -D__USE_MINGW_ANSI_STDIO
+else
+CFLAGS 	+= -fPIC
+endif
+CFLAGS 	+= $(USER_CFLAGS)
+
+SOURCES += $(ALL_C_FILES) $(USER_C_FILES)
+ifneq (,$(BLACKLIST))
+  SOURCES := $(filter-out $(BLACKLIST),$(SOURCES))
+endif
+OBJS 	+= $(patsubst %.c,%.o,$(SOURCES))
+
+all: $(USER_TARGET)
+
+$(USER_TARGET): $(OBJS)
+
+AR ?= ar
+
+%.a:
+	$(AR) cr $@ $^
+
+%.exe:
+	$(CC) $(CFLAGS) -o $@ $^ $(KRML_HOME)/krmllib/dist/generic/libkrmllib.a
+
+%.so:
+	$(CC) $(CFLAGS) -shared -o $@ $^
+
+%.d: %.c
+	@set -e; rm -f $@; \
+	  $(CC) -MM -MG $(CFLAGS) $< > $@.$$$$; \
+	  sed 's,\($(notdir $*)\)\.o[ :]*,$(dir $@)\1.o $@ : ,g' < $@.$$$$ > $@; \
+	  rm -f $@.$$$$
+
+include $(patsubst %.c,%.d,$(SOURCES))
+
+clean:
+	rm -rf *.o *.d $(USER_TARGET)

dist/Makefile.include

@@ -0,0 +1,5 @@
+USER_TARGET=libmerkletree.a
+USER_CFLAGS=
+USER_C_FILES=
+ALL_C_FILES=LowStar.c MerkleTree.c
+ALL_H_FILES=MerkleTree.h Merkle_Krmllib.h internal/LowStar.h internal/Merkle_EverCrypt.h

dist/libmerkletree.def

@@ -0,0 +1,69 @@
+LIBRARY libmerkletree
+
+EXPORTS
+  LowStar_Vector_new_capacity
+  mt_init_hash
+  mt_free_hash
+  mt_init_path
+  mt_free_path
+  mt_get_path_length
+  mt_path_insert
+  mt_get_path_step
+  mt_get_path_step_pre
+  mt_create_custom
+  mt_free
+  mt_insert
+  mt_insert_pre
+  mt_get_root
+  mt_get_root_pre
+  mt_get_path
+  mt_get_path_pre
+  mt_flush
+  mt_flush_pre
+  mt_flush_to
+  mt_flush_to_pre
+  mt_retract_to
+  mt_retract_to_pre
+  mt_verify
+  mt_verify_pre
+  mt_serialize_size
+  mt_serialize
+  mt_deserialize
+  mt_serialize_path
+  mt_deserialize_path
+  mt_sha256_compress
+  mt_create
+  MerkleTree_Low_uu___is_MT
+  MerkleTree_Low_merkle_tree_conditions
+  MerkleTree_Low_offset_of
+  MerkleTree_Low_mt_free
+  MerkleTree_Low_mt_insert_pre
+  MerkleTree_Low_mt_insert
+  MerkleTree_Low_mt_create_custom
+  MerkleTree_Low_uu___is_Path
+  MerkleTree_Low_init_path
+  MerkleTree_Low_clear_path
+  MerkleTree_Low_free_path
+  MerkleTree_Low_mt_get_root_pre
+  MerkleTree_Low_mt_get_root
+  MerkleTree_Low_mt_path_insert
+  MerkleTree_Low_mt_get_path_length
+  MerkleTree_Low_mt_get_path_step_pre
+  MerkleTree_Low_mt_get_path_step
+  MerkleTree_Low_mt_get_path_pre
+  MerkleTree_Low_mt_get_path
+  MerkleTree_Low_mt_flush_to_pre
+  MerkleTree_Low_mt_flush_to
+  MerkleTree_Low_mt_flush_pre
+  MerkleTree_Low_mt_flush
+  MerkleTree_Low_mt_retract_to_pre
+  MerkleTree_Low_mt_retract_to
+  MerkleTree_Low_mt_verify_pre
+  MerkleTree_Low_mt_verify
+  MerkleTree_Low_Serialization_mt_serialize_size
+  MerkleTree_Low_Serialization_mt_serialize
+  MerkleTree_Low_Serialization_mt_deserialize
+  MerkleTree_Low_Serialization_mt_serialize_path
+  MerkleTree_Low_Serialization_mt_deserialize_path
+  MerkleTree_Low_Hashfunctions_init_hash
+  MerkleTree_Low_Hashfunctions_free_hash