diff --git a/Changelog b/Changelog index 236f0ea78848684562b03480bc68947033900529..217c2c3d43c25c5dd0a168ef1eb34ebf095d42e7 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 9263b4da4adabeb62cb32baaa15964ee53c523ad..f61b636189f1a49d8fc714a3a3ff081169388207 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -28.1+dev +29.0~beta diff --git a/VERSION_CODENAME b/VERSION_CODENAME index e1d1ff400e5b54cf2be1b09eb7318092467ec5a7..6ef0d73b2e61dce4f0efb74239694c393c8113d0 100644 --- a/VERSION_CODENAME +++ b/VERSION_CODENAME @@ -1 +1 @@ -Nickel +Copper diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex index 3ec55d7756b1b2de403ed7bd430516c7916396a8..ff75abc257c07627c32d9314b764e75c4c368331 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 6d9b6206baeca6c765b323144b0c2956fe614e89..29846545f20f429b6f22f4a13973b36833ed38d0 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 15be71d45c22841d2227ce18fb765fdbaba30749..53586a75eff6edbf6c4346ed6e60ed057bad6c33 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 f66b07a9bee6e76466d0a59c2a1b82a644c18b69..102f3e6c4f18178e21f755aaa96e01bd82350602 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 79241282cce3a601fbd852435e500fcdad2fc91c..9fa9f99f1162f0dd144476421401d98a35a2e913 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 24d1a18eacecd8aaafc6e18451b67235e277397c..bf4060ee8207958c23209631234947b97ea854b1 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 5feab787af1238becf9ed949e083e53c3f8bc388..d84b3bed6003f44bb8e9583bb20bc2aea535acfa 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 4caa911ae3ed0c0f1bd4ddbf5da26255ab279864..628d7f690491c15236bfe18b28a69d7e4826c584 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 07094491a8e42d695ea3404e9dca8edcd5442798..90d5044211b9ed9383c2cc9e4f3b3b10ad8402b0 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 a6cf1a108a64e16beaff0500c60884132537ed4f..05fc80c89312da72e64f2edaedacae7a9aefd5c9 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 a3811c43f9358f19c11d5687f382ed1c4634666b..fa7bdf4f85548fc44b0480e7dd41f931cc67ddb1 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 480b1edd994acde6fb4f9f53d227d3efbb09685b..2e07fd682872d525bc099358fcd556ab91934839 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 f822966b9cac1d76be714d94e9d9d29a7ac065a6..ca5ff1cbd912c1e69493fa6e6368f0ea8a91badc 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 f3bf52da936cd899864ab42ffd1c95188be1a465..b1b29a889bfa8bbd453c4e0a271ec540911264c6 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 dac383c76dd979ee94a3c6f03504d55c8362b5fe..c07ef6b5afc0021aa92676853801dc1eacc6deb0 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 ee698d82393e2ec5cb4f433f00626aed7ef70838..1daeb95b11dc17b3e329deed14c362c26d64ee9f 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 aaef6216cc52d35a83c6ed3285ae6b0bfae9e211..93558db217ce6583e560b751fd2e724735acccae 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 20f4c1bf06c0742c567e6130e5f34f923a0f8f6c..8d4f1b47e79dd226d3e29c18508bedf45e474369 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 c17049d1c6d8bf34e267abc5e1427c05163a8301..af34bfc8c80de114a7ff139e1318ef9707e58b16 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 a1e1b42cc33d4fbd837640c5fe07bb44ee281c8b..7a6a5b2579b05678719fb83a3ffee2f57130013a 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 8346ae9428f4ff1fb52c31ddf846cbd965fc15f1..e41e6940082440037bf97db038080b74b39cdded 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 55e3f3ec2a17585ce6398cd6d1e2ad9affa43f2b..895cf0760cba2575c3cd6d44173dce9bf685f798 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 98675f9071e26568945b029c8f1ab51997678a51..9cfe4a3364f668eef96d3595e4c365b364307dfb 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 acc5bfc810bd5fc15b66126efe33a4457e253da7..1b97aa438030a65e67c78b57361bfb5cbf94dc20 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 019afc381da04856c7be0502bda0b5bdbafd86f4..eb9432541772260fb7a04b274b4599d72ad9e549 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 cd26b633ec0524104b67329f536e448bd87f661c..ca8f52c3bfec4b4d1ce8c1829059a4ef2c5053c0 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