Commits (131)
......@@ -52,6 +52,7 @@ autom4te.cache
/tests/crowbar/mutable
/tests/crowbar/output-*
/tests/crowbar/test_ghost_cfg
/tests/fc_script/compile_commands.json
/tests/journal/intra.byte
/tests/misc/my_visitor_plugin/my_visitor.opt
/tests/misc/my_visitor.sav
......@@ -201,8 +202,8 @@ Makefile.plugin.generated
/src/kernel_internals/parsing/cparser.ml
/src/kernel_internals/parsing/cparser.mli
/src/libraries/stdlib/transitioning.ml
/src/plugins/gui/dgraph.ml
/src/plugins/gui/dgraph.mli
/src/plugins/callgraph/cg_viewer.ml
/src/plugins/gui/debug_manager.ml
/src/plugins/gui/dgraph_helper.ml
/src/plugins/gui/GSourceView.ml
/src/plugins/gui/GSourceView.mli
......
......@@ -228,3 +228,15 @@ make_public:
- nix
only:
- schedules
make_public_meta:
stage: make_public
script:
- echo "$FRAMA_C_PUBLIC_SSH_PRIVATE_KEY" | nix run -f channel:nixos-19.03 coreutils --command base64 -d > nix/frama-c-public/id_ed25519
- nix run -f channel:nixos-19.03 coreutils --command chmod 400 nix/frama-c-public/id_ed25519
- GIT_SSH=$PWD/nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git clone git@git.frama-c.com:frama-c/meta.git nix/frama-c-public/meta
- GIT_SSH=$PWD/nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git -C nix/frama-c-public/meta push git@git.frama-c.com:pub/meta origin/master:refs/heads/master
tags:
- nix
only:
- schedules
......@@ -17,6 +17,15 @@
Open Source Release <next-release>
##################################
- Metrics [2020-10-27] Add json output in addition to text and html
###################################
Open Source Release 22.0 (Titanium)
###################################
- MdR [2020-10-19] Update Sarif output to 2.1.0 + prettier URI
- Dev [2020-10-20] Support for OCamlGraph 2.0.0
- ACSL [2020-10-16] Allows for axiomatic blocks-like extensions
- Variadic [2020-10-14] Don't print generated function name but print
original name and a comment with the generated name so that the
printed code is compilable.
......@@ -24,7 +33,7 @@ Open Source Release <next-release>
transition, and use such variables in subsequent guards.
- Kernel [2020-10-09] Add option -print-config-json, to output Frama-C
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
and functions with neither definition nor specification.
-* Eva [2020-09-28] Improved string builtins on wide strings: crash fixed,
......@@ -45,6 +54,7 @@ Open Source Release <next-release>
option) on loops with several exit conditions, conditions using
equality operators, temporary variables introduced by the Frama-C
normalization or goto statements.
-! Kernel [2020-07-21] OCaml version greater than or equal to 4.08.1 required.
- Eva [2020-05-29] New builtins for trigonometric functions acos, asin
and atan (and their single-precision version acosf, asinf, atanf).
- Kernel [2020-05-28] Support for C11's _Thread_local storage specifier
......
......@@ -7,7 +7,7 @@
- [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 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)
- [Compiling from source](#compiling-from-source)
- [Quick Start](#quick-start)
......@@ -92,7 +92,7 @@ why3 config --detect
### Reference configuration
See file [reference-configuration.md](reference-configuration.md)
for a set of packages that is known to work with Frama-C 21 (Scandium).
for a set of packages that is known to work with Frama-C 22 (Titanium).
### Installing Custom Versions of Frama-C
......@@ -129,7 +129,7 @@ following tools:
#### Prerequisites: WSL + a Linux distribution
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,
but the instructions below may require some modifications).
......@@ -158,7 +158,7 @@ Move to your user directory, download the distribution and install it:
```
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
```
......@@ -171,16 +171,15 @@ For installing opam, some packages are required. The following commands can be
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 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:
```
opam init --disable-sandboxing -c 4.05.0 --shell-setup
opam init --disable-sandboxing --shell-setup
eval $(opam env)
opam install -y depext
```
......
......@@ -413,25 +413,6 @@ clean_share_link:
clean:: clean_share_link
##############
# Ocamlgraph #
##############
# dgraph (included in ocamlgraph)
#[LC] Cf https://github.com/backtracking/ocamlgraph/pull/32
ifeq ($(HAS_GNOMECANVAS),yes)
ifneq ($(ENABLE_GUI),no)
GRAPH_GUICMO= dgraph.cmo
GRAPH_GUICMX= dgraph.cmx
GRAPH_GUIO= dgraph.o
HAS_DGRAPH=yes
else # enable_gui is no: disable dgraph
HAS_DGRAPH=no
endif
else # gnome_canvas is not yes: disable dgraph
HAS_DGRAPH=no
endif
##################
# Frama-C Kernel #
##################
......@@ -739,18 +720,6 @@ src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml
endif
GENERATED+=src/plugins/gui/gtk_compat.ml
ifeq ($(HAS_DGRAPH),yes)
DGRAPHFILES:=debug_manager
src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.yes.ml
$(CP) $< $@
$(CHMOD_RO) $@
else
DGRAPHFILES:=
src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.no.ml
$(CP) $< $@
$(CHMOD_RO) $@
endif
SINGLE_GUI_CMO:= \
wutil_once \
gtk_compat \
......@@ -813,6 +782,8 @@ PLUGIN_DIR:=src/plugins/callgraph
PLUGIN_CMO:= options journalize subgraph cg services uses register
ifeq ($(HAS_DGRAPH),yes)
PLUGIN_GUI_CMO:=cg_viewer
PLUGIN_DISTRIB_EXTERNAL:=cg_viewer.yes.ml
PLUGIN_GENERATED:=$(PLUGIN_DIR)/cg_viewer.ml
else
PLUGIN_GUI_CMO:=
PLUGIN_DISTRIB_EXTERNAL:=cg_viewer.ml
......@@ -1710,9 +1681,12 @@ ALL_ML_FILES:=$(shell find src -name '*.ml' -print -o -name '*.mli' -print -o -p
ALL_ML_FILES+=ptests/ptests.ml
ifeq ($(origin MANUAL_ML_FILES),undefined)
MANUAL_ML_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(ALL_ML_FILES))
MANUAL_ML_FILES:=$(ALL_ML_FILES)
endif
MANUAL_ML_FILES:=\
$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(MANUAL_ML_FILES))
# Allow control of files to be linted/fixed by external sources
# (e.g. pre-commit hook that will concentrate on files which have changed)
......@@ -2307,6 +2281,10 @@ PLUGIN_DEP_LIST:=$(PLUGIN_LIST)
.PHONY: depend
# tell make not to remove generated files even if they are only a byproduct
# of making .depend.
.PRECIOUS: $(GENERATED) share/Makefile.dynamic_config
# in case .depend is absent, we will make it. Otherwise, it will be left
# untouched. Only make depend will force a recomputation of dependencies
.depend: $(GENERATED) share/Makefile.dynamic_config
......
......@@ -134,6 +134,30 @@ src/libraries/stdlib/transitioning.ml: \
cat $< > $@
$(CHMOD_RO) $@
ifeq ($(HAS_DGRAPH),yes)
DGRAPHFILES:=debug_manager
GENERATED+=src/plugins/gui/debug_manager.ml
ifeq ($(HAS_OCAMLGRAPH_2), yes)
DGRAPH_MODULE=Graph_gtk
DGRAPH_ERROR=Graph_gtk.DGraphMake.DotError
else
DGRAPH_MODULE=Dgraph
DGRAPH_ERROR=Dgraph.DGraphModel.DotError
endif
src/plugins/gui/debug_manager.ml \
src/plugins/gui/dgraph_helper.ml \
src/plugins/callgraph/cg_viewer.ml: %.ml: %.yes.ml Makefile.generating share/Makefile.config
$(RM) $@
$(SED) -e 's/DGRAPH_MODULE/$(DGRAPH_MODULE)/g' \
-e 's/DGRAPH_ERROR/$(DGRAPH_ERROR)/g' $< > $@
$(CHMOD_RO) $@
else
DGRAPHFILES:=
src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.no.ml Makefile.generating share/Makefile.config
$(CP) $< $@
$(CHMOD_RO) $@
endif
##################
# Frama-C-config #
##################
......
......@@ -96,7 +96,7 @@ via the GUI:
## Further reference
- 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
questions with the `frama-c` tag, which is monitored by several members of the
......@@ -110,9 +110,10 @@ via the GUI:
the [issues tracking system](https://git.frama-c.com/pub/frama-c/issues),
for reporting bugs.
- The [Frama-C wiki](https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:start)
has some useful information, although it is not entirely up-to-date.
- The [Frama-C documentation page](https://beta.frama-c.com/html/documentation.html)
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
language, undefined behavior, floating-point computations, etc.
21.1+dev
22.0+dev
\ No newline at end of file
Scandium
Titanium
\ No newline at end of file
......@@ -76,5 +76,5 @@ if [ $has_any_diffs -ne 0 ]; then
echo " opam switch create ${working_ocaml}"
echo " opam install depext"
echo " opam depext --install$all_packages"
echo " rm -f ~/.why3.conf && why3 config --full-config"
echo " rm -f ~/.why3.conf && why3 config --detect"
fi
......@@ -33,7 +33,6 @@ fi
OCAML_VERSION=$(ocamlc -version)
case $OCAML_VERSION in
4.05*|4.06*|4.07*) DYNLINK='load_printer "dynlink.cma"';;
4.08*)
echo "impossible to load dynlink in ocamldebug for version $OCAML_VERSION";
echo "pretty-printers will not be loaded";
......
......@@ -7,5 +7,5 @@ if test -z "$next"; then
echo "\$ ./bin/update_api_doc.sh <NEXT>"
echo "See the Release Management Documentation for an example."
else
find src -name '*.ml*' -exec sed -i -e "s/Frama-C+dev/${next}/g" '{}' ';'
find src -name '*.ml*' -exec sed -i -e "s/Frama-C+dev/${next}/gI" '{}' ';'
fi
......@@ -279,6 +279,10 @@ if test -z "$OCAMLGRAPH" ; then
AC_MSG_ERROR(Cannot find ocamlgraph via ocamlfind \
(requires ocamlgraph 1.8.5 or higher).)
fi
AC_SUBST(HAS_OCAMLGRAPH_2)
HAS_OCAMLGRAPH_2=no
case $OCAMLGRAPH in
0.* | 1.[[01234567]].* \
| 1.8.0 | 1.8.0+dev \
......@@ -287,10 +291,14 @@ case $OCAMLGRAPH in
| 1.8.3 | 1.8.3+dev \
| 1.8.4 | 1.8.4+dev)
AC_MSG_ERROR(found $OCAMLGRAPH: requires 1.8.5 or higher.);;
1.8.5 | 1.8.6 | 1.8.7)
1.8.5 | 1.8.6 | 1.8.7|1.8.8)
AC_MSG_RESULT(found);;
2.0.*)
HAS_OCAMLGRAPH_2=yes
AC_MSG_RESULT(found);;
*)
AC_MSG_RESULT(found $OCAMLGRAPH: should work);;
HAS_OCAMLGRAPH_2=yes
AC_MSG_RESULT(found $OCAMLGRAPH: should work, but is not tested);;
esac
# zarith
......@@ -733,7 +741,13 @@ plugin_require(from_analysis,callgraph)
check_plugin(gui,src/plugins/gui,[support for gui],yes)
plugin_require_external(gui,lablgtk)
plugin_use_external(gui,gnomecanvas)
# in ocamlgraph 2, the gtk part is separated. Hence if we found it,
# there's no need to check specifically for gnomecanvas
if test "$HAS_OCAMLGRAPH_2" = "yes"; then
plugin_use_external(gui,ocaml_ocamlgraph_gtk)
else
plugin_use_external(gui,gnomecanvas)
fi
plugin_require_external(gui,gtksourceview)
plugin_use_external(gui,dot)
......@@ -973,6 +987,10 @@ configure_library([LABLGTK],
[$LABLGTKPATH_FOR_CONFIGURE/lablgtk.$LIB_SUFFIX not found.],
no)
if test "$HAS_OCAMLGRAPH_2" = yes; then
configure_pkg([ocamlgraph_gtk],[package ocamlgraph_gtk not found])
fi
# dot and xdot tools
####################
......@@ -991,6 +1009,13 @@ new_section "checking for plug-in dependencies"
check_frama_c_dependencies
AC_SUBST(HAS_DGRAPH)
if test "$HAS_OCAMLGRAPH_2" = "yes"; then
HAS_DGRAPH=$HAS_OCAML_OCAMLGRAPH_GTK;
else
HAS_DGRAPH=$HAS_GNOMECANVAS
fi
############################
# Substitutions to perform #
############################
......
FROM debian:buster as base
# Install non-OCaml dependencies + opam
RUN apt-get update && apt-get install -y \
cvc4 \
opam \
z3 \
&& rm -rf /var/lib/apt/lists/*
RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.05.0 -y
# "RUN eval $(opam env)" does not work, so we manually set its variables
ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.05.0"
ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml"
ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/toplevel"
ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.05.0/man"
ENV PATH "/root/.opam/ocaml-base-compiler.4.05.0/bin:$PATH"
RUN opam update -y && opam install depext -y
# Install packages from reference configuration
RUN apt-get update && opam update -y && opam depext --install -y --verbose \
alt-ergo.1.30 \
apron.20160125 \
conf-graphviz.0.1 \
mlgmpidl.1.2.7 \
ocamlfind.1.8.0 \
ocamlgraph.1.8.8 \
why3.0.88.3 \
yojson.1.4.1 \
zarith.1.7 \
&& rm -rf /var/lib/apt/lists/*
RUN why3 config --detect-provers
# with_source: keep Frama-C sources
ARG with_source=no
RUN cd /root && \
wget http://frama-c.com/download/frama-c-18.0-Argon.tar.gz && \
tar xvf frama-c-*.tar.gz && \
(cd frama-c-* && \
./configure --disable-gui && \
make -j && \
make install \
) && \
rm -f frama-c-*.tar.gz && \
[ "${with_source}" != "no" ] || rm -rf frama-c-*
# with_test: run Frama-C tests; requires "with_source=yes"
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
apt-get update && \
opam update -y && opam depext --install -y \
conf-python-3.1.0.0 \
conf-time.1 \
--verbose \
&& \
rm -rf /var/lib/apt/lists/* && \
cd /root/frama-c-* && \
make tests; \
fi
FROM debian:buster as base
# Install non-OCaml dependencies + opam
RUN apt-get update && apt-get install -y \
cvc4 \
opam \
z3 \
&& rm -rf /var/lib/apt/lists/*
RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.05.0 -y
# "RUN eval $(opam env)" does not work, so we manually set its variables
ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.05.0"
ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml"
ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/toplevel"
ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.05.0/man"
ENV PATH "/root/.opam/ocaml-base-compiler.4.05.0/bin:$PATH"
RUN opam update -y && opam install depext -y
# Install packages from reference configuration
RUN apt-get update && opam update -y && opam depext --install -y --verbose \
alt-ergo-free.2.0.0 \
apron.20160125 \
conf-graphviz.0.1 \
mlgmpidl.1.2.9 \
ocamlfind.1.8.0 \
ocamlgraph.1.8.8 \
why3.1.2.0 \
yojson.1.4.1 \
zarith.1.7 \
&& rm -rf /var/lib/apt/lists/*
RUN why3 config --detect-provers
# with_source: keep Frama-C sources
ARG with_source=no
RUN cd /root && \
wget http://frama-c.com/download/frama-c-19.1-Potassium.tar.gz && \
tar xvf frama-c-*.tar.gz && \
(cd frama-c-* && \
./configure --disable-gui && \
make -j && \
make install \
) && \
rm -f frama-c-*.tar.gz && \
[ "${with_source}" != "no" ] || rm -rf frama-c-*
# with_test: run Frama-C tests; requires "with_source=yes"
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
apt-get update && \
opam update -y && opam depext --install -y \
conf-python-3.1.0.0 \
conf-time.1 \
--verbose \
&& \
rm -rf /var/lib/apt/lists/* && \
cd /root/frama-c-* && \
make tests; \
fi
FROM debian:sid as base
FROM debian:buster as base
# Install non-OCaml dependencies + opam
RUN apt-get update && apt-get install -y \
......@@ -58,7 +58,6 @@ RUN if [ "${with_test}" != "no" ]; then \
conf-time.1 \
--verbose \
&& \
apt-get install python -y && \
rm -rf /var/lib/apt/lists/* && \
cd /root/frama-c-* && \
make tests; \
......
FROM debian:sid as base
FROM debian:buster as base
# Install non-OCaml dependencies + opam
RUN apt-get update && apt-get install -y \
......
FROM debian:sid as base
FROM debian:buster as base
# Install non-OCaml dependencies + opam
RUN apt-get update && apt-get install -y \
......
......@@ -1072,8 +1072,8 @@ the sequence above is read in order and defines a configuration level
\texttt{CMD}\nscodeidx{Test!Directive}{CMD} is the last
\texttt{CMD} directive of the preceding configuration level.
\item \texttt{LOG} adds a file to be compared against an oracle in the
next \texttt{OPT} directive. Several files can be monitored from a single
\texttt{OPT} directive, through several \texttt{LOG} directives.
next \texttt{OPT} or \texttt{STDOPT} directive. Several files can be monitored from a single
\texttt{OPT}/\texttt{STDOPT} directive, through several \texttt{LOG} directives.
These files must be generated in the result
directory of the corresponding suite (and potentially alternative
configuration).
......
......@@ -29,13 +29,13 @@ clean:
%.log: SOURCE = $(word 1,$(subst ., ,$*)).c
$(TARGETS) : %.log: $$(SOURCE) $(FRAMAC) $(MAKEFILE_LIST)
$(FRAMAC) $(FCFLAGS) -val $< > $@
$(FRAMAC) $(FCFLAGS) -eva $< > $@
global-initial-values.log: FCFLAGS += -lib-entry
context-depth%.log: FCFLAGS += -lib-entry
context-depth.2.log: FCFLAGS += -context-width 1 -context-depth 1
context-depth.3.log: FCFLAGS += -context-width 1 -context-depth 1 -context-valid-pointers
slevel.1.log: FCFLAGS += -slevel 55
slevel.2.log: FCFLAGS += -slevel 28
ilevel.2.log: FCFLAGS += -val-ilevel 16
context-depth.2.log: FCFLAGS += -eva-context-width 1 -eva-context-depth 1
context-depth.3.log: FCFLAGS += -eva-context-width 1 -eva-context-depth 1 -eva-context-valid-pointers
slevel.1.log: FCFLAGS += -eva-slevel 55
slevel.2.log: FCFLAGS += -eva-slevel 28
ilevel.2.log: FCFLAGS += -eva-ilevel 16
split-fabs.log: FCFLAGS += -eva-domains equality