From e594be2048986717071af835490da95fa025b286 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 23 Oct 2020 10:24:22 +0200
Subject: [PATCH] Update API doc for 22.0-Titanium
---
src/kernel_internals/parsing/errorloc.mli | 2 +-
src/kernel_services/ast_data/annotations.mli | 6 +++---
src/kernel_services/ast_data/globals.mli | 10 +++++-----
src/kernel_services/ast_printing/printer_api.mli | 2 +-
src/kernel_services/ast_queries/cil.mli | 4 ++--
src/kernel_services/ast_queries/cil_datatype.mli | 4 ++--
src/kernel_services/ast_queries/file.mli | 2 +-
.../ast_queries/json_compilation_database.mli | 2 +-
src/kernel_services/ast_queries/logic_const.mli | 4 ++--
src/kernel_services/ast_queries/logic_utils.mli | 4 ++--
src/kernel_services/cmdline_parameters/cmdline.mli | 4 ++--
.../cmdline_parameters/parameter_customize.mli | 4 ++--
.../cmdline_parameters/parameter_sig.mli | 2 +-
src/kernel_services/plugin_entry_points/emitter.mli | 2 +-
src/kernel_services/plugin_entry_points/kernel.mli | 2 +-
src/kernel_services/plugin_entry_points/plugin.mli | 6 +++---
src/libraries/stdlib/extlib.mli | 2 +-
src/libraries/utils/filepath.mli | 8 ++++----
src/plugins/qed/logic.ml | 10 +++++-----
19 files changed, 40 insertions(+), 40 deletions(-)
diff --git a/src/kernel_internals/parsing/errorloc.mli b/src/kernel_internals/parsing/errorloc.mli
index 0089c29d902..76ceffd5a5a 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 60cae71fd14..1e49ae756b5 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 9e5293c20ff..b3f359ffbc8 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 55444e77588..b6cec4010d9 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 df110d9e57e..3bf916dcb66 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 22b09a997e1..d088edb1cde 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 52c7f9b91f2..9192bb4f790 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 5b9f18f1b08..299d0ea5472 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 90795135858..2c2ebd716d2 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 b1e4074364f..ae2b76fdbd2 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 d1cbe9927c7..d4a26b2eec6 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 49e2f1433d6..b1360bc21d3 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 89a439f71b3..d72b00e5014 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 f8a43053a48..c3f30a88bc5 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 c81f3efefe7..f62ba3b05e3 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 39798e3efef..6cee5207ce1 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 391de576362..e6a69068fea 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 dae52a5ab34..e2958f5edda 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 eb4ff31c0b0..53ebca7474d 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} *)
--
GitLab