Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
b6b8ad62
Commit
b6b8ad62
authored
6 years ago
by
Patrick Baudin
Committed by
Julien Signoles
6 years ago
Browse files
Options
Downloads
Patches
Plain Diff
[Makefile] distribution in internal/external compilation mode
parent
1dccebda
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/plugins/e-acsl/Makefile.in
+41
-29
41 additions, 29 deletions
src/plugins/e-acsl/Makefile.in
src/plugins/e-acsl/headers/header_spec.txt
+0
-7
0 additions, 7 deletions
src/plugins/e-acsl/headers/header_spec.txt
with
41 additions
and
36 deletions
src/plugins/e-acsl/Makefile.in
+
41
−
29
View file @
b6b8ad62
...
@@ -231,9 +231,9 @@ clean::
...
@@ -231,9 +231,9 @@ clean::
# Cleaning #
# Cleaning #
############
############
EACSL_CLEANFILES
=
$(
wildcard
doc/doxygen/doxygen.cfg
\
EACSL_CLEANFILES
=
doc/doxygen/doxygen.cfg
\
Makefile config.log config.status configure .depend autom4te.cache/
*
\
Makefile config.log config.status configure .depend autom4te.cache/
*
\
META.frama-c-e_acsl Makefile.plugin.generated local_config.ml top/
*
)
META.frama-c-e_acsl Makefile.plugin.generated local_config.ml top/
*
e-acsl-distclean
::
clean
e-acsl-distclean
::
clean
$(
PRINT_RM
)
generated project files
$(
PRINT_RM
)
generated project files
...
@@ -245,15 +245,12 @@ e-acsl-distclean:: clean
...
@@ -245,15 +245,12 @@ e-acsl-distclean:: clean
EXPORT
=
e-acsl-
$(
EACSL_VERSION
)
EXPORT
=
e-acsl-
$(
EACSL_VERSION
)
EACSL_OCAML_FILES
=
$(
wildcard
*
.mli
)
\
$(
filter-out
$(
wildcard
*
local_config.ml
)
,
$(
wildcard
*
.ml
))
EACSL_CONTRIB_FILES
=
\
EACSL_CONTRIB_FILES
=
\
$(
EACSL_GMP_REL_DIR
)
/mini-gmp.c
\
$(
EACSL_GMP_REL_DIR
)
/mini-gmp.c
\
$(
EACSL_GMP_REL_DIR
)
/mini-gmp.h
\
$(
EACSL_GMP_REL_DIR
)
/mini-gmp.h
\
$(
EACSL_DLMALLOC_REL_DIR
)
/dlmalloc.c
$(
EACSL_DLMALLOC_REL_DIR
)
/dlmalloc.c
EACSL_MANUAL_FILES
=
$(
wildcard
$(
E_ACSL_DIR
)
/
doc/manuals/
*
.pdf
)
EACSL_MANUAL_FILES
=
doc/manuals/
*
.pdf
EACSL_DOC_FILES
=
\
EACSL_DOC_FILES
=
\
$(
EACSL_MANUAL_FILES
)
\
$(
EACSL_MANUAL_FILES
)
\
...
@@ -262,14 +259,16 @@ EACSL_DOC_FILES = \
...
@@ -262,14 +259,16 @@ EACSL_DOC_FILES = \
man/e-acsl-gcc.sh.1
man/e-acsl-gcc.sh.1
EACSL_TEST_FILES
=
\
EACSL_TEST_FILES
=
\
tests/test_config.in tests/print.ml
\
tests/test_config.in tests/print.ml
# Test files without header management
EACSL_DISTRIB_TESTS
=
\
$(
foreach
dir
,
$(
addprefix tests/,
$(
PLUGIN_TESTS_DIRS
))
,
\
$(
foreach
dir
,
$(
addprefix tests/,
$(
PLUGIN_TESTS_DIRS
))
,
\
$(
wildcard
\
$(
dir
)
/
*
.[ic]
\
$(
dir
)
/
*
.[ic]
\
$(
dir
)
/test_config
\
$(
dir
)
/test_config
\
$(
dir
)
/oracle/
*
.c
\
$(
dir
)
/oracle/
*
.c
\
$(
dir
)
/oracle/
*
.oracle
\
$(
dir
)
/oracle/
*
.oracle
\
)
)
)
EACSL_RTL_FILES
=
$(
EACSL_RTL_SRC
)
EACSL_RTL_FILES
=
$(
EACSL_RTL_SRC
)
...
@@ -284,7 +283,7 @@ EACSL_MISC_FILES = \
...
@@ -284,7 +283,7 @@ EACSL_MISC_FILES = \
EACSL_SHARE_FILES
=
share/e-acsl/
*
.[ch] share/e-acsl/
*
/
*
.[ch]
EACSL_SHARE_FILES
=
share/e-acsl/
*
.[ch] share/e-acsl/
*
/
*
.[ch]
PLUGIN
_DISTRIB_EXTERNAL
:
=
\
EACSL
_DISTRIB_EXTERNAL
=
\
$(
EACSL_SHARE_FILES
)
\
$(
EACSL_SHARE_FILES
)
\
$(
EACSL_MISC_FILES
)
\
$(
EACSL_MISC_FILES
)
\
$(
EACSL_DOC_FILES
)
\
$(
EACSL_DOC_FILES
)
\
...
@@ -294,38 +293,57 @@ PLUGIN_DISTRIB_EXTERNAL:=\
...
@@ -294,38 +293,57 @@ PLUGIN_DISTRIB_EXTERNAL:=\
$(
EACSL_LICENSE_FILES
)
\
$(
EACSL_LICENSE_FILES
)
\
$(
EACSL_CONTRIB_FILES
)
$(
EACSL_CONTRIB_FILES
)
EACSL_DISTRIB_FILES
:=
$(
PLUGIN_DISTRIB_EXTERNAL
)
$(
EACSL_OCAML_FILES
)
PLUGIN_DISTRIB_EXTERNAL
:=
$(
EACSL_DISTRIB_EXTERNAL
)
# Files of `DISTRIB_FILES` without header that is not listed into `headers/header_specs.txt` (with a `.ignore` attribute).
PLUGIN_HEADER_EXCEPTIONS
:=
# Files that are not listed by `DISTRIB_FILES` (and by the way, without header management) decicated to distributed tests
PLUGIN_DISTRIB_TESTS
:=
$(
EACSL_DISTRIB_TESTS
)
# for e-csl-distrib target:
EACSL_OCAML_FILES
=
*
.mli
\
$(
patsubst
$(
EACSL_PLUGIN_DIR
)
/%,%,
\
$(
filter-out
$(
wildcard
$(
EACSL_PLUGIN_DIR
)
/
*
local_config.ml
)
,
$(
wildcard
$(
EACSL_PLUGIN_DIR
)
/
*
.ml
)))
EACSL_DISTRIB_FILES
=
\
$(
patsubst
$(
EACSL_PLUGIN_DIR
)
/%,%,
\
$(
wildcard
$(
addprefix
$(
EACSL_PLUGIN_DIR
)
/,
\
$(
EACSL_OCAML_FILES
)
$(
EACSL_DISTRIB_EXTERNAL
)
$(
EACSL_DISTRIB_TESTS
))))
# BE CAREFUL: manually remove all *.ml* files which should not be released!
# BE CAREFUL: manually remove all *.ml* files which should not be released!
e-acsl-distrib
:
e-acsl-distrib
:
$(
PRINT_TAR
)
tmp-distrib
$(
PRINT_TAR
)
tmp-distrib
$(
TAR
)
cf tmp.tar
$(
EACSL_DISTRIB_FILES
)
cd
$(
EACSL_PLUGIN_DIR
);
\
$(
TAR
)
cf tmp.tar
$(
EACSL_DISTRIB_FILES
)
$(
PRINT_MAKING
)
export
directories
$(
PRINT_MAKING
)
export
directories
$(
MKDIR
)
$(
EXPORT
)
$(
MKDIR
)
$(
EACSL_PLUGIN_DIR
)
/
$(
EXPORT
)
$(
PRINT_UNTAR
)
tmp-distrib
$(
PRINT_UNTAR
)
tmp-distrib
cd
$(
EXPORT
);
\
cd
$(
EACSL_PLUGIN_DIR
)
/
$(
EXPORT
);
\
pwd
&&
\
$(
TAR
)
xf ../tmp.tar
&&
\
$(
TAR
)
xf ../tmp.tar
&&
\
autoconf
&&
\
autoconf
&&
\
$(
SED
)
-i
-e
's/IS_DISTRIBUTED:=no/IS_DISTRIBUTED:=yes/'
Makefile.in
&&
\
$(
SED
)
-i
-e
's/IS_DISTRIBUTED:=no/IS_DISTRIBUTED:=yes/'
Makefile.in
&&
\
$(
RM
)
-rf
autom4te.cache
$(
RM
)
-rf
autom4te.cache
$(
PRINT_RM
)
tmp-distrib
$(
PRINT_RM
)
tmp-distrib
$(
RM
)
tmp.tar
$(
RM
)
$(
EACSL_PLUGIN_DIR
)
/tmp.tar
$(
PRINT_MAKING
)
archive
$(
PRINT_MAKING
)
archive
$(
EACSL_PLUGIN_DIR
)
/
$(
EXPORT
)
.tar.gz
$(
TAR
)
czf
$(
EXPORT
)
.tar.gz
$(
EXPORT
)
cd
$(
EACSL_PLUGIN_DIR
)
;
\
$(
TAR
)
czf
$(
EXPORT
)
.tar.gz
$(
EXPORT
)
$(
PRINT
)
Cleaning
$(
PRINT
)
Cleaning
$(
RM
)
-fr
$(
EXPORT
)
$(
RM
)
-fr
$(
EACSL_PLUGIN_DIR
)
/
$(
EXPORT
)
WWW
?=
/localhome/julien/frama-c/doc/www
WWW
?=
/localhome/julien/frama-c/doc/www
e-acsl-install-distrib
:
e-acsl-distrib
e-acsl-install-distrib
:
e-acsl-distrib
$(
PRINT
)
Copying to website
$(
PRINT
)
Copying to website
$(
CP
)
$(
EXPORT
)
.tar.gz
$(
WWW
)
/distrib/download/e-acsl
$(
CP
)
$(
EACSL_PLUGIN_DIR
)
/
$(
EXPORT
)
.tar.gz
$(
WWW
)
/distrib/download/e-acsl
$(
CP
)
$(
EACSL_DOC_FILES
)
$(
WWW
)
/distrib/download/e-acsl
$(
CP
)
$(
addprefix
$(
EACSL_PLUGIN_DIR
)
/,
$(
EACSL_DOC_FILES
)
)
$(
WWW
)
/distrib/download/e-acsl
ifneq
("$(EACSL_MANUAL_FILES)","")
ifneq
("$(EACSL_MANUAL_FILES)","")
$(
CP
)
doc/manuals/e-acsl-manual.pdf
\
$(
CP
)
$(
EACSL_PLUGIN_DIR
)
/
doc/manuals/e-acsl-manual.pdf
\
$(
WWW
)
/distrib/download/e-acsl/e-acsl-manual-
$(
EACSL_VERSION
)
.pdf
$(
WWW
)
/distrib/download/e-acsl/e-acsl-manual-
$(
EACSL_VERSION
)
.pdf
$(
CP
)
doc/manuals/e-acsl.pdf
\
$(
CP
)
$(
EACSL_PLUGIN_DIR
)
/
doc/manuals/e-acsl.pdf
\
$(
WWW
)
/distrib/download/e-acsl/e-acsl-1.7.pdf
$(
WWW
)
/distrib/download/e-acsl/e-acsl-1.7.pdf
$(
CP
)
doc/manuals/e-acsl-implementation.pdf
\
$(
CP
)
$(
EACSL_PLUGIN_DIR
)
/
doc/manuals/e-acsl-implementation.pdf
\
$(
WWW
)
/distrib/download/e-acsl/e-acsl-implementation-
$(
EACSL_VERSION
)
.pdf
$(
WWW
)
/distrib/download/e-acsl/e-acsl-implementation-
$(
EACSL_VERSION
)
.pdf
endif
endif
...
@@ -349,12 +367,6 @@ e-acsl-distrib-check:
...
@@ -349,12 +367,6 @@ e-acsl-distrib-check:
# Header #
# Header #
##########
##########
# Files of `DISTRIB_FILES` without header that is not listed into `headers/header_specs.txt` (with a `.ignore` attribute).
PLUGIN_HEADER_EXCEPTIONS
=
# Files that are not listed by `DISTRIB_FILES` (and by the way, without header management) decicated to distributed tests
PLUGIN_DISTRIB_TESTS
=
ifneq
("$(FRAMAC_INTERNAL)","yes")
ifneq
("$(FRAMAC_INTERNAL)","yes")
EACSL_SPARETIMELABS
=
$(
EACSL_PLUGIN_DIR
)
/share/e-acsl/e_acsl_printf.h
EACSL_SPARETIMELABS
=
$(
EACSL_PLUGIN_DIR
)
/share/e-acsl/e_acsl_printf.h
...
...
This diff is collapsed.
Click to expand it.
src/plugins/e-acsl/headers/header_spec.txt
+
0
−
7
View file @
b6b8ad62
...
@@ -21,8 +21,6 @@ exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
...
@@ -21,8 +21,6 @@ exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
gmpr.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
gmpr.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
gmpz.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
gmpz.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
gmpz.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
gmpz.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
...
@@ -31,8 +29,6 @@ keep_status.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
...
@@ -31,8 +29,6 @@ keep_status.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
keep_status.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
keep_status.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
label.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
label.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
lfunctions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
lfunctions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
license/CEA_LGPL: .ignore
license/CEA_LGPL: .ignore
license/LGPLv2.1: .ignore
license/LGPLv2.1: .ignore
license/SPARETIMELABS: .ignore
license/SPARETIMELABS: .ignore
...
@@ -78,7 +74,6 @@ share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
...
@@ -78,7 +74,6 @@ share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_safe_locations.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_safe_locations.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_shexec.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_shexec.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_string.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_string.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_stubs_for_real.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_temporal.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_temporal.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_temporal_timestamp.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_temporal_timestamp.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_trace.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_trace.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
...
@@ -91,8 +86,6 @@ tests/print.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
...
@@ -91,8 +86,6 @@ tests/print.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
tests/test_config.in: .ignore
tests/test_config.in: .ignore
translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
translate_lfunctions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
translate_lfunctions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
typing.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
typing.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
typing.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
typing.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
visit.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
visit.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment