Commit 581629e1 authored by Allan Blanchard's avatar Allan Blanchard

Merge branch 'stable/titanium'

Conflicts on version name:
  VERSION
  VERSION_CODENAME
  opam/opam
parents b741d239 e1e1aca2
...@@ -33,7 +33,7 @@ Open Source Release 22.0 (Titanium) ...@@ -33,7 +33,7 @@ Open Source Release 22.0 (Titanium)
transition, and use such variables in subsequent guards. transition, and use such variables in subsequent guards.
- Kernel [2020-10-09] Add option -print-config-json, to output Frama-C - Kernel [2020-10-09] Add option -print-config-json, to output Frama-C
configuration data in JSON format. configuration data in JSON format.
- Logic [2020-10-XX] '\from' now accepts '&v' expressions - Logic [2020-10-14] '\from' now accepts '&v' expressions
- Metrics [2020-10-01] Distinguish between undefined but specified functions - Metrics [2020-10-01] Distinguish between undefined but specified functions
and functions with neither definition nor specification. and functions with neither definition nor specification.
-* Eva [2020-09-28] Improved string builtins on wide strings: crash fixed, -* Eva [2020-09-28] Improved string builtins on wide strings: crash fixed,
......
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
- [Installing Frama-C from opam repository](#installing-frama-c-from-opam-repository) - [Installing Frama-C from opam repository](#installing-frama-c-from-opam-repository)
- [Installing Custom Versions of Frama-C](#installing-custom-versions-of-frama-c) - [Installing Custom Versions of Frama-C](#installing-custom-versions-of-frama-c)
- [Installing Frama-C on Windows via WSL](#installing-frama-c-on-windows-via-wsl) - [Installing Frama-C on Windows via WSL](#installing-frama-c-on-windows-via-wsl)
- [Installing Frama-C on macOS](#installing-frama-c-on-mac-os) - [Installing Frama-C on macOS](#installing-frama-c-on-macos)
- [Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)](#installing-frama-c-via-your-linux-distribution-debianubuntufedora) - [Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)](#installing-frama-c-via-your-linux-distribution-debianubuntufedora)
- [Compiling from source](#compiling-from-source) - [Compiling from source](#compiling-from-source)
- [Quick Start](#quick-start) - [Quick Start](#quick-start)
...@@ -129,7 +129,7 @@ following tools: ...@@ -129,7 +129,7 @@ following tools:
#### Prerequisites: WSL + a Linux distribution #### Prerequisites: WSL + a Linux distribution
For enabling WSL on Windows, you may follow these instructions For enabling WSL on Windows, you may follow these instructions
(we tested with Ubuntu 18.04 LTS; (we tested with Ubuntu 20.04 LTS;
other distributions/versions should also work, other distributions/versions should also work,
but the instructions below may require some modifications). but the instructions below may require some modifications).
...@@ -158,7 +158,7 @@ Move to your user directory, download the distribution and install it: ...@@ -158,7 +158,7 @@ Move to your user directory, download the distribution and install it:
``` ```
cd C:\Users\<Your User Directory> cd C:\Users\<Your User Directory>
Invoke-WebRequest -Uri https://aka.ms/wsl-ubuntu-1804 -OutFile Ubuntu.appx -UseBasicParsing Invoke-WebRequest -Uri https://aka.ms/wslubuntu2004 -OutFile Ubuntu.appx -UseBasicParsing
Add-AppxPackage .\Ubuntu.appx Add-AppxPackage .\Ubuntu.appx
``` ```
...@@ -171,10 +171,9 @@ For installing opam, some packages are required. The following commands can be ...@@ -171,10 +171,9 @@ For installing opam, some packages are required. The following commands can be
run to update the system and install those packages: run to update the system and install those packages:
``` ```
sudo add-apt-repository -y ppa:avsm/ppa # unnecessary for Ubuntu 20.04
sudo apt update sudo apt update
sudo apt upgrade sudo apt upgrade
sudo apt install make m4 gcc opam sudo apt install make m4 gcc opam yaru-theme-gtk yaru-theme-icon
``` ```
Then opam can be set up using these commands: Then opam can be set up using these commands:
......
...@@ -782,6 +782,7 @@ PLUGIN_DIR:=src/plugins/callgraph ...@@ -782,6 +782,7 @@ PLUGIN_DIR:=src/plugins/callgraph
PLUGIN_CMO:= options journalize subgraph cg services uses register PLUGIN_CMO:= options journalize subgraph cg services uses register
ifeq ($(HAS_DGRAPH),yes) ifeq ($(HAS_DGRAPH),yes)
PLUGIN_GUI_CMO:=cg_viewer PLUGIN_GUI_CMO:=cg_viewer
PLUGIN_DISTRIB_EXTERNAL:=cg_viewer.yes.ml
PLUGIN_GENERATED:=$(PLUGIN_DIR)/cg_viewer.ml PLUGIN_GENERATED:=$(PLUGIN_DIR)/cg_viewer.ml
else else
PLUGIN_GUI_CMO:= PLUGIN_GUI_CMO:=
......
...@@ -96,7 +96,7 @@ via the GUI: ...@@ -96,7 +96,7 @@ via the GUI:
## Further reference ## Further reference
- Links to user and developer manuals, Frama-C archives, - Links to user and developer manuals, Frama-C archives,
and plug-in manuals are available at <br> http://frama-c.com/download.html and plug-in manuals are available at <br> http://beta.frama-c.com/html/get-frama-c.html
- [StackOverflow](http://stackoverflow.com/questions/tagged/frama-c) has several - [StackOverflow](http://stackoverflow.com/questions/tagged/frama-c) has several
questions with the `frama-c` tag, which is monitored by several members of the questions with the `frama-c` tag, which is monitored by several members of the
...@@ -110,9 +110,10 @@ via the GUI: ...@@ -110,9 +110,10 @@ via the GUI:
the [issues tracking system](https://git.frama-c.com/pub/frama-c/issues), the [issues tracking system](https://git.frama-c.com/pub/frama-c/issues),
for reporting bugs. for reporting bugs.
- The [Frama-C wiki](https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:start) - The [Frama-C documentation page](https://beta.frama-c.com/html/documentation.html)
has some useful information, although it is not entirely up-to-date. contains links to all manuals and plugins description, as well as tutorials, courses
and more.
- The [Frama-C blog](http://pub.frama-c.com/blog) has several posts about - The [Frama-C blog](http://beta.frama-c.com/blog) has several posts about
new developments of Frama-C, as well as general discussions about the C new developments of Frama-C, as well as general discussions about the C
language, undefined behavior, floating-point computations, etc. language, undefined behavior, floating-point computations, etc.
...@@ -751,7 +751,7 @@ src/plugins/callgraph/Callgraph.mli: CEA_LGPL_OR_PROPRIETARY ...@@ -751,7 +751,7 @@ src/plugins/callgraph/Callgraph.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/callgraph_api.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/callgraph/callgraph_api.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/cg.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/callgraph/cg.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/cg.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/callgraph/cg.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/cg_viewer.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/callgraph/cg_viewer.yes.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/journalize.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/callgraph/journalize.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/journalize.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/callgraph/journalize.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/options.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/callgraph/options.ml: CEA_LGPL_OR_PROPRIETARY
......
...@@ -65,7 +65,7 @@ authors: [ ...@@ -65,7 +65,7 @@ authors: [
homepage: "http://frama-c.com/" homepage: "http://frama-c.com/"
license: "GNU Lesser General Public License version 2.1" license: "GNU Lesser General Public License version 2.1"
dev-repo: "git+https://git.frama-c.com/pub/frama-c.git" dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
doc: "http://frama-c.com/download/user-manual-22.0-beta-Titanium.pdf" doc: "http://frama-c.com/download/user-manual-21.1-Scandium.pdf"
bug-reports: "https://git.frama-c.com/pub/frama-c/issues" bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
tags: [ tags: [
"deductive" "deductive"
......
...@@ -327,6 +327,27 @@ e-acsl-distclean: clean ...@@ -327,6 +327,27 @@ e-acsl-distclean: clean
$(PRINT_RM) generated project files $(PRINT_RM) generated project files
$(RM) $(wildcard $(addprefix $(E_ACSL_DIR)/, $(EACSL_CLEANFILES))) $(RM) $(wildcard $(addprefix $(E_ACSL_DIR)/, $(EACSL_CLEANFILES)))
#################################################################
# 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
################################ ################################
# Building source distribution # # Building source distribution #
################################ ################################
...@@ -339,7 +360,7 @@ EACSL_MANUAL_FILES = doc/manuals/*.pdf ...@@ -339,7 +360,7 @@ EACSL_MANUAL_FILES = doc/manuals/*.pdf
EACSL_DOC_FILES = \ EACSL_DOC_FILES = \
doc/doxygen/doxygen.cfg.in \ doc/doxygen/doxygen.cfg.in \
doc/Changelog \ doc/Changelog \
man/e-acsl-gcc.sh.1 $(EACSL_MANPAGES)
EACSL_TEST_FILES = \ EACSL_TEST_FILES = \
tests/test_config_dev.in \ tests/test_config_dev.in \
...@@ -360,23 +381,25 @@ EACSL_TEST_FILES = \ ...@@ -360,23 +381,25 @@ EACSL_TEST_FILES = \
EACSL_DISTRIB_TESTS = \ EACSL_DISTRIB_TESTS = \
$(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \ $(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
$(dir)/*.[ich] \ $(dir)/*.[ich] \
$(dir)/test_config \ $(dir)/test_config_ci \
$(dir)/oracle_ci/*.c \ $(dir)/test_config_dev \
$(dir)/oracle_ci/*.oracle \ $(dir)/oracle_ci/* \
$(dir)/oracle_dev/* \
) )
EACSL_RTL_FILES = $(EACSL_RTL_SRC) EACSL_RTL_FILES = $(EACSL_RTL_SRC)
EACSL_SCRIPT_FILES = scripts/e-acsl-gcc.sh EACSL_SCRIPT_FILES = $(EACSL_SCRIPTS)
EACSL_LICENSE_FILES = \ EACSL_LICENSE_FILES = \
license/CEA_LGPL license/SPARETIMELABS \ license/CEA_LGPL license/SPARETIMELABS \
license/headache_config.txt license/LGPLv2.1 license/headache_config.txt license/LGPLv2.1
EACSL_MISC_FILES = \ EACSL_MISC_FILES = \
configure.ac Makefile.in INSTALL README configure.ac Makefile.in README
EACSL_SHARE_FILES = share/e-acsl/*.[ch] share/e-acsl/*/*.[ch] EACSL_SHARE_FILES = \
$(addprefix share/,$(addsuffix /*.[ch],$(EACSL_C_DIRECTORIES)))
EACSL_DISTRIB_EXTERNAL =\ EACSL_DISTRIB_EXTERNAL =\
$(EACSL_DISTRIB_DYNDEP) \ $(EACSL_DISTRIB_DYNDEP) \
...@@ -412,9 +435,12 @@ wc: ...@@ -412,9 +435,12 @@ wc:
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/internals/e_acsl_rtl_io.h \
$(EACSL_PLUGIN_DIR)/share/e-acsl/internals/e_acsl_rtl_io.c
EACSL_SHARE_BARE= share/e-acsl/*.[ch] share/e-acsl/*/*.[ch] EACSL_SHARE_BARE= \
$(addprefix share/,$(addsuffix /*.[ch],$(EACSL_C_DIRECTORIES)))
EACSL_SHARE=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_SHARE_BARE)) EACSL_SHARE=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_SHARE_BARE))
EACSL_CEA_SHARE=$(filter-out $(EACSL_SPARETIMELABS), $(wildcard $(EACSL_SHARE))) EACSL_CEA_SHARE=$(filter-out $(EACSL_SPARETIMELABS), $(wildcard $(EACSL_SHARE)))
...@@ -455,20 +481,13 @@ include $(FRAMAC_SHARE)/Makefile.dynamic ...@@ -455,20 +481,13 @@ include $(FRAMAC_SHARE)/Makefile.dynamic
EACSL_INSTALL_MANUAL_FILES=$(wildcard $(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_MANUAL_FILES))) EACSL_INSTALL_MANUAL_FILES=$(wildcard $(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_MANUAL_FILES)))
EACSL_INSTALL_C_DIRECTORIES := \ EACSL_INSTALL_SCRIPTS=$(addprefix $(E_ACSL_DIR)/,$(EACSL_SCRIPTS))
e-acsl \
e-acsl/internals \ EACSL_INSTALL_MANPAGES=$(addprefix $(E_ACSL_DIR)/,$(EACSL_MANPAGES))
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
install:: install::
$(PRINT_INSTALL) E-ACSL share files $(PRINT_INSTALL) E-ACSL share files
for dir in $(EACSL_INSTALL_C_DIRECTORIES); do \ for dir in $(EACSL_C_DIRECTORIES); do \
$(MKDIR) $(FRAMAC_DATADIR)/$$dir && \ $(MKDIR) $(FRAMAC_DATADIR)/$$dir && \
$(CP) $(E_ACSL_DIR)/share/$$dir/*.[ch] $(FRAMAC_DATADIR)/$$dir ; \ $(CP) $(E_ACSL_DIR)/share/$$dir/*.[ch] $(FRAMAC_DATADIR)/$$dir ; \
done done
...@@ -484,10 +503,15 @@ endif ...@@ -484,10 +503,15 @@ endif
$(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(LIBDIR) $(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(LIBDIR)
$(PRINT_INSTALL) E-ACSL scripts $(PRINT_INSTALL) E-ACSL scripts
$(MKDIR) $(BINDIR) $(MKDIR) $(BINDIR)
$(CP) $(E_ACSL_DIR)/scripts/e-acsl-gcc.sh $(BINDIR)/ $(CP) $(EACSL_INSTALL_SCRIPTS) $(BINDIR)/
$(PRINT_INSTALL) E-ACSL man pages $(PRINT_INSTALL) E-ACSL man pages
$(MKDIR) $(MANDIR)/man1 $(MKDIR) $(MANDIR)/man1
$(CP) $(E_ACSL_DIR)/man/e-acsl-gcc.sh.1 $(MANDIR)/man1/ $(CP) $(EACSL_INSTALL_MANPAGES) $(MANDIR)/man1/
EACSL_INSTALLED_SCRIPTS=$(addprefix $(BINDIR)/,$(notdir $(EACSL_SCRIPTS)))
EACSL_INSTALLED_MANPAGES=$(addprefix $(MANDIR)/man1/,$(notdir $(EACSL_MANPAGES)))
uninstall:: uninstall::
$(PRINT_RM) E-ACSL share files $(PRINT_RM) E-ACSL share files
...@@ -497,9 +521,9 @@ uninstall:: ...@@ -497,9 +521,9 @@ uninstall::
$(PRINT_RM) E-ACSL libraries $(PRINT_RM) E-ACSL libraries
$(RM) $(LIBDIR)/libeacsl-*.a $(RM) $(LIBDIR)/libeacsl-*.a
$(PRINT_RM) E-ACSL scripts $(PRINT_RM) E-ACSL scripts
$(RM) $(BINDIR)/e-acsl-gcc.sh $(RM) $(EACSL_INSTALLED_SCRIPTS)
$(PRINT_RM) E-ACSL man pages $(PRINT_RM) E-ACSL man pages
$(RM) $(MANDIR)/man1/e-acsl-gcc.sh.1 $(RM) $(EACSL_INSTALLED_MANPAGES)
##################################### #####################################
# Regenerating the Makefile on need # # Regenerating the Makefile on need #
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment