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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
# Generated automatically from Makefile.common.in by configure.
WHYBIN=../../bin/why.opt
WHY=WHYLIB=../../lib $(WHYBIN) -split-user-conj
GWHY=WHYLIB=../../lib ../../bin/gwhy.opt -split-user-conj --lib-file arrays.why
CADUCEUS=WHYLIB=../../lib ../../bin/caduceus.opt
# WHYOPTIONS=--coq-v8
WHYOPTIONS=--coq-v8 --valid
DP=../../bin/why-dp.opt
dp: simplify cvcl
coq: $(VO:_valid.vo=_why.vo)
simplify: $(VO:_valid.vo=_why.sx)
$(DP) -timeout 10 $^ 2>/dev/null
yices: $(VO:_valid.vo=_why.smt)
$(DP) -smt-solver yices -timeout 10 $^ 2>/dev/null
z3: $(VO:_valid.vo=_why.z3.smt)
$(DP) -smt-solver z3 -timeout 10 $^ 2>/dev/null
z3smt: $(VO:_valid.vo=_why.smt)
$(DP) -smt-solver z3 -timeout 10 $^ 2>/dev/null
zenon: $(VO:_valid.vo=_why.znn)
$(DP) -timeout 10 $^ 2>/dev/null
cvcl: $(VO:_valid.vo=_why.cvc)
$(DP) -timeout 10 $^ 2>/dev/null
ergo: $(VO:_valid.vo=_why.why)
$(DP) -timeout 10 $^ 2>/dev/null
.PHONY: check
check: $(VO:_valid.vo=.check)
harvey: $(VO:_valid.vo=_why.rv)
$(DP) -timeout 10 $^ 2>/dev/null
%_valid.v %_why.v: %.mlw $(WHYBIN)
$(WHY) $(WHYOPTIONS) $<
%_valid.v %_why.v: %.c $(CADUCEUS)
$(CADUCEUS) $<
%_why.vo: %_why.v
coqc -I ../../lib/coq $(OPT) $<
%_valid.vo: %_valid.v %_why.vo
coqc -I ../../lib/coq $(OPT) $<
%.vo: %.v
coqc -I ../../lib/coq $(OPT) $<
%_why.pvs: %.mlw $(WHYBIN)
$(WHY) --pvs $<
%_why.sx: %.mlw $(WHYBIN)
$(WHY) --simplify $<
%_why.smt: %.mlw $(WHYBIN)
$(WHY) --smtlib --encoding sstrat $<
%_why.z3.smt: %.mlw $(WHYBIN)
$(WHY) --z3 --encoding sstrat $<
%_why.znn: %.mlw $(WHYBIN)
$(WHY) --zenon $<
%_why.cvc: %.mlw $(WHYBIN)
$(WHY) --cvcl $<
%_why.why: %.mlw $(WHYBIN)
$(WHY) --why $<
%_why.why: %.why $(WHYBIN)
$(WHY) --why $<
%.check: %.mlw $(WHYBIN)
$(WHYBIN) -tc $<
%.check: %.why $(WHYBIN)
$(WHYBIN) -tc $<
%_why.rv: %.mlw $(WHYBIN)
$(WHY) --harvey $<
%_why.miz: %.mlw $(WHYBIN)
$(WHY) --mizar $<
%_why.miz: %.c $(WHYBIN)
$(WHY) --mizar $<
%.ml: %.mlw
$(WHY) -ocaml $< > $@
ocamlc -c -i $@
%.wol: %.mlw
$(WHY) --wol $<
%.gui: %.mlw
$(GWHY) $<
%.gui: %.why
$(GWHY) $<
%.fastwp: %.mlw
$(GWHY) -fast-wp $<
clean::
rm -f *~ *.vo *.wol
rm -f *_valid.v
depend:: $(VO:.vo=.v)
coqdep -I ../../lib/coq *.v > .depend
include .depend
|
