diff --git a/src/kernel_internals/runtime/fc_config.mli b/src/kernel_internals/runtime/fc_config.mli index db77f8eac8ca6f95b920dec9ca010d0832d85ccd..6dec6669fa4bd939fa3836073518ad42d3f8f9ee 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 ffaf67de138d8e4f7eeecfd2d8c943303613460f..67020591219f1f8562acb3c23ce801520b9d58f4 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 4f6c1e6baa0813f46d12bfb8502f5d1a01b45d69..31e85b310b84657dad627038e3d8385b8ca3604c 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 1f3534a0d558942334464100e077f0ba32daf9cd..8acfd8762f44a318231b6813e2e581e6348b72d1 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 047293232cb10bb13703fc8693db5aa7189e2093..97ed08e174cd72d5739ab01ac6fdcc3cf9e44caa 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 84bc7f86f3189b98f4e940d1ed7fae540e5f37e5..05129394522bc88c3537442082d1ca52890276dc 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 16a3b015d7f20125b3a5ff540f734facc9787e90..7ff61ac8848cc0eec2a6373c9ae614b6852c1840 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 d6d44246446f891d9237de0478945762d0fe7422..5cafbeea9481051f511cf752528f75776c609bef 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 4937534d6ea3de301c5c750b460441872f34ec98..cc6a80fc4f6aee12ff1439ef90ff01ddc4dd9572 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 4c603aa208ee9b0425c3d22bbaff40702e5dfd00..585f253b8c8c8688b982e928340c77b7abf4d5d0 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