From d67dce66d698d19e4b97a898c5de9ce94758dd79 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Fri, 28 Oct 2022 09:46:38 +0200 Subject: [PATCH] [Doc] Updates @since and @before tags to 26.0-Iron. --- src/kernel_internals/runtime/fc_config.mli | 4 ++-- src/kernel_services/ast_data/alarms.mli | 2 +- src/kernel_services/ast_data/annotations.mli | 6 +++--- src/kernel_services/ast_data/kernel_function.mli | 2 +- src/kernel_services/ast_queries/ast_info.mli | 8 ++++---- src/kernel_services/ast_queries/cil.mli | 2 +- src/kernel_services/plugin_entry_points/db.mli | 2 +- .../plugin_entry_points/dynamic.mli | 2 +- .../plugin_entry_points/kernel.mli | 2 +- src/libraries/datatype/datatype.mli | 16 ++++++++-------- 10 files changed, 23 insertions(+), 23 deletions(-) diff --git a/src/kernel_internals/runtime/fc_config.mli b/src/kernel_internals/runtime/fc_config.mli index db77f8eac8c..6dec6669fa4 100644 --- a/src/kernel_internals/runtime/fc_config.mli +++ b/src/kernel_internals/runtime/fc_config.mli @@ -64,11 +64,11 @@ val framac_libc: Filepath.Normalized.t val libdirs: Filepath.Normalized.t list (** Directories where library and executable files are, in order of priority. - @since Frama-C+dev *) + @since 26.0-Iron *) val libdir: Filepath.Normalized.t (** Last directory of libdirs (the directory of frama-c installation) - @since Frama-C+dev *) + @since 26.0-Iron *) val plugin_dir: Filepath.Normalized.t list (** Directory where the Frama-C dynamic plug-ins are. *) diff --git a/src/kernel_services/ast_data/alarms.mli b/src/kernel_services/ast_data/alarms.mli index ffaf67de138..67020591219 100644 --- a/src/kernel_services/ast_data/alarms.mli +++ b/src/kernel_services/ast_data/alarms.mli @@ -110,7 +110,7 @@ val to_seq: (Emitter.t * kernel_function * stmt * int * alarm * code_annotation) Seq.t (** Returns the sequence of all alarms and the associated annotations at some program point - @since Frama-C+dev *) + @since 26.0-Iron *) val find: code_annotation -> alarm option (** @return the alarm corresponding to the given assertion, if any. diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli index 4f6c1e6baa0..31e85b310b8 100644 --- a/src/kernel_services/ast_data/annotations.mli +++ b/src/kernel_services/ast_data/annotations.mli @@ -355,7 +355,7 @@ val add_spec: [register_children] is directly given to the function [add_behaviors]. @since 23.0-Vanadium - @before Frama-C+dev: the [force] parameter does not exist + @before 26.0-Iron: the [force] parameter does not exist *) val add_behaviors: @@ -373,7 +373,7 @@ val add_decreases: function, an exception [AlreadySpecified] is raised. If [force] is [true] the old specification is dropped and the new one replaces it. - @before Frama-C+dev: the [force] parameter does not exist + @before 26.0-Iron: the [force] parameter does not exist *) val add_terminates: @@ -384,7 +384,7 @@ val add_terminates: function, an exception [AlreadySpecified] is raised. If [force] is [true] the old specification is dropped and the new one replaces it. - @before Frama-C+dev: the [force] parameter does not exist + @before 26.0-Iron: the [force] parameter does not exist *) val add_complete: string list contract_component_addition diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli index 1f3534a0d55..8acfd8762f4 100644 --- a/src/kernel_services/ast_data/kernel_function.mli +++ b/src/kernel_services/ast_data/kernel_function.mli @@ -252,7 +252,7 @@ val has_definition : t -> bool val is_ghost : t -> bool (** @return [true] iff the given kernel function is ghost - @since Frama-C+dev *) + @since 26.0-Iron *) (* ************************************************************************* *) (** {2 Membership of variables} *) diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli index 047293232cb..97ed08e174c 100644 --- a/src/kernel_services/ast_queries/ast_info.mli +++ b/src/kernel_services/ast_queries/ast_info.mli @@ -43,7 +43,7 @@ val possible_value_of_integral_const: constant -> Integer.t option [None] if the expression is not a constant expression or does not evaluate to an integer constant. - @before Frama-C+dev the function only returned [Some v] when the + @before 26.0-Iron the function only returned [Some v] when the expression was an integer literal (i.e. [Const c]). *) val possible_value_of_integral_expr: exp -> Integer.t option @@ -59,7 +59,7 @@ val value_of_integral_const: constant -> Integer.t an integer constant expression. If unsure, use {!possible_value_of_integral_expr}. - @before Frama-C+dev the function would fail if the expression was not an + @before 26.0-Iron the function would fail if the expression was not an integer literal (see {!possible_value_of_integral_expr}). *) val value_of_integral_expr: exp -> Integer.t @@ -67,7 +67,7 @@ val value_of_integral_expr: exp -> Integer.t (** [true] iff the expression is a constant expression that evaluates to a null pointer, i.e. 0 or a cast to 0. - @before Frama-C+dev the function would return [false] as soon as the + @before 26.0-Iron the function would return [false] as soon as the expression was not an integer literal (possibly casted). *) val is_null_expr: exp -> bool @@ -78,7 +78,7 @@ val is_null_expr: exp -> bool {b Warning:} note that for the purpose of this function [&x] is {i not} a constant expression, hence the function will return [false] in this case. - @before Frama-C+dev the function would return [false] as soon as + @before 26.0-Iron the function would return [false] as soon as the expression was not an integer literal (possibly casted). *) val is_non_null_expr: exp -> bool diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index 84bc7f86f31..05129394522 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -1485,7 +1485,7 @@ val isWFGhostType : typ -> bool val typeAddGhost : typ -> typ (** Add the ghost attribute to a type (does nothing if the type is alreay ghost) @return the ghost qualified original type - @since Frama-C+dev *) + @since 26.0-Iron *) (* ************************************************************************* *) (** {2 The visitor} *) diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index 16a3b015d7f..7ff61ac8848 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -63,7 +63,7 @@ val register_compute: val register_guarded_compute: (unit -> bool) -> (unit -> unit) ref -> (unit -> unit) -> unit -(** @before Frama-C+dev there was a string parameter (first position) that was +(** @before 26.0-Iron there was a string parameter (first position) that was only used for Journalization, that has been removed. *) (** Frama-C main interface. diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli index d6d44246446..5cafbeea948 100644 --- a/src/kernel_services/plugin_entry_points/dynamic.mli +++ b/src/kernel_services/plugin_entry_points/dynamic.mli @@ -35,7 +35,7 @@ val register: [name], the type [ty] and the plug-in [plugin]. @raise Type.AlreadyExists if [name] already exists. In other words you cannot register a value with the same name twice. - @before Frama-C+dev there was a labeled argument [journalized], that has + @before 26.0-Iron there was a labeled argument [journalized], that has been removed when Journalization has been removed. @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *) diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli index 4937534d6ea..cc6a80fc4f6 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -374,7 +374,7 @@ module LoadModule: Parameter_sig.String_list module LoadLibrary: Parameter_sig.String_list (** Behavior of option "-load-library" - @since Frama-C+dev + @since 26.0-Iron *) module AutoLoadPlugins: Parameter_sig.Bool diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli index 4c603aa208e..585f253b8c8 100644 --- a/src/libraries/datatype/datatype.mli +++ b/src/libraries/datatype/datatype.mli @@ -31,7 +31,7 @@ (** Values associated to each datatype. Some others are provided directly in module {!Type}. - @before Frama-C+dev there was additional fields only used for Journalization + @before 26.0-Iron there was additional fields only used for Journalization that has been removed. *) type 'a t = private @@ -52,7 +52,7 @@ module type Ty = sig end (** All values associated to a datatype, excepted [copy]. - @before Frama-C+dev there was several additional values only used for + @before 26.0-Iron there was several additional values only used for Journalization that has been removed. *) module type S_no_copy = sig @@ -137,7 +137,7 @@ val never_any_project: (Project_skeleton.t -> bool) -> 'a -> bool (** Sub-signature of {!S}. @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide - @before Frama-C+dev there was several additional values only used for + @before 26.0-Iron there was several additional values only used for Journalization that has been removed. *) module type Undefined = sig @@ -176,7 +176,7 @@ module Serializable_undefined: Undefined Values to implement in order to get a datatype. Feel free to use easy builders (see above) for easy implementation. - @before Frama-C+dev there was several additional values only used for + @before 26.0-Iron there was several additional values only used for Journalization that has been removed. *) module type Make_input = sig @@ -363,7 +363,7 @@ end (** Functor for polymorphic types with only 1 type variable. @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide - @before Frama-C+dev the functor had several additional values only used for + @before 26.0-Iron the functor had several additional values only used for Journalization that has been removed. *) module Polymorphic @@ -390,7 +390,7 @@ end (** Functor for polymorphic types with 2 type variables. @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide - @before Frama-C+dev the functor had several additional values only used for + @before 26.0-Iron the functor had several additional values only used for Journalization that has been removed. *) module Polymorphic2 @@ -423,7 +423,7 @@ end (** Functor for polymorphic types with 3 type variables. @since Oxygen-20120901 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide - @before Frama-C+dev the functor had several additional values only used for + @before 26.0-Iron the functor had several additional values only used for Journalization that has been removed. *) module Polymorphic3 @@ -464,7 +464,7 @@ end (** Functor for polymorphic types with 4 type variables. @since Oxygen-20120901 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide - @before Frama-C+dev the functor had several additional values only used for + @before 26.0-Iron the functor had several additional values only used for Journalization that has been removed. *) module Polymorphic4 -- GitLab