Makefile.in 15.6 KB
Newer Older
1
2
##########################################################################
#                                                                        #
Patrick Baudin's avatar
Patrick Baudin committed
3
#  This file is part of the Frama-C's E-ACSL plug-in.                    #
4
#                                                                        #
Andre Maroneze's avatar
Andre Maroneze committed
5
#  Copyright (C) 2012-2020                                               #
6
#    CEA (Commissariat à l'énergie atomique et aux énergies              #
Julien Signoles's avatar
Julien Signoles committed
7
#         alternatives)                                                  #
8
9
10
11
12
13
14
15
16
17
18
#                                                                        #
#  you can redistribute it and/or modify it under the terms of the GNU   #
#  Lesser General Public License as published by the Free Software       #
#  Foundation, version 2.1.                                              #
#                                                                        #
#  It is distributed in the hope that it will be useful,                 #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
#  GNU Lesser General Public License for more details.                   #
#                                                                        #
#  See the GNU Lesser General Public License version 2.1                 #
Virgile Prevosto's avatar
Virgile Prevosto committed
19
#  for more details (enclosed in the file licenses/LGPLv2.1).            #
20
21
22
#                                                                        #
##########################################################################

23
24
25
26
#######################
# Frama-C Environment #
#######################

27
28
29
# Do not use ?= to initialize both below variables
# (fixed efficiency issue, see GNU Make manual, Section 8.11)
ifndef FRAMAC_SHARE
30
FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
31
32
endif

33
34
35
36
37
38
39
40
41
42
43
44
45
46
###################
# Plug-in sources #
###################

# libraries
SRC_LIBRARIES:= \
	error \
	builtins \
	functions \
	misc \
	gmp_types \
	varname
SRC_LIBRARIES:=$(addprefix src/libraries/, $(SRC_LIBRARIES))

47
48
49
50
51
# source files that depend on optional dependencies
SRC_DYN_DEPENDENCIES:= \
	dep_eva
SRC_DYN_DEPENDENCIES:=$(addprefix src/dependencies/, $(SRC_DYN_DEPENDENCIES))

52
53
54
55
56
57
58
# project initializer
SRC_PROJECT_INITIALIZER:= \
	rtl \
	prepare_ast
SRC_PROJECT_INITIALIZER:=\
  $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))

59
60
61
62
# analyses
SRC_ANALYSES:= \
	rte \
	literal_strings \
63
	memory_tracking \
64
65
66
67
68
69
70
	exit_points \
	lscope \
	interval \
	typing
SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))

# code generator
71
72
73
74
CODE_GENERATOR_CMI:= \
	contract_types
CODE_GENERATOR_CMI:=$(addprefix src/code_generator/, $(CODE_GENERATOR_CMI))

75
SRC_CODE_GENERATOR:= \
76
77
	smart_exp \
	smart_stmt \
78
79
80
	gmp \
	label \
	env \
81
	rational \
82
83
84
	loops \
	quantif \
	at_with_lscope \
85
	memory_translate \
86
	logic_functions \
87
	logic_array \
88
	translate \
89
	contract \
90
	translate_annots \
91
	temporal \
92
93
94
	memory_observer \
	literal_observer \
	global_observer \
Julien Signoles's avatar
Julien Signoles committed
95
	injector
96
97
SRC_CODE_GENERATOR:=$(addprefix src/code_generator/, $(SRC_CODE_GENERATOR))

98
99
100
101
#########################
# Plug-in configuration #
#########################

102
PLUGIN_DIR ?=.
103
104
105
PLUGIN_EXTRA_DIRS:=\
	src \
	src/libraries \
106
	src/dependencies \
107
108
109
	src/analyses \
	src/project_initializer \
	src/code_generator
110
111
112
PLUGIN_ENABLE:=@ENABLE_E_ACSL@
PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@
PLUGIN_NAME:=E_ACSL
113
114
PLUGIN_CMO:= src/local_config \
	src/options \
115
	$(SRC_LIBRARIES) \
116
	$(SRC_DYN_DEPENDENCIES) \
117
	$(SRC_PROJECT_INITIALIZER) \
118
	$(SRC_ANALYSES) \
119
	$(SRC_CODE_GENERATOR) \
120
	src/main
121
122
PLUGIN_CMI:= \
	$(CODE_GENERATOR_CMI)
