-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile
141 lines (104 loc) · 4.48 KB
/
Makefile
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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
CC := gcc
CFLAGS := -Wall -Werror
GEN_CFLAGS := -w
EXT_CFLAGS := -DOUT_OF_TASK
BINDIR := bin
GENDIR := gen
EACSLDIR := $(GENDIR)/eacsl
RTEDIR := $(GENDIR)/rte
VALDIR := $(GENDIR)/val
GENBINDIR := $(BINDIR)/gen
EACSLBINDIR := $(GENBINDIR)/eacsl
FRAMAC := frama-c
FRAMAC_DFLAGS := -jessie
FRAMAC_REPLAY := -jessie-target why3autoreplay
FRAMAC_EFLAGS := -e-acsl -pp-annot -cpp-extra-args " -C -E -x c $(EXT_CFLAGS) "
FRAMAC_EGEN := -then-last -print -ocode
FRAMAC_RTEFLAGS := -rte -rte-all -rte-precond -pp-annot -cpp-extra-args " -C -E -x c $(EXT_CFLAGS) "
FRAMAC_VALFLAGS := -val -pp-annot -cpp-extra-args " -C -E -x c $(EXT_CFLAGS) "
FRAMAC_VALGEN := -print -ocode
FRAMAC_ESHARE := $(shell frama-c -print-share-path)/e-acsl
FRAMAC_EMSHARE := $(shell frama-c -print-share-path)/e-acsl/memory_model
FRAMAC_EACSL_LIB := $(FRAMAC_ESHARE)/e_acsl.c $(FRAMAC_EMSHARE)/e_acsl_bittree.c $(FRAMAC_EMSHARE)/e_acsl_mmodel.c
CFLAGS += $(EXT_CFLAGS)
SRCFILES := $(sort $(shell find . -maxdepth 1 -type f -name '*.c'))
BINFILES := $(patsubst ./%.c, $(BINDIR)/%, $(SRCFILES))
EACSLFILES := $(patsubst ./%.c, $(EACSLDIR)/%.c, $(SRCFILES))
RTEFILES := $(patsubst ./%.c, $(RTEDIR)/%.c, $(SRCFILES))
VALFILES := $(patsubst ./%.c, $(VALDIR)/%.c, $(SRCFILES))
EACSLBINFILES := $(patsubst $(EACSLDIR)/%.c, $(EACSLBINDIR)/%, $(EACSLFILES))
all: build ## Default target. Build each program.
build: $(BINDIR) $(BINFILES) ## Build each program.
eacsl: $(GENDIR) $(EACSLDIR) $(EACSLFILES) ## Generate E-ACSL programs.
eacsl-build: eacsl $(GENBINDIR) $(EACSLBINDIR) $(EACSLBINFILES) ## Build generated E-ACSL programs.
rte: $(GENDIR) $(RTEDIR) $(RTEFILES) ## Generate RTE specifications.
val: $(GENDIR) $(VALDIR) $(VALFILES) ## Run value analysis.
$(BINDIR):
@-mkdir -p $(BINDIR)
$(GENDIR):
@-mkdir -p $(GENDIR)
$(EACSLDIR):
@-mkdir -p $(EACSLDIR)
$(RTEDIR):
@-mkdir -p $(RTEDIR)
$(VALDIR):
@-mkdir -p $(VALDIR)
$(GENBINDIR):
@-mkdir -p $(GENBINDIR)
$(EACSLBINDIR):
@-mkdir -p $(EACSLBINDIR)
$(BINDIR)/%: %.c
$(CC) $(CFLAGS) $< -o $@
$(EACSLDIR)/%.c: %.c
$(FRAMAC) $(FRAMAC_EFLAGS) $< $(FRAMAC_EGEN) $@
$(RTEDIR)/%.c: %.c
$(FRAMAC) $(FRAMAC_RTEFLAGS) $< $(FRAMAC_RTEGEN) $@
$(VALDIR)/%.c: %.c
$(FRAMAC) $(FRAMAC_VALFLAGS) $< $(FRAMAC_VALGEN) $@
$(GENBINDIR)/%: $(GENDIR)/%.c
$(CC) $(GEN_CFLAGS) $(FRAMAC_EACSL_LIB) $< -o $@
run: build ## Run each program. You can also type run-<target>.
@for i in $(BINFILES); do echo $$i; ./$$i; done
run-%: $(BINDIR) $(BINDIR)/%
$(BINDIR)/$*
eacsl-run: eacsl-build ## Run each E-ACSL program. You can also type eacsl-run-<target>.
@for i in $(GENBINFILES); do echo $$i; ./$$i; done
eacsl-run-%: $(GENDIR) $(GENBINDIR) $(GENBINDIR)/%
$(GENBINDIR)/$*
verify: ## Run Frama-C on all files simultaneously. You can also type verify-<target>.
@$(FRAMAC) $(FRAMAC_DFLAGS) $(SRCFILES)
verify-separatedly: ## Run Frama-C on each file consequently.
@for i in $(SRCFILES); do echo $$i; $(FRAMAC) $(FRAMAC_DFLAGS) $$i; done
verify-%:
@$(FRAMAC) $(FRAMAC_DFLAGS) $*.c
replay: ## Replay proofs simultaiously. You can also type replay-<target>.
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_REPLAY) $(SRCFILES)
replay-separatedly: ## Replay proofs consequently.
@for i in $(SRCFILES); do echo $$i; $(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_REPLAY) $$i; done
replay-%:
@$(FRAMAC) $(FRAMAC_DFLAGS) $(FRAMAC_REPLAY) $*.c
clean: ## Remove all binary and generated files.
-rm -fr $(GENBINDIR) $(RTEDIR) $(VALDIR) $(EACSLDIR) $(BINDIR) $(GENDIR)
.PHONY: all build eacsl eacsl-build rte val run eacsl-run verify verify-separatedly replay replay-separatedly clean
#COLORS
GREEN := $(shell tput -Txterm setaf 2)
WHITE := $(shell tput -Txterm setaf 7)
YELLOW := $(shell tput -Txterm setaf 3)
RESET := $(shell tput -Txterm sgr0)
# Add the following 'help' target to your Makefile
# And add help text after each target name starting with '\#\#'
# A category can be added with @category
HELP_FUN = \
%help; \
while(<>) { push @{$$help{$$2 // 'options'}}, [$$1, $$3] if /^([a-zA-Z\-]+)\s*:.*\#\#(?:@([a-zA-Z\-]+))?\s(.*)$$/ }; \
print "usage: make [target]\n\n"; \
for (sort keys %help) { \
print "${WHITE}$$_:${RESET}\n"; \
for (@{$$help{$$_}}) { \
$$sep = " " x (32 - length $$_->[0]); \
print " ${YELLOW}$$_->[0]${RESET}$$sep${GREEN}$$_->[1]${RESET}\n"; \
}; \
print "\n"; }
help: ## Show this help.
@perl -e '$(HELP_FUN)' $(MAKEFILE_LIST)
.PHONY: help