diff --git a/src/kernel_internals/parsing/errorloc.mli b/src/kernel_internals/parsing/errorloc.mli index 0089c29d902db394d3eb49a57e1080a95625782e..76ceffd5a5afbf1ddd093864553bc0043a885aa0 100644 --- a/src/kernel_internals/parsing/errorloc.mli +++ b/src/kernel_internals/parsing/errorloc.mli @@ -74,7 +74,7 @@ val pp_context_from_file: ?ctx:int -> ?start_line:int -> Format.formatter -> Filepath.position -> unit (** prints a readable description of a location - @since Frama-C+dev *) + @since 22.0-Titanium *) val pp_location: Format.formatter -> Cil_types.location -> unit (** Parse errors are usually fatal, but their reporting is sometimes diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli index 60cae71fd149e6c52cdb5015d2509e6194a17bb5..1e49ae756b5729db03bcf120966a9e69e151ac27 100644 --- a/src/kernel_services/ast_data/annotations.mli +++ b/src/kernel_services/ast_data/annotations.mli @@ -69,7 +69,7 @@ val funspec: val has_funspec: kernel_function -> bool (** @return [true] iff the function has a non-empty specification. - @since Frama-C+dev *) + @since 22.0-Titanium *) val behaviors: ?emitter:Emitter.t -> ?populate:bool -> kernel_function -> funbehavior list @@ -284,7 +284,7 @@ val add_code_annot: There can be at most one loop variant registered per statement. Attempting to register a second one will result in a fatal error. - @modify Frama-C+dev: add keep_empty argument + @modify 22.0-Titanium: add keep_empty argument *) val add_assert: @@ -411,7 +411,7 @@ val add_allocates: keep_empty:bool -> allocation behavior_component_addition (** Add new allocates into the given behavior. See {!Annotations.add_assigns} for the signification of [keep_empty] - @modify Frama-C+dev add keep_empty argument + @modify 22.0-Titanium add keep_empty argument *) val add_extended: acsl_extension behavior_component_addition diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli index 9e5293c20ff883cae5aebbac55abd97051e1e499..b3f359ffbc8507182062c6876f840e6835056682 100644 --- a/src/kernel_services/ast_data/globals.mli +++ b/src/kernel_services/ast_data/globals.mli @@ -107,15 +107,15 @@ module Functions: sig val mem_name: string -> bool (** @return [true] iff there is a function with such a name - @since Frama-C+dev *) + @since 22.0-Titanium *) val mem_def_name: string -> bool (** @return [true] iff there is a function definition with such a name - @since Frama-C+dev *) + @since 22.0-Titanium *) val mem_decl_name: string -> bool (** @return [true] iff there is a function declaration with such a name - @since Frama-C+dev *) + @since 22.0-Titanium *) (** {2 Searching} *) @@ -236,7 +236,7 @@ module Types : sig val mem_enum_tag: string -> bool (** @return [true] iff there is an enum constant with the given name in the AST. - @since Frama-C+dev *) + @since 22.0-Titanium *) val find_enum_tag: string -> exp * typ (** Find an enum constant from its name in the AST. @@ -245,7 +245,7 @@ module Types : sig val mem_type: Logic_typing.type_namespace -> string -> bool (** @return [true] iff there is a type with the given name in the given namespace in the AST. - @since Frama-C+dev *) + @since 22.0-Titanium *) val find_type: Logic_typing.type_namespace -> string -> typ (** Find a type from its name in the AST. diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli index 55444e77588a2125f697a28054600bcfb826c2b8..b6cec4010d9dcd9865f1b6538bde79265a3684c0 100644 --- a/src/kernel_services/ast_printing/printer_api.mli +++ b/src/kernel_services/ast_printing/printer_api.mli @@ -453,7 +453,7 @@ module type S_pp = sig val pp_predicate_node: Format.formatter -> predicate_node -> unit val pp_predicate: Format.formatter -> predicate -> unit val pp_toplevel_predicate: Format.formatter -> toplevel_predicate -> unit - (** @since Frama-C+dev *) + (** @since 22.0-Titanium *) val pp_identified_predicate: Format.formatter -> identified_predicate -> unit val pp_code_annotation: Format.formatter -> code_annotation -> unit val pp_funspec: Format.formatter -> funspec -> unit diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index df110d9e57e479c9d9642a4aa05770c490d6b758..3bf916dcb66519cd830e6f6caaf5ab0d4d483d3f 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -548,12 +548,12 @@ val isArithmeticType: typ -> bool (** True if the argument is a scalar type (i.e. integral, enum, floating point or pointer - @since Frama-C+dev + @since 22.0-Titanium *) val isScalarType: typ -> bool (** alias of isScalarType. - @deprecated Frama-C+dev use isScalarType instead + @deprecated 22.0-Titanium use isScalarType instead *) val isArithmeticOrPointerType: typ -> bool diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli index 22b09a997e1a07f6634c988cb473e13a54338339..d088edb1cde690465549be0e21c470341b9e135f 100644 --- a/src/kernel_services/ast_queries/cil_datatype.mli +++ b/src/kernel_services/ast_queries/cil_datatype.mli @@ -73,7 +73,7 @@ module Location: sig (** Pretty-print both location start and end, including file, line and character offset. - @since Frama-C+dev + @since 22.0-Titanium *) val pretty_debug: t Pretty_utils.formatter @@ -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 22.0-Titanium *) val equal_start_semantic : location -> location -> bool diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli index 52c7f9b91f229c7bb42338e6e1ce544bb6e97993..9192bb4f790dddd6d5b6a5bf14b379616ee9b377 100644 --- a/src/kernel_services/ast_queries/file.mli +++ b/src/kernel_services/ast_queries/file.mli @@ -73,7 +73,7 @@ val list_available_machdeps: unit -> string list (** [list_available_machdeps ()] gives the list of the names of available machdeps, starting with the ones added with new_machdep and ending with the list of default machdeps. - @since Frama-C+dev *) + @since 22.0-Titanium *) type code_transformation_category (** type of registered code transformations diff --git a/src/kernel_services/ast_queries/json_compilation_database.mli b/src/kernel_services/ast_queries/json_compilation_database.mli index 5b9f18f1b087c5dc1b185eb10404de4584f0f49d..299d0ea5472228d1c37f1480c4755900bd649585 100644 --- a/src/kernel_services/ast_queries/json_compilation_database.mli +++ b/src/kernel_services/ast_queries/json_compilation_database.mli @@ -27,6 +27,6 @@ val get_flags : Datatype.Filepath.t -> string list (** [has_entry f] returns true iff [f] has an entry in the JSON compilation database. Must only be called if a JCDB file has been specified. - @since Frama-C+dev + @since 22.0-Titanium *) val has_entry : Datatype.Filepath.t -> bool diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli index 9079513585804f3b4d54d1c4052eb7b30f392675..2c2ebd716d21ef10694c88d9c0e412285ceafe91 100644 --- a/src/kernel_services/ast_queries/logic_const.mli +++ b/src/kernel_services/ast_queries/logic_const.mli @@ -51,12 +51,12 @@ val refresh_spec: funspec -> funspec to check a property, without adding it as hypothesis for the rest of the verification. See {!Cil_types.toplevel_predicate} for more information. Default is [false], i.e. use standard ACSL semantics. - @since Frama-C+dev + @since 22.0-Titanium *) val toplevel_predicate: ?only_check:bool -> predicate -> toplevel_predicate (** creates a new identified predicate with a fresh id. - @modify Frama-C+dev add [only_check] optional parameter + @modify 22.0-Titanium add [only_check] optional parameter *) val new_predicate: ?only_check:bool -> predicate -> identified_predicate diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli index b1e4074364ff4216e5558b9c7b449678405f7df5..ae2b76fdbd2762248cd4dbcb801571c71b641951 100644 --- a/src/kernel_services/ast_queries/logic_utils.mli +++ b/src/kernel_services/ast_queries/logic_utils.mli @@ -315,12 +315,12 @@ val add_attribute_glob_annot: (** {2 Contracts } *) (** [true] if the behavior has only an assigns clause. - @since Frama-C+dev + @since 22.0-Titanium *) val behavior_has_only_assigns: behavior -> bool (** [true] if the only non-empty fields of the contract are assigns clauses - @since Frama-C+dev + @since 22.0-Titanium *) val funspec_has_only_assigns: funspec -> bool diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli index d1cbe9927c71177ded1492b58c917726be657ef1..d4a26b2eec6654a73ea790ce5faebf2b0fc1abb3 100644 --- a/src/kernel_services/cmdline_parameters/cmdline.mli +++ b/src/kernel_services/cmdline_parameters/cmdline.mli @@ -319,7 +319,7 @@ val add_aliases: If [deprecated] is set to true, the use of the aliases emits a warning. @Invalid_argument if an alias name is the empty string @since Carbon-20110201 - @modify Frama-c+dev add [visible] and [deprecated] arguments. *) + @modify 22.0-Titanium add [visible] and [deprecated] arguments. *) val replace_option_setting: string -> plugin:string -> group:Group.t -> option_setting -> unit @@ -396,7 +396,7 @@ val permissive: bool unknown option names and invalid values for some options (e.g. non-existent function names). - @since Frama-C+dev *) + @since 22.0-Titanium *) val last_project_created_by_copy: (unit -> string option) ref diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.mli b/src/kernel_services/cmdline_parameters/parameter_customize.mli index 49e2f1433d6c778fb4c6d10de01a67bb6eb23032..b1360bc21d3727d51e469d5b3b4cbd09fc0aa4ee 100644 --- a/src/kernel_services/cmdline_parameters/parameter_customize.mli +++ b/src/kernel_services/cmdline_parameters/parameter_customize.mli @@ -129,7 +129,7 @@ val is_reconfigurable: unit -> unit only parameters corresponding to options registered at the {!Cmdline.Configuring} stage are reconfigurable. @since Nitrogen-20111001 - @modify Frama-C+dev [do_iterate] renamed to [is_reconfigurable] + @modify 22.0-Titanium [do_iterate] renamed to [is_reconfigurable] *) val is_not_reconfigurable: unit -> unit @@ -137,7 +137,7 @@ val is_not_reconfigurable: unit -> unit parameters corresponding to options registered at the {!Cmdline.Configuring} stage are reconfigurable. @since Nitrogen-20111001 - @modify Frama-C+dev [do_iterate] renamed to [is_reconfigurable] + @modify 22.0-Titanium [do_iterate] renamed to [is_reconfigurable] *) val no_category: unit -> unit diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli index 89a439f71b324967ac4c0775bf8eaf4587a86af8..d72b00e501427c26a9ac0839577841468a24994d 100644 --- a/src/kernel_services/cmdline_parameters/parameter_sig.mli +++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli @@ -185,7 +185,7 @@ module type S_no_parameter = sig If [visible] is set to false, the aliases do not appear in help messages. If [deprecated] is set to true, the use of the aliases emits a warning. @raise Invalid_argument if one of the strings is empty - @modify Frama-c+dev add [visible] and [deprecated] arguments. *) + @modify 22.0-Titanium add [visible] and [deprecated] arguments. *) (**/**) val is_set: unit -> bool diff --git a/src/kernel_services/plugin_entry_points/emitter.mli b/src/kernel_services/plugin_entry_points/emitter.mli index f8a43053a482103f3fb645402705e47431d997e3..c3f30a88bc5bec315f82b5d91565a199c55d66ae 100644 --- a/src/kernel_services/plugin_entry_points/emitter.mli +++ b/src/kernel_services/plugin_entry_points/emitter.mli @@ -71,7 +71,7 @@ val orphan: t emitter that is no longer available (in particular, annotations loaded from a state that was generated from a different set of plug-ins than in current session). Should not be used outside of the kernel. - @since Frama-C+dev + @since 22.0-Titanium *) (** Usable emitters are the ones which can really emit something. *) diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli index c81f3efefe7163adf572bb7ff3f34d0f35e8d635..f62ba3b05e3b0e7eaae81d3e521ffc219007cccf 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -240,7 +240,7 @@ module AutocompleteHelp: Parameter_sig.String_set module PrintConfigJson: Parameter_sig.Bool (** Behavior of option "-print-config-json" - @since Frama-C+dev *) + @since 22.0-Titanium *) (* ************************************************************************* *) (** {2 Output Messages} *) diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli index 39798e3efef3bb17f497d9ef1ff1a7da81101dd9..6cee5207ce189c7d2e2051c085226b264b121357 100644 --- a/src/kernel_services/plugin_entry_points/plugin.mli +++ b/src/kernel_services/plugin_entry_points/plugin.mli @@ -71,7 +71,7 @@ module type S_no_log = sig [add_plugin_output_aliases [alias]] adds the aliases -alias-help, -alias-verbose, etc. @since 18.0-Argon - @modify Frama-c+dev add [visible] and [deprecated] arguments. *) + @modify 22.0-Titanium add [visible] and [deprecated] arguments. *) end (** Provided plug-general services for plug-ins. @@ -90,7 +90,7 @@ type plugin = private p_help: string; p_parameters: (string, Typed_parameter.t list) Hashtbl.t } (** @since Beryllium-20090901 - @modify Frama-C+dev previously only "iterable" parameters were included, + @modify 22.0-Titanium previously only "iterable" parameters were included, now all parameters are. *) @@ -175,7 +175,7 @@ val iter_on_plugins: (plugin -> unit) -> unit val fold_on_plugins: (plugin -> 'a -> 'a) -> 'a -> 'a (** Fold [f] on each registered plug-in. - @since Frama-C+dev *) + @since 22.0-Titanium *) (**/**) (* ************************************************************************* *) diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli index 391de576362035a40b73ea78cfb7f9acabaef5fb..e6a69068fea642c0e1772714153c329931714b8f 100644 --- a/src/libraries/stdlib/extlib.mli +++ b/src/libraries/stdlib/extlib.mli @@ -323,7 +323,7 @@ val html_escape: string -> string (** [format_string_of_stag stag] returns the string corresponding to [stag], or raises an exception if the tag extension is unsupported. - @since Frama-C+dev + @since 22.0-Titanium *) val format_string_of_stag: Format.stag -> string diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli index dae52a5ab344512dfff8b234a58b08bfd63a44da..e2958f5edda2dce7e56495f8640aab70854b9657 100644 --- a/src/libraries/utils/filepath.mli +++ b/src/libraries/utils/filepath.mli @@ -92,7 +92,7 @@ val add_symbolic_dir: string -> string -> unit (** Returns the list of symbolic dirs added via [add_symbolic_dir], plus preexisting ones (e.g. FRAMAC_SHARE), as pairs (name, dir). - @since Frama-C+dev + @since 22.0-Titanium *) val all_symbolic_dirs: unit -> (string * string) list @@ -114,7 +114,7 @@ module Normalized: sig resulting from the concatenation of [dir] ^ "/" ^ [file]. The resulting path must respect [existence]. - @since Frama-C+dev + @since 22.0-Titanium *) val concat: ?existence:existence -> t -> string -> t @@ -159,7 +159,7 @@ module Normalized: sig (** [is_file f] returns [true] iff [f] points to a regular file (or a symbolic link pointing to a file). Returns [false] if any errors happen when [stat]'ing the file. - @since Frama-C+dev *) + @since 22.0-Titanium *) val is_file: t -> bool (** [to_base_uri path] returns a pair [prefix, rest], according to the @@ -171,7 +171,7 @@ module Normalized: sig E.g. for the path "FRAMAC_SHARE/libc/string.h", returns ("FRAMAC_SHARE", "libc/string.h"). - @since Frama-C+dev + @since 22.0-Titanium *) val to_base_uri: t -> string option * string end diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml index eb4ff31c0b06e02c04192daa8514bd410065baa4..53ebca7474d19a9b992487b4c3e177f3e01054d0 100644 --- a/src/plugins/qed/logic.ml +++ b/src/plugins/qed/logic.ml @@ -432,7 +432,7 @@ sig The [force] parameters defaults to [false], when it is [true], if there exist another builtin, it is replaced with the new one. Use with care. - @modify Frama-C+dev add optional [force] parameter + @modify 22.0-Titanium add optional [force] parameter *) val set_builtin' : @@ -448,7 +448,7 @@ sig The [force] parameters defaults to [false], when it is [true], if there exist another builtin, it is replaced with the new one. Use with care. - @modify Frama-C+dev add optional [force] parameter + @modify 22.0-Titanium add optional [force] parameter *) val set_builtin_get : @@ -460,7 +460,7 @@ sig The [force] parameters defaults to [false], when it is [true], if there exist another builtin, it is replaced with the new one. Use with care. - @modify Frama-C+dev add optional [force] parameter + @modify 22.0-Titanium add optional [force] parameter *) val set_builtin_eq : @@ -475,7 +475,7 @@ sig The [force] parameters defaults to [false], when it is [true], if there exist another builtin, it is replaced with the new one. Use with care. - @modify Frama-C+dev add optional [force] parameter + @modify 22.0-Titanium add optional [force] parameter *) val set_builtin_leq : @@ -491,7 +491,7 @@ sig The [force] parameters defaults to [false], when it is [true], if there exist another builtin, it is replaced with the new one. Use with care. - @modify Frama-C+dev add optional [force] parameter + @modify 22.0-Titanium add optional [force] parameter *) (** {3 Specific Patterns} *)