From 4880efeae88616d0cac334dd847a080106c27552 Mon Sep 17 00:00:00 2001 From: Thibault Martin <thi.martin.pro@pm.me> Date: Mon, 13 May 2024 10:07:16 +0200 Subject: [PATCH] Update version for 29.0~beta --- Changelog | 4 ++++ VERSION | 2 +- VERSION_CODENAME | 2 +- doc/developer/changes.tex | 4 +++- doc/userman/user-changes.tex | 4 +++- opam | 4 ++-- reference-configuration.md | 2 +- src/kernel_internals/parsing/errorloc.mli | 2 +- src/kernel_internals/runtime/boot.mli | 8 ++++---- src/kernel_internals/runtime/machdep.mli | 4 ++-- src/kernel_services/ast_data/annotations.mli | 8 ++++---- src/kernel_services/ast_data/property.mli | 4 ++-- .../ast_queries/acsl_extension.mli | 4 ++-- src/kernel_services/ast_queries/ast_info.mli | 18 +++++++++--------- src/kernel_services/ast_queries/cil.mli | 8 ++++---- .../ast_queries/cil_builtins.mli | 4 ++-- .../ast_queries/logic_typing.mli | 2 +- .../cmdline_parameters/parameter_sig.ml | 8 ++++---- .../plugin_entry_points/async.mli | 4 ++-- src/kernel_services/plugin_entry_points/db.mli | 4 ++-- .../plugin_entry_points/kernel.mli | 4 ++-- src/libraries/project/state_builder.mli | 2 +- src/libraries/utils/command.mli | 2 +- src/libraries/utils/filepath.mli | 2 +- src/plugins/e-acsl/doc/Changelog | 4 ++++ src/plugins/wp/Changelog | 4 ++++ src/plugins/wp/MemAddr.mli | 2 +- tools/hdrck/frama-c-hdrck.opam | 2 +- tools/lint/frama-c-lint.opam | 2 +- 29 files changed, 70 insertions(+), 54 deletions(-) diff --git a/Changelog b/Changelog index 236f0ea7884..217c2c3d43c 100644 --- a/Changelog +++ b/Changelog @@ -18,6 +18,10 @@ Open Source Release <next-release> ############################################################################### +############################################################################### +Open Source Release 29.0 (Copper) +############################################################################### + - Kernel [2024-04-30] new warning category too-large-array, allowing to use array > SIZE_MAX by changing its status (default is error). o Dev [2024-04-22] Remove frama-c-build-scripts.sh; add a section in diff --git a/VERSION b/VERSION index 9263b4da4ad..f61b636189f 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -28.1+dev +29.0~beta diff --git a/VERSION_CODENAME b/VERSION_CODENAME index e1d1ff400e5..6ef0d73b2e6 100644 --- a/VERSION_CODENAME +++ b/VERSION_CODENAME @@ -1 +1 @@ -Nickel +Copper diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex index 3ec55d7756b..ff75abc257c 100644 --- a/doc/developer/changes.tex +++ b/doc/developer/changes.tex @@ -5,7 +5,9 @@ This chapter summarizes the major changes in this documentation between each \framac release, from newest to oldest. -\section*{Frama-C+dev} +%\section*{Frama-C+dev} + +\section*{29.0 (Copper)} \begin{itemize} \item \textbf{Logging Services}: Document new \texttt{Current\_loc} module \item There is no more \texttt{Db} module: diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex index 6d9b6206bae..29846545f20 100644 --- a/doc/userman/user-changes.tex +++ b/doc/userman/user-changes.tex @@ -3,7 +3,9 @@ This chapter summarizes the changes in this documentation between each \FramaC release. First we list changes of the last release. -\section*{Frama-C+dev} +%\section*{Frama-C+dev} + +\section*{29.0 (Copper)} \begin{itemize} \item \textbf{Normalizing the Source Code:} document the possibility of undefining builtin macros from the chosen \texttt{-machdep}. diff --git a/opam b/opam index 15be71d45c2..53586a75eff 100644 --- a/opam +++ b/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: "28.1+dev" +version: "29.0~beta" description:""" Frama-C gathers several analysis techniques in a single collaborative framework, based on analyzers (called "plug-ins") that can build upon the @@ -72,7 +72,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-28.1-Nickel.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/reference-configuration.md b/reference-configuration.md index f66b07a9bee..102f3e6c4f1 100644 --- a/reference-configuration.md +++ b/reference-configuration.md @@ -1,5 +1,5 @@ The following set of packages is known to be a working configuration for -compiling Frama-C 28.1. +compiling Frama-C 29.0. - OCaml 4.13.1 - alt-ergo.2.5.3 (for wp, optional) diff --git a/src/kernel_internals/parsing/errorloc.mli b/src/kernel_internals/parsing/errorloc.mli index 79241282cce..9fa9f99f116 100644 --- a/src/kernel_internals/parsing/errorloc.mli +++ b/src/kernel_internals/parsing/errorloc.mli @@ -75,7 +75,7 @@ val finishParsing: unit -> unit (** Call this function to finish parsing and the location will be underlined with [^] NB: if the two positions in the location refer to different files, the first position will not be considered. - @before Frama-C+dev: the function took as argument a single position and + @before 29.0-Copper: the function took as argument a single position and and an optional [start_line] (as an [int]) to indicate a different starting line. *) diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli index 24d1a18eace..bf4060ee820 100644 --- a/src/kernel_internals/runtime/boot.mli +++ b/src/kernel_internals/runtime/boot.mli @@ -22,7 +22,7 @@ (** Frama-C main interface. @since Lithium-20081201 - @before Frama-C+dev it was in a module named Db + @before 29.0-Copper it was in a module named Db @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *) module Main : sig val extend : (unit -> unit) -> unit @@ -33,7 +33,7 @@ end val play_analysis : unit -> unit (** Run all the Frama-C analyses. This function should be called only by toplevels. - @since Frama-C+dev + @since 29.0-Copper *) val boot : unit -> unit @@ -41,6 +41,6 @@ val boot : unit -> unit val set_toplevel: ((unit -> unit) -> unit) -> unit (** Changes the toplevel function to run on boot - @since Frama-C+dev - @before Frama-C+dev it was provided in a different way in Db.Toplevel + @since 29.0-Copper + @before 29.0-Copper it was provided in a different way in Db.Toplevel *) diff --git a/src/kernel_internals/runtime/machdep.mli b/src/kernel_internals/runtime/machdep.mli index 5feab787af1..d84b3bed600 100644 --- a/src/kernel_internals/runtime/machdep.mli +++ b/src/kernel_internals/runtime/machdep.mli @@ -27,7 +27,7 @@ required by [share/libc/features.h] and other system-dependent headers. @param censored_macros prevents the generation of directives for the builtin macros in [mach.custom_defs] whose names match. empty by default. - @before Frama-C+dev censored_macros did not exist + @before 29.0-Copper censored_macros did not exist *) val gen_all_defines: Format.formatter -> @@ -38,7 +38,7 @@ val gen_all_defines: (** generates a [__fc_machdep.h] file in a temp directory and returns the directory name, to be added to the search path for preprocessing stdlib. @param see {!gen_all_defines} - @before Frama-C+dev censored_macros did not exist. + @before 29.0-Copper censored_macros did not exist. *) val generate_machdep_header: ?censored_macros:Datatype.String.Set.t -> diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli index 4caa911ae3e..628d7f69049 100644 --- a/src/kernel_services/ast_data/annotations.mli +++ b/src/kernel_services/ast_data/annotations.mli @@ -228,24 +228,24 @@ val iter_behaviors: (funbehavior -> unit) -> kernel_function -> unit (** Iter on the behaviors of the given kernel function. @since Fluorine-20130401 - @before Frama-C+dev previous version was behaving as + @before 29.0-Copper previous version was behaving as {!iter_behaviors_by_emitter} *) val fold_behaviors: (funbehavior -> 'a -> 'a) -> kernel_function -> 'a -> 'a (** Fold on the behaviors of the given kernel function. - @before Frama-C+dev previous version was behaving as + @before 29.0-Copper previous version was behaving as {!fold_behaviors_by_emitter} *) val iter_behaviors_by_emitter: (Emitter.t -> funbehavior -> unit) -> kernel_function -> unit (** Iter on the behaviors, for each emitter, of the given kernel function. - @since Frama-C+dev *) + @since 29.0-Copper *) val fold_behaviors_by_emitter: (Emitter.t -> funbehavior -> 'a -> 'a) -> kernel_function -> 'a -> 'a (** Fold on the behaviors, for each emitter, of the given kernel function. - @since Frama-C+dev *) + @since 29.0-Copper *) val iter_complete: (Emitter.t -> string list -> unit) -> kernel_function -> unit diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli index 07094491a8e..90d5044211b 100644 --- a/src/kernel_services/ast_data/property.mli +++ b/src/kernel_services/ast_data/property.mli @@ -508,14 +508,14 @@ val get_kf: identified_property -> kernel_function option val get_ir: identified_property -> identified_reachable (** For a given property, returns its corresponding [kernel_function], [kinstr] and program point. - @since Frama-C+dev *) + @since 29.0-Copper *) val get_prog_state: identified_property -> identified_reachable (** Uses [get_ir]. If [ir_kf] is [Some kf] and [ir_kinstr] is [Kglobal], we try to attach a statement depending on [ir_program_point] : the first statement of [kf] for [Before], the return statement of kf for [After]. - @since Frama-C+dev *) + @since 29.0-Copper *) val get_behavior: identified_property -> funbehavior option val get_names: identified_property -> string list diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli index a6cf1a108a6..05fc80c8931 100644 --- a/src/kernel_services/ast_queries/acsl_extension.mli +++ b/src/kernel_services/ast_queries/acsl_extension.mli @@ -53,7 +53,7 @@ type extension_printer = (** type of functions that compare two extensions (with the same keyword) to decide if they're identical or not. See {!Ast_diff} for more information. - @since Frama-C+dev + @since 29.0-Copper *) type extension_same = acsl_extension_kind -> acsl_extension_kind -> Ast_diff.is_same_env -> bool @@ -111,7 +111,7 @@ type extension_same = let () = Acsl_extension.register_behavior ~plugin:"myplugin" "FOO" foo_typer false ] - @before Frama-C+dev parameters [plugin] and [is_same_ext] were not present + @before 29.0-Copper parameters [plugin] and [is_same_ext] were not present @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *) type register_extension = diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli index a3811c43f93..fa7bdf4f855 100644 --- a/src/kernel_services/ast_queries/ast_info.mli +++ b/src/kernel_services/ast_queries/ast_info.mli @@ -232,7 +232,7 @@ module Function: sig val get_id: cil_function -> int val get_statics: fundec -> varinfo list - (** @since Frama-C+dev *) + (** @since 29.0-Copper *) end @@ -242,43 +242,43 @@ end val start_with_frama_c: string -> bool (** @return true if the given string starts with ["Frama_C_"]. - @since Frama-C+dev + @since 29.0-Copper *) val is_show_each_builtin: string -> bool (** @return true if the given string starts with ["Frama_C_show_each"]. - @since Frama-C+dev + @since 29.0-Copper *) val is_domain_show_each_builtin: string -> bool (** @return true if the given string starts with ["Frama_C_domain_show_each"]. - @since Frama-C+dev + @since 29.0-Copper *) val is_dump_each_builtin: string -> bool (** @return true if the given string starts with ["Frama_C_dump_each"]. - @since Frama-C+dev + @since 29.0-Copper *) val is_dump_file_builtin: string -> bool (** @return true if the given string starts with ["Frama_C_dump_each_file"]. - @since Frama-C+dev + @since 29.0-Copper *) val is_split_builtin: string -> bool (** @return true if the given string starts with ["Frama_C_builtin_split"]. - @since Frama-C+dev + @since 29.0-Copper *) val start_with_frama_c_builtin: string -> bool (** @return true if the given string starts with ["Frama_C_"]. - @since Frama-C+dev + @since 29.0-Copper *) val is_frama_c_builtin: varinfo -> bool (** @return true if {!start_with_frama_c_builtin} or {!Cil_builtins.has_fc_builtin_attr} are true. - @before Frama-C+dev Behave like {!start_with_frama_c_builtin}. + @before 29.0-Copper Behave like {!start_with_frama_c_builtin}. *) (* diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index 480b1edd994..2e07fd68287 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -730,7 +730,7 @@ val combineAttributes : combineWhat -> attribute list -> attributes -> attribute recursive definition. @since 28.0-Nickel - @before Frama-C+dev [strictReturnTypes] was not named and [strictInteger] + @before 29.0-Copper [strictReturnTypes] was not named and [strictInteger] not present in {!typ_combine}. *) type combineFunction = @@ -770,7 +770,7 @@ type combineFunction = @raise Cannot_combine with an explanation when the type cannot be combined. @since 28.0-Nickel - @before Frama-C+dev [strictInteger (true)] and [strictReturnTypes (false)] + @before 29.0-Copper [strictInteger (true)] and [strictReturnTypes (false)] were optional *) val combineTypesGen : ?emitwith:(Log.event -> unit) -> combineFunction -> @@ -781,7 +781,7 @@ val combineTypesGen : ?emitwith:(Log.event -> unit) -> combineFunction -> global symbols are equal, then they are the same object. @since 28.0-Nickel - @before Frama-C+dev [strictInteger (true)] was not present and left with its + @before 29.0-Copper [strictInteger (true)] was not present and left with its default value in combineTypesGen. *) val combineTypes : ?strictInteger:bool -> ?strictReturnTypes:bool -> @@ -1080,7 +1080,7 @@ val constFoldToInt: ?machdep:bool -> exp -> Integer.t option val constFoldTermNodeAtTop: term_node -> term_node (** Do constant folding on an term. - @before Frama-C+Dev takes a boolean [machdep] to decide if we actually do + @before 29.0-Copper takes a boolean [machdep] to decide if we actually do the fold or not. *) val constFoldTerm: term -> term diff --git a/src/kernel_services/ast_queries/cil_builtins.mli b/src/kernel_services/ast_queries/cil_builtins.mli index f822966b9ca..ca5ff1cbd91 100644 --- a/src/kernel_services/ast_queries/cil_builtins.mli +++ b/src/kernel_services/ast_queries/cil_builtins.mli @@ -59,12 +59,12 @@ module Frama_c_builtins: val is_builtin: varinfo -> bool (** @return true if {!has_fc_builtin_attr} or {!is_special_builtin} are true. - @before Frama-C+dev Only check for {!has_fc_builtin_attr}. + @before 29.0-Copper Only check for {!has_fc_builtin_attr}. @since Fluorine-20130401 *) val has_fc_builtin_attr: varinfo -> bool (** @return true if the given variable has a FC_BUILTIN attribute - @since Frama-C+dev *) + @since 29.0-Copper *) val is_unused_builtin: varinfo -> bool (** @return true if the given variable refers to a Frama-C builtin that diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli index f3bf52da936..b1b29a889bf 100644 --- a/src/kernel_services/ast_queries/logic_typing.mli +++ b/src/kernel_services/ast_queries/logic_typing.mli @@ -281,7 +281,7 @@ val append_pre_label: Lenv.t -> Lenv.t val append_init_label: Lenv.t -> Lenv.t (** returns the builtin label corresponding to the given name if it exists - @since Frama-C+dev + @since 29.0-Copper *) val builtin_label: string -> logic_builtin_label option diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.ml b/src/kernel_services/cmdline_parameters/parameter_sig.ml index dac383c76dd..c07ef6b5afc 100644 --- a/src/kernel_services/cmdline_parameters/parameter_sig.ml +++ b/src/kernel_services/cmdline_parameters/parameter_sig.ml @@ -286,12 +286,12 @@ module type Custom = sig val set_possible_values: string list -> unit (** Set what are the acceptable values for this parameter. If the given list is empty, then all values are acceptable. - @since Frama-C+dev *) + @since 29.0-Copper *) val get_possible_values: unit -> string list (** What are the acceptable values for this parameter. If the returned list is empty, then all values are acceptable. - @since Frama-C+dev *) + @since 29.0-Copper *) end (* ************************************************************************** *) @@ -574,7 +574,7 @@ module type Builder = sig end): Filepath (** Allow using custom types as parameters. - @since Frama-c+dev *) + @since 29.0-Copper *) module Custom(X: sig include Input_with_arg include Datatype.S @@ -586,7 +586,7 @@ module type Builder = sig (** A fixed set of possible values, represented by a type [t], intended to be a variant with only a finite number of possible constructions. Note that [t] must be comparable using [Stdlib.compare]. - @since Frama-c+dev *) + @since 29.0-Copper *) module Enum(X : sig include Input_with_arg type t diff --git a/src/kernel_services/plugin_entry_points/async.mli b/src/kernel_services/plugin_entry_points/async.mli index ee698d82393..1daeb95b11d 100644 --- a/src/kernel_services/plugin_entry_points/async.mli +++ b/src/kernel_services/plugin_entry_points/async.mli @@ -21,8 +21,8 @@ (**************************************************************************) (** Module dedicated to asynchronous actions. - @since Frama-C+dev - @before Frama-C+dev these features were in a module named Db + @since 29.0-Copper + @before 29.0-Copper these features were in a module named Db *) (** Registered daemon on progress. *) diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index aaef6216cc5..93558db217c 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -22,10 +22,10 @@ (** DEPRECATED Frama-C main interface. @since Lithium-20081201 - @deprecated Frama-C+dev Use module {!Boot.Main} *) + @deprecated 29.0-Copper Use module {!Boot.Main} *) module Main: sig val extend : (unit -> unit) -> unit [@@ deprecated "Use module Boot.Main"] (** Register a function to be called by the Frama-C main entry point. - @deprecated Frama-C+dev Use module {!Boot.Main} *) + @deprecated 29.0-Copper Use module {!Boot.Main} *) end diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli index 20f4c1bf06c..8d4f1b47e79 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -145,12 +145,12 @@ val wkey_annot_error: warn_category val wkey_plugin_not_loaded: warn_category (** Warning related to not loaded plugins. - @since Frama-C+dev + @since 29.0-Copper *) val wkey_extension_unknown: warn_category (** Warning related to the use of an unregistered ACSL extension. - @since Frama-C+dev + @since 29.0-Copper *) val wkey_ghost_already_ghost: warn_category diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli index c17049d1c6d..af34bfc8c80 100644 --- a/src/libraries/project/state_builder.mli +++ b/src/libraries/project/state_builder.mli @@ -508,7 +508,7 @@ module type Counter = sig @since Fluorine-20130401 *) (** Resets the counter to 0. - @since Frama-C+dev *) + @since 29.0-Copper *) val reset: unit -> unit val self: State.t diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli index a1e1b42cc33..7a6a5b2579b 100644 --- a/src/libraries/utils/command.mli +++ b/src/libraries/utils/command.mli @@ -126,7 +126,7 @@ val command : process will be filled into the arguments buffer. @raise Sys_error when a system error occurs @raise Async.Cancel when the computation is interrupted or on timeout - @before Frama-C+dev Async.Cancel was Db.Cancel + @before 29.0-Copper Async.Cancel was Db.Cancel *) (* diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli index 8346ae9428f..e41e6940082 100644 --- a/src/libraries/utils/filepath.mli +++ b/src/libraries/utils/filepath.mli @@ -78,7 +78,7 @@ module Normalized: sig [file] ^ [ext]. Note that it does not introduce a dot. The resulting path must respect [existence]. - @since Frama-C+dev + @since 29.0-Copper *) val extend: ?existence:existence -> t -> string -> t diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index 55e3f3ec2a1..895cf0760cb 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 29.0 (Copper) +############################################################################### + -! E-ACSL [2024-04-04] remove option -e-acsl-version. ############################################################################### diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog index 98675f9071e..9cfe4a3364f 100644 --- a/src/plugins/wp/Changelog +++ b/src/plugins/wp/Changelog @@ -24,6 +24,10 @@ Plugin WP <next-release> ############################################################################### +############################################################################### +Plugin WP 29.0 (Copper) +############################################################################### + - WP [2024-03-26] wp_nullable_args is renamed \wp::nullable_args to follow kernel changes - WP [2024-01-24] Introduce counter examples via the new option diff --git a/src/plugins/wp/MemAddr.mli b/src/plugins/wp/MemAddr.mli index acc5bfc810b..1b97aa43803 100644 --- a/src/plugins/wp/MemAddr.mli +++ b/src/plugins/wp/MemAddr.mli @@ -26,7 +26,7 @@ open Lang.F symbols. Types indicates in the documentation are Why3 types, not OCaml types. - @since Frama-C+dev + @since 29.0-Copper *) val t_addr : Lang.tau diff --git a/tools/hdrck/frama-c-hdrck.opam b/tools/hdrck/frama-c-hdrck.opam index 019afc381da..eb943254177 100644 --- a/tools/hdrck/frama-c-hdrck.opam +++ b/tools/hdrck/frama-c-hdrck.opam @@ -1,7 +1,7 @@ opam-version: "2.0" name: "frama-c-hdrck" synopsis: "Frama-C header check tool" -version: "28.1" +version: "29.0" description:""" Performs all checks related to file headers as required by the Frama-C continuous integration. diff --git a/tools/lint/frama-c-lint.opam b/tools/lint/frama-c-lint.opam index cd26b633ec0..ca8f52c3bfe 100644 --- a/tools/lint/frama-c-lint.opam +++ b/tools/lint/frama-c-lint.opam @@ -1,7 +1,7 @@ opam-version: "2.0" name: "frama-c-lint" synopsis: "Frama-C lint tool" -version: "28.1" +version: "29.0" description:""" Performs all checks related to source code formatting as required by the Frama-C continuous integration. Namely: OCP-indent for ML files, clang-format for E-ACSL -- GitLab