1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
BENCH ?= no
ifeq ($(BENCH),yes)
WHY3=../../bin/why3.opt
WHY3SHARE=../../share
else
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
WHY3SHARE=$(shell $(WHY3) --print-datadir)
endif
include $(WHY3SHARE)/Makefile.config
ifeq ($(BENCH),yes)
INCLUDE += -I ../../lib/why3
endif
MAIN=main
GEN=base64
OBJ=$(GEN)
GENML = $(addsuffix .ml, $(GEN))
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
CMX = $(addsuffix .cmx, $(OBJ))
OCAMLOPT=ocamlopt -noassert -inline 1000
all: $(MAIN).$(OCAMLBEST)
extract: $(GENML)
doc:
$(WHY3) doc ../string_base64_encoding.mlw
$(WHY3) session html .
$(MAIN).opt: $(CMX) $(MAIN).cmx
$(OCAMLOPT) $(INCLUDE) zarith.cmxa -o $@ $^
$(MAIN).cmx: $(CMX)
$(GENML): ../string_base64_encoding.mlw
$(WHY3) extract -D ocaml64 -L .. -o $@ ../string_base64_encoding.mlw
%.cmx: %.ml
$(OCAMLOPT) $(INCLUDE) -annot -c $<
clean::
rm -f $(GENML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
rm -f gcd__*.ml*
%.cmo: %.ml
$(JSOCAMLC) $(INCLUDE) -annot -c $<
%.cmi: %.mli
$(JSOCAMLC) $(INCLUDE) -annot -c $<
clean::
rm -f *.cm[io] $(NAME).byte $(NAME).js
|
