From e222b1dfb029ebdfc6697b1236e37008b16eb81e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 17 May 2021 23:49:44 +0200
Subject: [PATCH] Update @since
---
opam/opam | 5 ++--
src/kernel_services/ast_data/annotations.mli | 2 +-
src/kernel_services/ast_data/cil_types.mli | 2 +-
src/kernel_services/ast_data/globals.mli | 2 +-
src/kernel_services/ast_data/property.mli | 2 +-
.../ast_data/property_status.mli | 2 +-
src/kernel_services/ast_queries/ast_info.mli | 6 ++--
src/kernel_services/ast_queries/cil.mli | 28 +++++++++----------
.../ast_queries/cil_builtins.mli | 2 +-
src/kernel_services/ast_queries/cil_const.mli | 2 +-
.../ast_queries/cil_datatype.mli | 2 +-
src/kernel_services/ast_queries/file.mli | 2 +-
src/kernel_services/ast_queries/logic_env.mli | 2 +-
.../cmdline_parameters/parameter_sig.mli | 2 +-
.../plugin_entry_points/dynamic.mli | 4 +--
.../plugin_entry_points/kernel.mli | 6 ++--
.../plugin_entry_points/log.mli | 4 +--
src/libraries/stdlib/extlib.mli | 2 +-
src/libraries/utils/filepath.mli | 16 +++++------
src/libraries/utils/json.mli | 10 +++----
src/plugins/e-acsl/doc/Changelog | 4 +++
src/plugins/gui/help_manager.ml | 1 +
src/plugins/wp/Changelog | 4 +++
23 files changed, 61 insertions(+), 51 deletions(-)
diff --git a/opam/opam b/opam/opam
index b00e5233da3..3fb14aaa567 100644
--- a/opam/opam
+++ b/opam/opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "22.0+dev"
+version: "23.0~rc1"
description:"""
Frama-C gathers several analysis techniques in a single collaborative
framework, based on analyzers (called "plug-ins") that can build upon the
@@ -54,6 +54,7 @@ authors: [
"Anne Pacalet"
"Valentin Perrelle"
"Guillaume Petiot"
+ "Dario Pinto"
"Virgile Prevosto"
"Armand Puccetti"
"Virgile Robles"
@@ -65,7 +66,7 @@ authors: [
homepage: "http://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-22.0-Titanium.pdf"
+doc: "http://frama-c.com/download/user-manual-23.0-Vanadium.pdf"
bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
tags: [
"deductive"
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index 1b7e315613e..007bd100f3c 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -339,7 +339,7 @@ val add_spec: ?register_children:bool -> spec contract_component_addition
[register_children] is directly given to the function [add_behaviors].
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val add_behaviors:
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 0c6f4675096..11e5418d283 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -349,7 +349,7 @@ and attrparam =
assigned and that the fields have the right pointers to parents.).
@plugin development guide
- @since Frama-C+dev [cfields] is an option, [None] is used for incomplete
+ @since 23.0-Vanadium [cfields] is an option, [None] is used for incomplete
types (in replacement of removed field [cdefined]) *)
and compinfo = {
mutable cstruct: bool;
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index 1a6775ec972..d5a9e9faf8d 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -129,7 +129,7 @@ module Functions: sig
name is [name], sorted according to [cmp]. If [cmp] is [None],
the resulting order is unspecified.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val find_def_by_name : string -> kernel_function
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 531f38e79aa..54202673c28 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -218,7 +218,7 @@ include Datatype.S_with_collections with type t = identified_property
3. kind of property
4. id of the property
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
module Ordered_by_function:
Datatype.S_with_collections with type t = identified_property
diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli
index aaf4f44d710..36413851400 100644
--- a/src/kernel_services/ast_data/property_status.mli
+++ b/src/kernel_services/ast_data/property_status.mli
@@ -239,7 +239,7 @@ end
val iter: (Property.t -> unit) -> unit
val fold: (Property.t -> 'a -> 'a) -> 'a -> 'a
-(** @since Frama-C+dev *)
+(** @since 23.0-Vanadium *)
val iter_sorted:
cmp:(Property.t -> Property.t -> int) -> (Property.t -> unit) -> unit
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index 2f420c05573..bd827db2797 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -69,7 +69,7 @@ val precondition : goal:bool -> funspec -> predicate
With [~goal:true], only returns assert and check predicates.
With [~goal:false], only returns assert and admit predicates.
@since Carbon-20101201
- @modify Frama-C+dev introduce [goal] flag
+ @modify 23.0-Vanadium introduce [goal] flag
*)
val behavior_assumes : funbehavior -> predicate
@@ -80,7 +80,7 @@ val behavior_precondition : goal:bool -> funbehavior -> predicate
(** Builds the precondition from [b_assumes] and [b_requires] clauses.
For flag [~goal] see {!Ast_info.precondition} above.
@since Carbon-20101201
- @modify Frama-C+dev introduce [goal] flag
+ @modify 23.0-Vanadium introduce [goal] flag
*)
val behavior_postcondition :
@@ -88,7 +88,7 @@ val behavior_postcondition :
(** Builds the postcondition from [b_assumes] and [b_post_cond] clauses.
For flag [~goal] see {Ast_info.precondition} above.
@modify Boron-20100401 added termination kind as filtering argument.
- @modify Frama-C+dev introduce [goal] flag
+ @modify 23.0-Vanadium introduce [goal] flag
*)
val disjoint_behaviors : funspec -> string list -> predicate
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 2613a70e4cf..2f3a0822bef 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -107,7 +107,7 @@ val set_acceptEmptyCompinfo: unit -> unit
Note that if the selected machdep is GCC or MSVC, this call has no effect
as these modes already allow empty compinfos.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val acceptEmptyCompinfo: unit -> bool
@@ -115,7 +115,7 @@ val acceptEmptyCompinfo: unit -> bool
{!Cil.gccMode}, and can be forced by {!Cil.set_acceptEmptyCompinfo}
otherwise.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
(* ************************************************************************* *)
@@ -325,7 +325,7 @@ val ulongLongType: typ
It is equivalent to the ISO C int16_t type but without using the
corresponding header.
Must only be called if such type exists in the current architecture.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val int16_t: unit -> typ
@@ -333,7 +333,7 @@ val int16_t: unit -> typ
It is equivalent to the ISO C int32_t type but without using the
corresponding header.
Must only be called if such type exists in the current architecture.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val int32_t: unit -> typ
@@ -341,7 +341,7 @@ val int32_t: unit -> typ
It is equivalent to the ISO C int64_t type but without using the
corresponding header.
Must only be called if such type exists in the current architecture.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val int64_t: unit -> typ
@@ -978,12 +978,12 @@ val need_cast: ?force:bool -> typ -> typ -> bool
type is the same as the old type, then no cast is added, unless [force]
is [true] (default is [false])
@modify Fluorine-20130401 add [force] argument
- @modify Frama-C+dev change order or arguments
+ @modify 23.0-Vanadium change order or arguments
*)
val mkCastT: ?force:bool -> oldt:typ -> newt:typ -> exp -> exp
(** Like {!Cil.mkCastT} but uses typeOf to get [oldt]
- @modify Frama-C+dev change order or arguments
+ @modify 23.0-Vanadium change order or arguments
*)
val mkCast: ?force:bool -> newt:typ -> exp -> exp
@@ -1121,7 +1121,7 @@ val mkPureExpr:
(** Make a loop. Can contain Break or Continue.
The kind of loop (while, for, dowhile) is given by [sattr]
(none by default). Use {!Cil.mkWhile} for a While loop.
- @modify Frama-C+dev add unit argument. Default type is no longer While,
+ @modify 23.0-Vanadium add unit argument. Default type is no longer While,
use {!Cil.mkWhile} instead.
*)
val mkLoop: ?sattr:attributes -> guard:exp -> body:stmt list -> unit ->
@@ -1131,26 +1131,26 @@ val mkLoop: ?sattr:attributes -> guard:exp -> body:stmt list -> unit ->
can contain Break but not Continue. Can be used with i a pointer
or an integer. Start and done must have the same type but incr
must be an integer
- @modify Frama-C+dev add unit argument
+ @modify 23.0-Vanadium add unit argument
*)
val mkForIncr: ?sattr:attributes -> iter:varinfo -> first:exp -> stopat:exp ->
incr:exp -> body:stmt list -> unit -> stmt list
(** Make a for loop for(start; guard; next) \{ ... \}. The body can
contain Break but not Continue !!!
- @modify Frama-C+dev add unit argument
+ @modify 23.0-Vanadium add unit argument
*)
val mkFor: ?sattr:attributes -> start:stmt list -> guard:exp -> next: stmt list ->
body: stmt list -> unit -> stmt list
(** Make a while loop.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val mkWhile: ?sattr:attributes -> guard:exp -> body:stmt list -> unit ->
stmt list
(** Make a do ... while loop.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val mkDoWhile: ?sattr:attributes -> body:stmt list -> guard:exp -> unit ->
stmt list
@@ -1441,13 +1441,13 @@ val global_attributes: global -> attributes
(**
Whether the given attributes contain libc indicators.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val is_in_libc: attributes -> bool
(**
Whether the given global contains libc indicators.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val global_is_in_libc: global -> bool
diff --git a/src/kernel_services/ast_queries/cil_builtins.mli b/src/kernel_services/ast_queries/cil_builtins.mli
index 90b7cfea4a7..3c08e8507bc 100644
--- a/src/kernel_services/ast_queries/cil_builtins.mli
+++ b/src/kernel_services/ast_queries/cil_builtins.mli
@@ -99,7 +99,7 @@ module Builtin_functions :
the machdep and initializing machine-dependent builtins. Hence, types
such {!Cil.uint16_t} might be used if needed.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val add_custom_builtin: (unit -> (string * typ * typ list * bool)) -> unit
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index 5523ae89d6f..62d0b788fa4 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -82,7 +82,7 @@ val new_raw_id: unit -> int
* structure itself), and (4) an optional list of attributes to be associated
* with the composite type, "None" means that the struct is incomplete.
*
- * @since Frama-C+dev the 4th parameter is a function that returns an option.
+ * @since 23.0-Vanadium the 4th parameter is a function that returns an option.
**)
val mkCompInfo: bool -> (* whether it is a struct or a union *)
string -> (* name of the composite type; cannot be empty *)
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index dd75d97434b..4fcde6cd57f 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -85,7 +85,7 @@ module Location: sig
starting position. Compares normalized filenames, lines and columns,
but no absolute character offsets.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val compare_start_semantic : location -> location -> int
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index 642f1f036dc..91617f17eae 100644
--- a/src/kernel_services/ast_queries/file.mli
+++ b/src/kernel_services/ast_queries/file.mli
@@ -148,7 +148,7 @@ val get_name: t -> string
val get_preprocessor_command: unit -> string
(** Return the preprocessor command to use.
- @modify Frama-C+dev return type now contains only the command
+ @modify 23.0-Vanadium return type now contains only the command
*)
val pre_register: t -> unit
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index e1d369a1c87..02c6bf141f5 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -57,7 +57,7 @@ module Model_info: State_builder.Hashtbl
module Lemmas: State_builder.Hashtbl
with type key = string and type data = Cil_types.global_annotation
-(** @since Frama-C+dev *)
+(** @since 23.0-Vanadium *)
module Axiomatics: State_builder.Hashtbl
with type key = string and type data = Cil_types.location
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index 4d16f3101e7..d4aa36860df 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -299,7 +299,7 @@ module type Filepath = sig
(**
Whether the Filepath is empty.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val is_empty: unit -> bool
end
diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli
index c21d4b2e7af..40bf6c0b4b4 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.mli
+++ b/src/kernel_services/plugin_entry_points/dynamic.mli
@@ -150,7 +150,7 @@ end
(* ************************************************************************* *)
(** loads a list of Findlib packages
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val load_packages: string list -> unit
@@ -165,7 +165,7 @@ val load_module: string -> unit
val set_module_load_path : string list -> unit
(** [is_loaded package] returns [true] iff [package] has already been loaded.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val is_loaded: string -> bool
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 27b353b4565..f4a0a632fa6 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -314,7 +314,7 @@ end
(** Behavior of option "-add-symbolic-path"
@since Neon-20140301
- @modify Frama-C+dev inversed argument order (now uses path:name) *)
+ @modify 23.0-Vanadium inversed argument order (now uses path:name) *)
module SymbolicPath: Parameter_sig.Filepath_map with type value = string
module FloatNormal: Parameter_sig.Bool
@@ -359,13 +359,13 @@ end
module Session_dir: Parameter_sig.Filepath
(** Directory in which session files are searched.
@since Neon-20140301
- @modify Frama-C+dev parameter type is now Filepath instead of string
+ @modify 23.0-Vanadium parameter type is now Filepath instead of string
*)
module Config_dir: Parameter_sig.Filepath
(** Directory in which config files are searched.
@since Neon-20140301
- @modify Frama-C+dev parameter type is now Filepath instead of string
+ @modify 23.0-Vanadium parameter type is now Filepath instead of string
*)
(* this stop special comment does not work as expected (and as explained in the
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index 0a07a3805f6..9b9677ad475 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -87,7 +87,7 @@ exception FeatureRequest of Filepath.position option * string * string
You may catch [FeatureRequest(s,p,r)] to support degenerated behavior.
The (optional) source location is s, the responsible plugin is 'p'
and the feature request is 'r'.
- @modified Frama-C+dev added source location.
+ @modified 23.0-Vanadium added source location.
*)
(* -------------------------------------------------------------------------- *)
@@ -214,7 +214,7 @@ module type Messages = sig
If the exception is not caught, Frama-C displays a feature-request
message to the user.
@since Beryllium-20090901
- @modified Frama-C+dev added current and source arguments.
+ @modified 23.0-Vanadium added current and source arguments.
*)
val deprecated: string -> now:string -> ('a -> 'b) -> ('a -> 'b)
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 07eac0f5449..66405c32536 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -211,7 +211,7 @@ val the: exn:exn -> 'a option -> 'a
@raise Invalid_argument if the value is [None] and [exn] is not specified.
@return v if the value is [Some v].
@modify Magnesium-20151001 add optional argument [exn]
- @modify Frama-C+dev optional argument [exn] now mandatory; otherwise,
+ @modify 23.0-Vanadium optional argument [exn] now mandatory; otherwise,
use [Option.get], which is equivalent.
@plugin development guide *)
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index c81c1f198bc..3040390414c 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -92,7 +92,7 @@ module Normalized: sig
(** [to_string_list l] returns [l] as a list of strings containing the
absolute paths to the elements of [l].
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val to_string_list: t list -> string list
@@ -122,28 +122,28 @@ module Normalized: sig
val pp_abs: Format.formatter -> t -> unit
(** Unknown filepath, used as 'dummy' for [Datatype.Filepath].
- @deprecated Frama-C+dev use 'empty' instead
+ @deprecated 23.0-Vanadium use 'empty' instead
*)
val unknown: t
[@@alert deprecated "Use Filepath.Normalized.empty instead"]
(** @since 20.0-Calcium
- @deprecated Frama-C+dev use 'is_empty' instead
+ @deprecated 23.0-Vanadium use 'is_empty' instead
*)
val is_unknown: t -> bool
[@@alert deprecated "Use Filepath.Normalized.is_empty instead"]
(** Empty filepath, used as 'dummy' for [Datatype.Filepath].
- @since Frama-C+dev.
+ @since 23.0-Vanadium.
*)
val empty: t
- (** @since Frama-C+dev *)
+ (** @since 23.0-Vanadium *)
val is_empty: t -> bool
(** [is_special_stdout f] returns [true] iff [f] is '-' (a single dash),
which is a special notation for 'stdout'.
- @since Frama-C+dev *)
+ @since 23.0-Vanadium *)
val is_special_stdout: t -> bool
(** [is_file f] returns [true] iff [f] points to a regular file
@@ -170,7 +170,7 @@ end
(that is, it is prefixed by [base_name]), or to the current
working directory if no base is specified.
@since Aluminium-20160501
- @modify Frama-C+dev argument types changed from string to Normalized.t
+ @modify 23.0-Vanadium argument types changed from string to Normalized.t
*)
val is_relative: ?base_name:Normalized.t -> Normalized.t -> bool
@@ -181,7 +181,7 @@ val is_relative: ?base_name:Normalized.t -> Normalized.t -> bool
val add_symbolic_dir: string -> Normalized.t -> unit
(** Remove all symbolic dirs that have been added earlier.
- @since Frama-C+dev *)
+ @since 23.0-Vanadium *)
val reset_symbolic_dirs: unit -> unit
(** Returns the list of symbolic dirs added via [add_symbolic_dir], plus
diff --git a/src/libraries/utils/json.mli b/src/libraries/utils/json.mli
index 2549b3ae076..576e24a014c 100644
--- a/src/libraries/utils/json.mli
+++ b/src/libraries/utils/json.mli
@@ -139,7 +139,7 @@ val field : string -> t -> t
Note: no other functions should modify the contents of [path]; any
modifications will be overwritten when the cache is flushed.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
(** Exception raised by the functions below when incompatible types are
@@ -160,7 +160,7 @@ exception CannotMerge of string
@raise CannotMerge if the objects have conflicting types for
the same keys, or if the root JSON element is not an object.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val merge_object : Filepath.Normalized.t -> Yojson.Basic.t -> unit
@@ -171,7 +171,7 @@ val merge_object : Filepath.Normalized.t -> Yojson.Basic.t -> unit
of elements.
@raise CannotMerge if the root JSON element is not an array.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val merge_array : Filepath.Normalized.t -> Yojson.Basic.t -> unit
@@ -179,7 +179,7 @@ val merge_array : Filepath.Normalized.t -> Yojson.Basic.t -> unit
[from_file path] opens [path] and stores its JSON object in
a memory cache, to be used by the other related functions.
@raise Yojson.Json_error if [path] is a malformed JSON file.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val from_file: Filepath.Normalized.t -> Yojson.Basic.t
@@ -187,6 +187,6 @@ val from_file: Filepath.Normalized.t -> Yojson.Basic.t
Flushes the JSON objects in the cache. Returns the names of the written
files.
- @since Frama-C+dev
+ @since 23.0-Vanadium
*)
val flush_cache : unit -> Filepath.Normalized.t list
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index f3a19a88325..d3efe23c9da 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,10 @@
Plugin E-ACSL <next-release>
############################
+#############################
+Plugin E-ACSL 23.0 (Vanadium)
+#############################
+
- E-ACSL [2021-04-09] Add support for loop variant.
- E-ACSL [2021-04-07] Add support for multiple binders in guarded
quantifications (frama-c/e-acsl#127).
diff --git a/src/plugins/gui/help_manager.ml b/src/plugins/gui/help_manager.ml
index 01d2244fd0f..5219fe6e467 100644
--- a/src/plugins/gui/help_manager.ml
+++ b/src/plugins/gui/help_manager.ml
@@ -57,6 +57,7 @@ let show main_ui =
"Anne Pacalet";
"Valentin Perrelle";
"Guillaume Petiot";
+ "Dario Pinto";
"Virgile Prevosto";
"Armand Puccetti";
"Virgile Robles";
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 3abab2c703e..08be8622a52 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,10 @@
Plugin WP <next-release>
#########################
+#########################
+Plugin WP 23.0 (Vanadium)
+#########################
+
- WP [2020-03-01] Section « Limitation & Roadmap » added to the WP manual.
- WP [2020-03-01] New internal WP engine, fixing many issues related to
control flow graph and local variable scoping.
--
GitLab