diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b1651d00cc8fe14f0bf160afbf0af72925f0eb51..07408029b7f8fc528172c00f9e3554d73ae1771c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -504,7 +504,7 @@ ocaml-versions-nightly:
image: 'ocaml/opam:ubuntu-20.04-ocaml-$OCAML'
script:
- sudo apt update
- - opam pin . -n
+ - opam pin . -n -k path
- opam depext frama-c --with-test
- opam install --jobs 2 frama-c --with-test --with-doc
- frama-c --plugins
diff --git a/ACKNOWLEDGEMENTS.md b/ACKNOWLEDGEMENTS.md
new file mode 100644
index 0000000000000000000000000000000000000000..5330533764638ae9061ad5edb167490a6ba8f53e
--- /dev/null
+++ b/ACKNOWLEDGEMENTS.md
@@ -0,0 +1,35 @@
+# Acknowledgements
+
+The development of Frama-C has been fuelled by many collaborative projects,
+notably at French and European level. Below is a list of the most important
+ones
+
+## European projects
+
+- [SecOPERA](https://www.secopera.eu) (2023-2025)
+- [Medsecurance](https://www.medsecurance.org/) (2023-2025)
+- [EnsureSec](https://www.ensuresec.eu/index.html) (2020-2022)
+- [Sparta](https://www.sparta.eu/) (2019-2022)
+- [Decoder](https://www.decoder-project.eu) (2019-2022)
+- [Vessedia](https://cordis.europa.eu/project/id/731453) (2017-2020)
+- [Stance](https://cordis.europa.eu/project/id/317753) (2012-2016)
+
+## French projects
+
+### ANR
+
+- [OptiTrust](https://anr.fr/Projet-ANR-22-CE25-0017) (2022-2026)
+- [CoMeMov](https://anr.fr/Project-ANR-22-CE25-0018) (2022-2025)
+- [U3CAT](https://www.frama-c.com/u3cat/) (2009-2012)
+- [Device-Soft](https://anr.fr/Project-ANR-09-CARN-0006) (2009-2011)
+- [CAT](https://anr.fr/Projet-ANR-05-RNTL-0003) (2006-2009)
+
+### PEPR
+
+- [SecurEval](https://www.pepr-secureval.com/) (2022-2027)
+
+### Others
+
+- [LEIA](https://list.cea.fr/fr/21-septembre-2021-leia-automatise-lanalyse-logicielle-pour-garantir-la-securite-des-objets-connectes/) (2021-2022)
+- [INGOPCS](https://www.s2opc.com/ingopcs/) (2016-2018)
+- [Hi-Lite](https://www.open-do.org/projects/hi-lite/index.html) (2010-2013)
diff --git a/ALL_VERSIONS b/ALL_VERSIONS
index 1b2b1d941b716157fdd8030ab63f26fe823d0e5d..b1b8812d34378cbf5905a0aadc8c1ed3459cedfe 100644
--- a/ALL_VERSIONS
+++ b/ALL_VERSIONS
@@ -1,5 +1,6 @@
Version number Date of release Notes
============== =============== =====
+29.0 (Copper) 2024, June 6
28.1 (Nickel) 2024, March 24 Bugs fixed
28.0 (Nickel) 2023, November 29
27.1 (Cobalt) 2023, July 18
diff --git a/Changelog b/Changelog
index 217c2c3d43c25c5dd0a168ef1eb34ebf095d42e7..b35148dd49c1d72bf82366c745ec2459f9d32dda 100644
--- a/Changelog
+++ b/Changelog
@@ -22,16 +22,28 @@ Open Source Release <next-release>
Open Source Release 29.0 (Copper)
###############################################################################
+- Ivette [2024-05-03] Fix performance issues on large codebases.
- Kernel [2024-04-30] new warning category too-large-array, allowing to
use array > SIZE_MAX by changing its status (default is error).
+- Eva [2024-04-26] Improve builtins memcpy, memmove and memset when
+ arguments are imprecise.
o Dev [2024-04-22] Remove frama-c-build-scripts.sh; add a section in
the user manual about how to manually replace it.
-! Kernel [2024-04-19] Change format of custom_defs field in machdep schema
and allow #undefining builtin macros in the command-line.
+- Eva [2024-04-18] Remove support for deprecated WIDEN_HINTS loop pragma.
+ Use ACSL extension "widen_hints" instead.
o Kernel [2024-04-17] Remove deprecated funcs Extlib.string_{pre,suf}fix
- Alias [2024-04-16] Fix analysis results in the presence of structures.
Complete rework of the API. Improved documentation. Fix stack
overflow in case of a cyclic graph.
+- Eva [2024-04-10] Reduce pointer values according to ACSL predicate
+ \base_addr.
+-* Eva [2024-04-10] Fix a crash when running successive analyses using
+ the -eva-domains-function parameter.
+- Ivette [2024-04-09] New notifications at the bottom-right of the main
+ window. Some components are highlighted in the bottom bar when
+ they are updated but are not currently visible.
- Kernel [2024-04-04] Avoid ambiguous pretty-printing when C labels match
the name of an ACSL built-in label (fix #@1359)
-! Kernel [2024-04-02] Systematically abort when a function is redeclared
@@ -41,13 +53,31 @@ o Kernel [2024-04-17] Remove deprecated funcs Extlib.string_{pre,suf}fix
o Kernel [2024-04-02] Annotations.{fold,iter}_behaviors now pass full
behaviors to the iterated function. To iter on fragments split by
behavior and emitter, use {fold,iter}_behaviors_by_emitter.
+- Eva [2024-03-29] Reduce pointer values according to ACSL predicate
+ valid_string and valid_read_string.
o! Kernel [2024-03-29] Refactor current location handling mechanism
+o Ivette [2024-03-29] Upgrade to node 20 and electron 28. Use vite instead
+ of webpack. Upgrade many dependencies.
+- Ivette [2024-03-28] In the Eva values table, show values before/after
+ statements with annotation, as values can be reduced after them.
+- Ivette [2024-03-26] Add feedback when the user requests the evaluation
+ of a custom term.
- Kernel [2024-03-26] Introduce \plugin:: prefix for ACSL extensions,
unknown extensions can be safely ignored when the plug-in that
handles them is not available
+- Ivette [2024-03-20] Add shortcut to select next/previous tab.
+- Ivette [2024-03-14] Complete redesign of the main view. Components and
+ views can be selected in the left sidebar (the right sidebar has
+ been removed). The top bar contains tabs of the currently selected
+ views. Components can be docked in the bottom bar, to be shown or
+ hidden on a simple click.
-* Variadic [2024-03-07] Make sure that generated functions have fresh names
o! Kernel [2024-03-07] More coherent naming of functions determining if a
symbol is a Frama-C built-in.
+- Eva [2024-03-04] Better reporting of imprecise "garbled mix" values
+ (resulting from imprecise or unsupported operations on addresses)
+ through more relevant messages and a compact summary at the end of
+ the analysis, enabled by default.
-* Kernel [2024-03-04] Accept conditional expr whose 2d and 3d operands
have type void, as per C11 6.5.15§3
-* Kernel [2024-02-22] When an array is declared with a fixed length l,
@@ -57,6 +87,8 @@ o! Kernel [2024-01-29] Db is now mostly empty, the only remaining value is
Db.Main.extend which is deprecated and replaced by
Boot.Main.extend. Features related to asynchronous interactions
are now handled in module Async
+- Ivette [2023-11-24] Global variables and types are listed in the sidebar.
+ Global variables can be filtered according to some criteria.
###############################################################################
Open Source Release 28.1 (Nickel)
diff --git a/doc/eva/examples/merge.c b/doc/eva/examples/merge.c
index dbc936c0106f585d7be057c220175149277362d2..838b22d29bfc57cb8caac47c92652fb972db4f68 100644
--- a/doc/eva/examples/merge.c
+++ b/doc/eva/examples/merge.c
@@ -1,5 +1,5 @@
int x,y;
-char t[8];
+char t[10];
int main(int c)
{
diff --git a/doc/eva/examples/misa_write.c b/doc/eva/examples/misa_write.c
new file mode 100644
index 0000000000000000000000000000000000000000..42680662405636ebdc3bed11cee23100db34f4f6
--- /dev/null
+++ b/doc/eva/examples/misa_write.c
@@ -0,0 +1,7 @@
+int x;
+int *t[2];
+
+int main(int i){
+ int **ptr = (int **) ((unsigned long) t + i);
+ *ptr = &x;
+}
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index 76628e4e00deb03c73726dddb65a3185d6edb710..13521e3d5c25894cc60705fc550480620d063806 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -1337,8 +1337,20 @@ some of these approximations.
Most origins are of the form \lstinline|Cause L|, where \lstinline|L|
is an (optional) line or the application indicating where the approximation
took place. Origin causes are one of the following:
+
+\subsubsection{Arithmetic operation}
+The origin \lstinline$Arithmetic L$ denotes arithmetic operations over
+addresses, whose result cannot be precisely represented by the analyzer.
+\csource{examples/ari.c}
+In this example, the return value for \lstinline|f| is:
+
+\begin{logs}
+{{ garbled mix of &{x; y} (origin: Arithmetic {ari.c:4}) }}
+\end{logs}
+
\subsubsection{Misaligned read}
-The origin \lstinline$Misaligned L$ indicates that
+
+The origin \lstinline$Misaligned read L$ indicates that
misaligned reads prevented the computation to be precise.
A misaligned read is a memory read-access where the bits read were not
previously written as a single write that modified the whole set of
@@ -1347,7 +1359,7 @@ bits exactly.
An example of a program leading to a misaligned read is the following:
\csource{examples/misa.c}
The value returned by the function \lstinline|main| is\\
-\lstinline|{{ garbled mix of &{ x; y } (origin: Misaligned { misa.c:6 }) }}|.\\
+\lstinline|{{ garbled mix of &{x; y} (origin: Misaligned read {misa.c:6}) }}|.\\
The analyzer is by default configured for a 64-bit architecture,
and that consequently the read memory access is not an out-of-bound access.
If it was, an alarm would be emitted, and the
@@ -1359,6 +1371,21 @@ but due to the offset of six bytes,
the 32-bit word read is made of the last two bytes from \lstinline|t[0]|
and the first two bytes from \lstinline|t[1]|.
+\subsubsection{Misaligned writes}
+
+The origin \lstinline$Misaligned write L$ indicates that the interpretation of
+a misaligned write to an imprecise location has created a garbled mix at this
+memory location.
+
+An example of a program where a misaligned write creates a garbled mix
+is the following:
+\csource{examples/misa_write.c}
+
+The interpretation of the last assignment by the analysis writes
+the imprecise value
+\lstinline|{{ garbled mix of &{x} (origin: Misaligned write {misa.c:6}) }}|
+into the array \lstinline|t|.
+
\subsubsection{Call to an unknown function}
The origin \lstinline$Library function L$ arises from the interpretation
of a function specification, when an \lstinline|assigns| clause applies to
@@ -1402,18 +1429,6 @@ called well values.
Computations that are imprecise because of a well value are marked
as \lstinline|origin: Well|.
-\subsubsection{Arithmetic operation}
-The origin \lstinline$Arithmetic L$
-indicates that arithmetic operations
-take place without the analyzer being able to represent the result
-precisely.
-\csource{examples/ari.c}
-In this example, the return value for \lstinline|f| is:
-
-\begin{logs}
-{{ garbled mix of &{ x; y } (origin: Arithmetic { ari.c:4 }) }}
-\end{logs}
-
\section{What is checked by \Eva{}}\label{obligations}
\Eva{} warns about possible run-time errors in the analyzed
diff --git a/opam b/opam
index b6ccdc6d1f41725cce55e759abefaea57791c9a7..41a6d62294c5f4f4477826a838817b71ad41c7dd 100644
--- a/opam
+++ b/opam
@@ -75,7 +75,7 @@ authors: [
homepage: "https://frama-c.com/"
license: "LGPL-2.1-only"
dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
-doc: "http://frama-c.com/download/user-manual-29.0-beta-Copper.pdf"
+doc: "http://frama-c.com/download/user-manual-29.0-Copper.pdf"
bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
tags: [
"deductive"
diff --git a/releases/29.0.md b/releases/29.0.md
index d408385573df3b1bc4fa48a5582ba137c330f122..5207c9a8e39a34c997d7ebc8a360a172a6a6f21d 100644
--- a/releases/29.0.md
+++ b/releases/29.0.md
@@ -23,7 +23,8 @@
- Extended support for Ivette
# Ivette
-- Revamped workspace (tabs, views, dock, alerts, …)
+- Revamped workspace (tabs, views, dock, alerts, notifications, …)
- Types and Globals navigation
- Better feedback on Eva values evaluation
- Extended support for WP
+- Improve performances