123
PLUGIN_HAS_MLI:=yes
124
PLUGIN_DISTRIBUTED:=yes
125
PLUGIN_DEPENDENCIES:= RteGen
126
PLUGIN_GENERATED:=
127

128
129
130
# We "save" this variable so that it can be used once PLUGIN_DIR has been reset
EACSL_PLUGIN_DIR:=$(PLUGIN_DIR)

131
# Suppress a spurious warning with OCaml >= 4.04.0
132
133
134
$(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmo \
$(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmi: E_ACSL_BFLAGS+= -w -60
$(EACSL_PLUGIN_DIR)/src/analyses/memory_tracking.cmx: E_ACSL_OFLAGS+= -w -60
135

136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
########################
# Dynamic dependencies #
########################

# Distributed files for the dynamic dependencies
EACSL_DISTRIB_DYNDEP:=

# Eva
DEP_EVA :=src/dependencies/dep_eva
DEP_EVA_ENABLED :=$(DEP_EVA).enabled.ml
DEP_EVA_DISABLED :=$(DEP_EVA).disabled.ml
PLUGIN_GENERATED += $(EACSL_PLUGIN_DIR)/$(DEP_EVA).ml

## Add enabled and disabled files to the list of distributed files
## (relative to e-acsl directory)
EACSL_DISTRIB_DYNDEP += $(DEP_EVA_ENABLED) $(DEP_EVA_DISABLED)

## Update enabled and disabled files path to be relative to the root directory
DEP_EVA_ENABLED:=$(addprefix $(EACSL_PLUGIN_DIR)/, $(DEP_EVA_ENABLED))
DEP_EVA_DISABLED:=$(addprefix $(EACSL_PLUGIN_DIR)/, $(DEP_EVA_DISABLED))

## Add Eva to the plugin dependencies if enabled
ifneq "$(ENABLE_EVA)" "no"
	PLUGIN_DEPENDENCIES+= Eva
endif

## Copy enabled or disabled file to the source file that will be used for the
## compilation
$(EACSL_PLUGIN_DIR)/src/dependencies/dep_eva.ml: \
		$(DEP_EVA_ENABLED) $(DEP_EVA_DISABLED) \
		$(EACSL_PLUGIN_DIR)/Makefile share/Makefile.config
	$(PRINT_MAKING) $@
	$(RM) $@
ifneq "$(ENABLE_EVA)" "no"
	$(CP) $(DEP_EVA_ENABLED) $@
else
	$(CP) $(DEP_EVA_DISABLED) $@
endif
	$(CHMOD_RO) $@

176
177
178
###############
# Local Flags #
###############
Julien Signoles's avatar
Julien Signoles committed
179
# Do not edit the line below: it is automatically set by 'make e-acsl-distrib'
180
IS_DISTRIBUTED:=no
181

182
183
184
185
#######################
# Local configuration #
#######################

186
PLUGIN_GENERATED += $(EACSL_PLUGIN_DIR)/src/local_config.ml
187

188
189
190
191
192
193
194
195
VERSION_FILE=$(FRAMAC_ROOT_SRCDIR)/VERSION

################
# Version      #
################

EACSL_VERSION:=$(shell sed -e 's/\\(.*\\)/\\1/' $(VERSION_FILE))

196
$(EACSL_PLUGIN_DIR)/src/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile.in $(VERSION_FILE)
197
	$(PRINT_MAKING) $@
198
	$(RM) $@
199
	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
200
	$(ECHO) "let version = \""$(EACSL_VERSION)"\"" >> $@
201
202
	$(CHMOD_RO) $@

203
204
205
206
###########
# Testing #
###########

207
208
ifeq (@MAY_RUN_TESTS@,yes)

Patrick Baudin's avatar
Patrick Baudin committed
209
210
-include in_frama_ci

Kostyantyn Vorobyov's avatar
Kostyantyn Vorobyov committed
211
PLUGIN_TESTS_DIRS := \
212
	examples \
Kostyantyn Vorobyov's avatar
Kostyantyn Vorobyov committed
213
	bts \
214
	constructs \
215
216
	arith \
	memory \
Julien Signoles's avatar
Julien Signoles committed
217
	gmp-only \
218
	full-mtracking \
219
	format \
Patrick Baudin's avatar
Patrick Baudin committed
220
	temporal \
221
	special
222
223
# [JS 2019/02/26] deactivate tests 'builtin' as long as setjmp/longjmp is not
# supported.
Julien Signoles's avatar
Julien Signoles committed
224
225
#	builtin

226
PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
Julien Signoles's avatar
Julien Signoles committed
227

228
DEV?=
Julien Signoles's avatar
Julien Signoles committed
229
ifeq ("$(DEV)","yes")
230
  EACSL_TEST_CONFIG:=dev
Julien Signoles's avatar
Julien Signoles committed
231
232
233
else
  EACSL_TEST_CONFIG:=ci
endif
234
235
236
237
# Prepend PTESTS_OPTS with the test config to use. If the user-provided
# PTESTS_OPTS variable contains another -config instruction, then it will be
# prioritized over the one selected by the Makefile.
E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: override PTESTS_OPTS:=-config $(EACSL_TEST_CONFIG) $(PTESTS_OPTS)
238

239
TEST_DEPENDENCIES:= \
Julien Signoles's avatar
Julien Signoles committed
240
	$(EACSL_PLUGIN_DIR)/tests/ptests_config \
241
242
	$(EACSL_PLUGIN_DIR)/tests/test_config_ci \
	$(EACSL_PLUGIN_DIR)/tests/test_config_dev \
243
244
245
	$(EACSL_PLUGIN_DIR)/tests/print.cmxs \
	$(EACSL_PLUGIN_DIR)/tests/print.cmo

246
247
248
# Add the test dependencies to the test targets, but also to
# `plugins_ptests_config` so that they are built along with the main target.
plugins_ptests_config: $(TEST_DEPENDENCIES)
249
250
E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: $(TEST_DEPENDENCIES)
tests:: $(TEST_DEPENDENCIES)
251

Julien Signoles's avatar
Julien Signoles committed
252
253
254
255
256
$(EACSL_PLUGIN_DIR)/tests/test_config_ci: \
		$(EACSL_PLUGIN_DIR)/tests/test_config_ci.in \
		$(EACSL_PLUGIN_DIR)/Makefile
	$(PRINT_MAKING) $@
	$(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@
257

Julien Signoles's avatar
Julien Signoles committed
258
259
$(EACSL_PLUGIN_DIR)/tests/test_config_dev: \
		$(EACSL_PLUGIN_DIR)/tests/test_config_dev.in \
Julien Signoles's avatar
Julien Signoles committed
260
261
262
263
		$(EACSL_PLUGIN_DIR)/Makefile
	$(PRINT_MAKING) $@
	$(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@

264
clean::
265
266
267
	for d in $(E_ACSL_EXTRA_DIRS); do \
	  $(RM) $$d/*~; \
	done
268
269
	$(PRINT_RM) cleaning generated test files
	$(RM) $(E_ACSL_DIR)/tests/*.cm* $(E_ACSL_DIR)/tests/*.o
270
271
	$(RM) $(E_ACSL_DIR)/tests/test_config_ci \
		$(E_ACSL_DIR)/tests/test_config_dev
272
273
	$(RM) $(foreach dir, $(PLUGIN_TESTS_DIRS), tests/$(dir)/result/*)

274
275
endif

276
################################################
277
# Third-party C libraries                      #
278
################################################
279

280
EACSL_LIBDIR := $(EACSL_PLUGIN_DIR)/lib
281
282
283
284
285

############
# DLMALLOC #
############

286
287
EACSL_DLMALLOC_REL_DIR := contrib/libdlmalloc
EACSL_DLMALLOC_DIR := $(EACSL_PLUGIN_DIR)/$(EACSL_DLMALLOC_REL_DIR)
288
289
290
291
292
293
294
295
296
EACSL_DLMALLOC_LIBNAME = libeacsl-dlmalloc.a
EACSL_DLMALLOC_LIB = $(EACSL_LIBDIR)/$(EACSL_DLMALLOC_LIBNAME)
EACSL_DLMALLOC_SRC = $(EACSL_DLMALLOC_DIR)/dlmalloc.c
EACSL_DLMALLOC_OBJ  = dlmalloc.o
EACSL_DLMALLOC_FLAGS = \
  -DHAVE_MORECORE=0 \
  -DHAVE_MMAP=1  \
  -DNO_MALLINFO=1 \
  -DNO_MALLOC_STATS=1 \
297
298
299
  -DMSPACES=1 \
  -DONLY_MSPACES \
  -DMALLOC_ALIGNMENT=32 \
300
  -DMSPACE_PREFIX="__e_acsl_"
301
302
303

$(EACSL_DLMALLOC_LIB): $(EACSL_DLMALLOC_SRC)
	$(MKDIR) $(EACSL_LIBDIR)
304
	echo 'CC           $<'
305
	$(CC) $< -c -O2 -g3 -o$(EACSL_DLMALLOC_OBJ) $(EACSL_DLMALLOC_FLAGS)
306
	echo 'AR           $@'
307
	$(AR) crus $@ $(EACSL_DLMALLOC_OBJ)
308
	echo 'RANLIB       $@'
309
	ranlib $@
310

311
all:: $(EACSL_DLMALLOC_LIB)
312

313
clean::
314
	$(RM) $(EACSL_DLMALLOC_LIB)
315

316
317
318
319
############
# Cleaning #
############

320
EACSL_CLEANFILES = doc/doxygen/doxygen.cfg \
321
	Makefile config.log config.status configure .depend autom4te.cache/* \
322
323
324
	META.frama-c-e_acsl Makefile.plugin.generated src/local_config.ml \
	top/* \
	$(TEST_DEPENDENCIES)
325

326
e-acsl-distclean: clean
327
	$(PRINT_RM) generated project files
328
	$(RM) $(wildcard $(addprefix $(E_ACSL_DIR)/, $(EACSL_CLEANFILES)))
329

330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
#################################################################
# Common variables between source distribution and installation #
#################################################################

EACSL_C_DIRECTORIES := \
	e-acsl \
	e-acsl/internals \
	e-acsl/instrumentation_model \
	e-acsl/observation_model \
	e-acsl/observation_model/internals \
	e-acsl/observation_model/bittree_model \
	e-acsl/observation_model/segment_model \
	e-acsl/numerical_model \
	e-acsl/libc_replacements

EACSL_SCRIPTS := \
	scripts/e-acsl-gcc.sh

EACSL_MANPAGES := \
	man/e-acsl-gcc.sh.1

351
352
353
354
################################
# Building source distribution #
################################

355
EACSL_CONTRIB_FILES = \
356
  $(EACSL_DLMALLOC_REL_DIR)/dlmalloc.c
357

358
EACSL_MANUAL_FILES = doc/manuals/*.pdf
359

360
EACSL_DOC_FILES = \
361
	doc/doxygen/doxygen.cfg.in \
362
	doc/Changelog \
363
	$(EACSL_MANPAGES)
364

365
EACSL_TEST_FILES = \
366
367
368
369
	tests/test_config_dev.in \
	tests/test_config_ci.in \
	tests/gmp-only/test_config_ci \
	tests/gmp-only/test_config_dev \
370
371
	tests/full-mtracking/test_config_ci \
	tests/full-mtracking/test_config_dev \
372
373
374
375
376
377
	tests/builtin/test_config_ci \
	tests/builtin/test_config_dev \
	tests/temporal/test_config_ci \
	tests/temporal/test_config_dev \
	tests/format/test_config_ci \
	tests/format/test_config_dev \
Julien Signoles's avatar
Julien Signoles committed
378
	tests/print.ml
379

380
# Test files without header management
381
EACSL_DISTRIB_TESTS = \
382
  $(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
383
      $(dir)/*.[ich] \
384
385
386
387
      $(dir)/test_config_ci \
      $(dir)/test_config_dev \
      $(dir)/oracle_ci/* \
      $(dir)/oracle_dev/* \
388
  )
389

390
EACSL_RTL_FILES = $(EACSL_RTL_SRC)
391

392
EACSL_SCRIPT_FILES = $(EACSL_SCRIPTS)
393

394
EACSL_LICENSE_FILES = \
395
396
  license/CEA_LGPL license/SPARETIMELABS \
  license/headache_config.txt license/LGPLv2.1
397

398
EACSL_MISC_FILES = \
399
  configure.ac Makefile.in README
400

401
402
EACSL_SHARE_FILES = \
	$(addprefix share/,$(addsuffix /*.[ch],$(EACSL_C_DIRECTORIES)))
403

404
EACSL_DISTRIB_EXTERNAL =\
405
  $(EACSL_DISTRIB_DYNDEP) \
406
  $(EACSL_SHARE_FILES) \
407
408
409
410
411
412
  $(EACSL_MISC_FILES) \
  $(EACSL_DOC_FILES) \
  $(EACSL_TEST_FILES) \
  $(EACSL_RTL_FILES) \
  $(EACSL_SCRIPT_FILES) \
  $(EACSL_LICENSE_FILES) \
413
  $(EACSL_CONTRIB_FILES)
414

415
416
PLUGIN_DISTRIB_EXTERNAL:= $(EACSL_DISTRIB_EXTERNAL)

417
418
# Files of `DISTRIB_FILES` without header and not listed in file
# `headers/header_specs.txt`.
419
420
PLUGIN_HEADER_EXCEPTIONS:=

421
# Files that are not listed in `DISTRIB_FILES`
422
# and dedicated to distributed tests
423
424
PLUGIN_DISTRIB_TESTS:= $(EACSL_DISTRIB_TESTS)

425
426
427
428
429
430
431
########
# Misc #
########

wc:
	ocamlwc -p $(EACSL_OCAML_FILES)

Julien Signoles's avatar
Julien Signoles committed
432
433
434
435
##########
# Header #
##########

Patrick Baudin's avatar
Patrick Baudin committed
436
ifneq ("$(FRAMAC_INTERNAL)","yes")
437

438
439
440
EACSL_SPARETIMELABS= \
	$(EACSL_PLUGIN_DIR)/share/e-acsl/internals/e_acsl_rtl_io.h \
	$(EACSL_PLUGIN_DIR)/share/e-acsl/internals/e_acsl_rtl_io.c
441

442
443
EACSL_SHARE_BARE= \
	$(addprefix share/,$(addsuffix /*.[ch],$(EACSL_C_DIRECTORIES)))
Patrick Baudin's avatar
Patrick Baudin committed
444
445
446
EACSL_SHARE=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_SHARE_BARE))
EACSL_CEA_SHARE=$(filter-out $(EACSL_SPARETIMELABS), $(wildcard $(EACSL_SHARE)))

447
448
449
450
451
452
EACSL_CEA_LGPL_BARE= src/*.ml src/*/*.ml src/*.mli src/*/*.mli \
	E_ACSL.mli \
	Makefile.in configure.ac \
	scripts/*.sh \
	tests/print.ml \
	man/e-acsl-gcc.sh.1
Patrick Baudin's avatar
Patrick Baudin committed
453
454
455
EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE)) \
               $(EACSL_CEA_SHARE)

456
# valid values: open-source, close-source
Patrick Baudin's avatar
Patrick Baudin committed
457
EACSL_HEADERS?=open-source
Julien Signoles's avatar
Julien Signoles committed
458
headers::
459
	@echo "Applying $(EACSL_HEADERS) headers..."
460
	headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
Patrick Baudin's avatar
Patrick Baudin committed
461
462
                 -h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/CEA_LGPL_OR_PROPRIETARY.E_ACSL \
                 $(EACSL_CEA_LGPL)
463
	headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
Patrick Baudin's avatar
Patrick Baudin committed
464
                 -h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_SPARETIMELABS \
465
                 $(EACSL_SPARETIMELABS)
Patrick Baudin's avatar
Patrick Baudin committed
466
467
468
	headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
                 -h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_DLMALLOC \
                 $(EACSL_PLUGIN_DIR)/contrib/libdlmalloc/dlmalloc.c
469

Patrick Baudin's avatar
Patrick Baudin committed
470
endif
Julien Signoles's avatar
Julien Signoles committed
471

472
473
474
################
# Generic part #
################
475
476
477

include $(FRAMAC_SHARE)/Makefile.dynamic

478
479
480
481
###########
# Install #
###########

482
483
EACSL_INSTALL_MANUAL_FILES=$(wildcard $(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_MANUAL_FILES)))

484
485
486
EACSL_INSTALL_SCRIPTS=$(addprefix $(E_ACSL_DIR)/,$(EACSL_SCRIPTS))

EACSL_INSTALL_MANPAGES=$(addprefix $(E_ACSL_DIR)/,$(EACSL_MANPAGES))
487

488
489
install::
	$(PRINT_INSTALL) E-ACSL share files
490
	for dir in $(EACSL_C_DIRECTORIES); do \
491
492
493
494
495
		$(MKDIR) $(FRAMAC_DATADIR)/$$dir && \
		$(CP) $(E_ACSL_DIR)/share/$$dir/*.[ch] $(FRAMAC_DATADIR)/$$dir ; \
	done
	# manuals are not present in standard distribution.
	# Don't fail because of that.
496
ifneq ("$(EACSL_INSTALL_MANUAL_FILES)","")
497
498
	$(PRINT_INSTALL) E-ACSL manuals
	$(MKDIR) $(FRAMAC_DATADIR)/manuals
499
	$(CP) $(EACSL_INSTALL_MANUAL_FILES) $(FRAMAC_DATADIR)/manuals;
500
endif
501
502
	$(PRINT_INSTALL) E-ACSL libraries
	$(MKDIR) $(LIBDIR)
503
	$(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(LIBDIR)
504
505
	$(PRINT_INSTALL) E-ACSL scripts
	$(MKDIR) $(BINDIR)
506
	$(CP) $(EACSL_INSTALL_SCRIPTS) $(BINDIR)/
507
508
	$(PRINT_INSTALL) E-ACSL man pages
	$(MKDIR) $(MANDIR)/man1
509
510
511
512
513
514
	$(CP) $(EACSL_INSTALL_MANPAGES) $(MANDIR)/man1/


EACSL_INSTALLED_SCRIPTS=$(addprefix $(BINDIR)/,$(notdir $(EACSL_SCRIPTS)))

EACSL_INSTALLED_MANPAGES=$(addprefix $(MANDIR)/man1/,$(notdir $(EACSL_MANPAGES)))
515
516
517
518
519

uninstall::
	$(PRINT_RM) E-ACSL share files
	$(RM) -r $(FRAMAC_DATADIR)/e-acsl
	$(PRINT_RM) E-ACSL manuals
520
	$(RM) $(FRAMAC_DATADIR)/manuals/*.pdf
521
	$(PRINT_RM) E-ACSL libraries
522
	$(RM) $(LIBDIR)/libeacsl-*.a
523
	$(PRINT_RM) E-ACSL scripts
524
	$(RM) $(EACSL_INSTALLED_SCRIPTS)
Patrick Baudin's avatar
Patrick Baudin committed
525
	$(PRINT_RM) E-ACSL man pages
526
	$(RM) $(EACSL_INSTALLED_MANPAGES)
527

528
529
530
531
#####################################
# Regenerating the Makefile on need #
#####################################

Julien Signoles's avatar
Julien Signoles committed
532
ifeq ("$(FRAMAC_INTERNAL)","yes")
533
534
CONFIG_STATUS_DIR:=$(FRAMAC_SRC)
CONFIG_STATUS_DIR_DEP:=
Julien Signoles's avatar
Julien Signoles committed
535
else
536
537
CONFIG_STATUS_DIR:=$(E_ACSL_DIR)
CONFIG_STATUS_DIR_DEP:=$(CONFIG_STATUS_DIR)/config.status
Julien Signoles's avatar
Julien Signoles committed
538
539
endif

540
$(E_ACSL_DIR)/Makefile: $(E_ACSL_DIR)/Makefile.in $(CONFIG_STATUS_DIR_DEP)
Julien Signoles's avatar
Julien Signoles committed
541
	cd $(CONFIG_STATUS_DIR) && ./config.status
542
543

#####################################
544
# Doxygen                           #
545
#####################################
546

547
548
549
DOXYGEN = @DOXYGEN@
doxygen:
	if ! test $(DOXYGEN) = "no"; then \
550
		$(DOXYGEN) $(E_ACSL_DIR)/doc/doxygen/doxygen.cfg ; \
551
	else \
552
		echo "Warning: Skip doxygen documentation: \
553
Doxygen executable not found."; \
554
555
	fi

556
doc:: doxygen
557
558
559
560
561

clean::
	$(PRINT_RM) generated documentation
	$(RM) $(E_ACSL_DIR)/doc/doxygen/html/*
	$(RM) $(E_ACSL_DIR)/doc/code/*
562
	$(RM) $(E_ACSL_DIR)/doc/doxygen/warn.log