Commit 43fc965d authored by Loïc Correnson's avatar Loïc Correnson

Merge branch 'master' into feature/dome/dome-ts

parents 3697609b 0a02aefd

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.
......@@ -6,8 +6,6 @@ ML_LINT_KO+=src/kernel_internals/parsing/lexerhack.ml
ML_LINT_KO+=src/kernel_internals/parsing/logic_preprocess.mli
ML_LINT_KO+=src/kernel_internals/runtime/boot.ml
ML_LINT_KO+=src/kernel_internals/runtime/machdeps.ml
ML_LINT_KO+=src/kernel_internals/runtime/messages.ml
ML_LINT_KO+=src/kernel_internals/runtime/messages.mli
ML_LINT_KO+=src/kernel_internals/runtime/special_hooks.ml
ML_LINT_KO+=src/kernel_internals/typing/allocates.ml
ML_LINT_KO+=src/kernel_internals/typing/frontc.mli
......@@ -139,7 +137,6 @@ ML_LINT_KO+=src/libraries/utils/cilconfig.ml
ML_LINT_KO+=src/libraries/utils/command.ml
ML_LINT_KO+=src/libraries/utils/command.mli
ML_LINT_KO+=src/libraries/utils/escape.mli
ML_LINT_KO+=src/libraries/utils/filepath.ml
ML_LINT_KO+=src/libraries/utils/hook.ml
ML_LINT_KO+=src/libraries/utils/hook.mli
ML_LINT_KO+=src/libraries/utils/hptmap.ml
......@@ -169,9 +166,6 @@ ML_LINT_KO+=src/plugins/aorai/logic_simplification.ml
ML_LINT_KO+=src/plugins/aorai/logic_simplification.mli
ML_LINT_KO+=src/plugins/aorai/ltl_output.ml
ML_LINT_KO+=src/plugins/aorai/path_analysis.ml
ML_LINT_KO+=src/plugins/aorai/promelaast.mli
ML_LINT_KO+=src/plugins/aorai/promelaoutput.ml
ML_LINT_KO+=src/plugins/aorai/promelaoutput.mli
ML_LINT_KO+=src/plugins/aorai/utils_parser.ml
ML_LINT_KO+=src/plugins/callgraph/callgraph_api.mli
ML_LINT_KO+=src/plugins/callgraph/cg.ml
......@@ -325,20 +319,3 @@ ML_LINT_KO+=src/plugins/value_types/precise_locs.ml
ML_LINT_KO+=src/plugins/value_types/value_types.ml
ML_LINT_KO+=src/plugins/value_types/value_types.mli
ML_LINT_KO+=src/plugins/value_types/widen_type.ml
ML_LINT_KO+=src/plugins/variadic/classify.ml
ML_LINT_KO+=src/plugins/variadic/environment.ml
ML_LINT_KO+=src/plugins/variadic/extends.ml
ML_LINT_KO+=src/plugins/variadic/extends.mli
ML_LINT_KO+=src/plugins/variadic/format_parser.ml
ML_LINT_KO+=src/plugins/variadic/format_parser.mli
ML_LINT_KO+=src/plugins/variadic/format_pprint.ml
ML_LINT_KO+=src/plugins/variadic/format_string.ml
ML_LINT_KO+=src/plugins/variadic/format_typer.ml
ML_LINT_KO+=src/plugins/variadic/format_typer.mli
ML_LINT_KO+=src/plugins/variadic/format_types.mli
ML_LINT_KO+=src/plugins/variadic/generic.ml
ML_LINT_KO+=src/plugins/variadic/options.ml
ML_LINT_KO+=src/plugins/variadic/standard.ml
ML_LINT_KO+=src/plugins/variadic/translate.ml
ML_LINT_KO+=src/plugins/variadic/va_build.ml
ML_LINT_KO+=src/plugins/variadic/va_types.mli
......@@ -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
......@@ -98,8 +99,10 @@ autom4te.cache
/doc/aorai/frama-c-aorai-example.tgz
/doc/aorai/frama-c-aorai-example
/doc/aorai/main.pdf
/doc/aorai/ya_file.tex
/doc/aorai/basic_ya.tex
/doc/aorai/extended_ya.tex
/doc/aorai/ya_variables.tex
/doc/code/print_api/*.html
/doc/code/print_api/*.dot
......@@ -199,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
......
......@@ -57,6 +57,14 @@ wp-qualif:
- nix
allow_failure: true
aorai-prove:
stage: tests
script:
- nix/frama-ci.sh build -A frama-c.aorai-prove
tags:
- nix
allow_failure: true
genassigns:
stage: tests
script:
......@@ -220,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
......@@ -16,6 +16,33 @@
##################################
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.
- Aorai [2020-10-13] Ya automata can set auxiliary variables during a
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-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,
better performance, misaligned pointers now considered invalid.
- Kernel [2020-09-22] New option -autocomplete p1, ..., pn that list the
options of plug-ins p1, ..., pn in a format suitable for
autocompletion scripts.
- Kernel [2020-09-21] Option -permissive now allows non-existent option
names.
- Logic [2020-09-11] Introduce check-only annotations for
requires, ensures, loop invariant and lemmas
- Kernel [2020-09-08] Add option -print-cpp-commands, to print the
......@@ -27,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)
......@@ -85,14 +85,14 @@ Actually, you can use any prover supported by Why3 in combination with Frama-C/W
Most provers are available on all platforms. After their installation,
Why3 must be configured to make them available for Frama-C/WP:
```shell
why3 config --detect
```
```shell
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