From b46fece00975c470a541ade0e8e219aae45ce872 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 14 Apr 2022 10:53:23 +0200
Subject: [PATCH] [doc] remove old @modify
---
src/kernel_internals/parsing/logic_lexer.mli | 2 +-
src/kernel_internals/runtime/fc_config.mli | 3 +-
src/kernel_internals/runtime/messages.mli | 3 +-
src/kernel_internals/typing/cabs2cil.mli | 2 -
src/kernel_internals/typing/oneret.mli | 6 +--
.../analysis/service_graph.mli | 4 +-
src/kernel_services/analysis/stmts_graph.mli | 4 +-
src/kernel_services/ast_data/alarms.mli | 11 +---
src/kernel_services/ast_data/annotations.mli | 21 --------
src/kernel_services/ast_data/ast.mli | 1 -
src/kernel_services/ast_data/cil_types.mli | 4 --
.../ast_data/kernel_function.mli | 2 +-
src/kernel_services/ast_data/property.mli | 22 +-------
src/kernel_services/ast_printing/printer.mli | 3 +-
.../ast_printing/printer_api.mli | 11 +---
src/kernel_services/ast_queries/ast_info.mli | 5 +-
src/kernel_services/ast_queries/cil.mli | 51 +++++--------------
src/kernel_services/ast_queries/cil_const.mli | 1 -
src/kernel_services/ast_queries/file.mli | 6 ---
src/kernel_services/ast_queries/filecheck.mli | 1 -
.../ast_queries/logic_const.mli | 30 ++++-------
.../ast_queries/logic_typing.mli | 1 -
.../ast_queries/logic_utils.mli | 5 +-
.../cmdline_parameters/cmdline.mli | 22 ++------
.../parameter_customize.mli | 5 +-
.../cmdline_parameters/parameter_sig.mli | 2 -
src/kernel_services/parsetree/logic_ptree.mli | 1 -
.../plugin_entry_points/db.mli | 39 +++-----------
.../plugin_entry_points/dynamic.mli | 8 +--
.../plugin_entry_points/kernel.mli | 2 -
.../plugin_entry_points/log.mli | 17 +------
.../plugin_entry_points/plugin.mli | 2 -
src/libraries/datatype/structural_descr.mli | 4 +-
src/libraries/datatype/type.mli | 7 +--
src/libraries/project/project.mli | 22 ++------
src/libraries/project/state.mli | 3 +-
src/libraries/project/state_builder.mli | 3 +-
src/libraries/stdlib/extlib.mli | 7 +--
src/libraries/utils/command.mli | 1 -
src/libraries/utils/filepath.mli | 1 -
src/libraries/utils/hook.mli | 4 +-
src/libraries/utils/pretty_utils.mli | 7 +--
src/plugins/aorai/aorai_utils.mli | 2 -
src/plugins/gui/design.mli | 9 +---
src/plugins/gui/filetree.mli | 13 +----
src/plugins/gui/gtk_helper.mli | 3 +-
src/plugins/gui/menu_manager.mli | 3 +-
src/plugins/slicing/Slicing.mli | 11 ++--
src/plugins/slicing/api.mli | 8 ++-
src/plugins/sparecode/Sparecode.mli | 1 -
src/plugins/sparecode/register.mli | 3 +-
51 files changed, 85 insertions(+), 324 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_lexer.mli b/src/kernel_internals/parsing/logic_lexer.mli
index 9b4d0aa4a0a..137ddec9b08 100644
--- a/src/kernel_internals/parsing/logic_lexer.mli
+++ b/src/kernel_internals/parsing/logic_lexer.mli
@@ -47,4 +47,4 @@ val ext_spec : Lexing.lexbuf -> Logic_ptree.ext_spec
(** ACSL extension for parsing external spec file.
Here, the tokens "/*" and "*/" are accepted by the lexer
as unnested C comments into the external ACSL specifications.
- @modify Sulfur-20171101 to accept /* */ as C comments. *)
+*)
diff --git a/src/kernel_internals/runtime/fc_config.mli b/src/kernel_internals/runtime/fc_config.mli
index 5bbe24571ce..df22d0880ef 100644
--- a/src/kernel_internals/runtime/fc_config.mli
+++ b/src/kernel_internals/runtime/fc_config.mli
@@ -80,8 +80,7 @@ val libdir: Filepath.Normalized.t
@since Beryllium-20090601-beta1 *)
val plugin_dir: Filepath.Normalized.t list
-(** Directory where the Frama-C dynamic plug-ins are.
- @modify Magnesium-20151001 *)
+(** Directory where the Frama-C dynamic plug-ins are. *)
val plugin_path: string
(** The colon-separated concatenation of [plugin_dir].
diff --git a/src/kernel_internals/runtime/messages.mli b/src/kernel_internals/runtime/messages.mli
index 6c01bd47c14..b594b7b61a1 100644
--- a/src/kernel_internals/runtime/messages.mli
+++ b/src/kernel_internals/runtime/messages.mli
@@ -23,8 +23,7 @@
(** Stored messages for persistence between sessions. *)
val iter: (Log.event -> unit) -> unit
-(** Iter over all stored messages. The messages are passed in emission order.
- @modify Nitrogen-20111001 Messages are now passed in emission order. *)
+(** Iter over all stored messages. The messages are passed in emission order. *)
val fold: ('a -> Log.event -> 'a) -> 'a -> 'a
(** Fold over all stored messages. The messages are passed in emission order. *)
diff --git a/src/kernel_internals/typing/cabs2cil.mli b/src/kernel_internals/typing/cabs2cil.mli
index f15e3a97b31..c58c8715399 100644
--- a/src/kernel_internals/typing/cabs2cil.mli
+++ b/src/kernel_internals/typing/cabs2cil.mli
@@ -265,8 +265,6 @@ val areCompatibleTypes: Cil_types.typ -> Cil_types.typ -> bool
compatible to avoid spurious casts.
@since Neon-20140301
- @modify Phosphorus-20170501-beta1
- @modify Chlorine-20180501 refined notion
*)
val stmtFallsThrough: Cil_types.stmt -> bool
diff --git a/src/kernel_internals/typing/oneret.mli b/src/kernel_internals/typing/oneret.mli
index bfc40abefa3..845c74dc833 100644
--- a/src/kernel_internals/typing/oneret.mli
+++ b/src/kernel_internals/typing/oneret.mli
@@ -106,7 +106,7 @@ val encapsulate_local_vars: Cil_types.fundec -> unit
Replace all the other returns with Goto. Make sure that there is a return
if the function is supposed to return something, and it is not declared to
not return.
- @modify Sulfur-20171101 The [~callback], when provided,
- is invoked with all the original returns clauses and their associated
- annotation on inserted gotos. *)
+
+ The [~callback], when provided, is invoked with all the original returns
+ clauses and their associated annotation on inserted gotos. *)
val oneret: ?callback:callback -> Cil_types.fundec -> unit
diff --git a/src/kernel_services/analysis/service_graph.mli b/src/kernel_services/analysis/service_graph.mli
index 56a7ce927f5..f67019460cf 100644
--- a/src/kernel_services/analysis/service_graph.mli
+++ b/src/kernel_services/analysis/service_graph.mli
@@ -50,7 +50,7 @@ module type S = sig
val entry_point: unit -> Service_graph.V.t option
(** [compute] must be called before
@since Carbon-20101201
- @modify Nitrogen-20111001 return an option type *)
+ *)
module TP: Graph.Graphviz.GraphWithDotAttrs
with type t = Service_graph.t
@@ -66,7 +66,6 @@ module Make
(G: sig
type t
module V: sig
- (** @modify Oxygen-20120901 require [compare] *)
include Graph.Sig.COMPARABLE
val id: t -> int
(** assume [id >= 0] and unique for each vertices of the graph *)
@@ -74,7 +73,6 @@ module Make
val name: t -> string
val attributes: t -> Graph.Graphviz.DotAttributes.vertex list
val entry_point: unit -> t option
- (** @modify Nitrogen-20111001 return an option*)
end
val iter_vertex : (V.t -> unit) -> t -> unit
val iter_succ : (V.t -> unit) -> t -> V.t -> unit
diff --git a/src/kernel_services/analysis/stmts_graph.mli b/src/kernel_services/analysis/stmts_graph.mli
index decbfbaad9c..e7e0eeaa9ed 100644
--- a/src/kernel_services/analysis/stmts_graph.mli
+++ b/src/kernel_services/analysis/stmts_graph.mli
@@ -46,9 +46,7 @@ val stmt_is_in_cycle_filtered : (stmt -> bool) -> stmt -> bool
on its input *)
(** [reachable_stmts kf stmt] returns the transitive closure of the successors
- of [stmt] in [kf]. The result is cached for later calls.
-
- @modify Silicon-20161101 return type changed to hptset *)
+ of [stmt] in [kf]. The result is cached for later calls. *)
val reachable_stmts: kernel_function -> stmt -> Stmt.Hptset.t
(** Get the statements that compose [s]. For a simple statement (not containing
diff --git a/src/kernel_services/ast_data/alarms.mli b/src/kernel_services/ast_data/alarms.mli
index 53ffb88c696..adfe341aaf4 100644
--- a/src/kernel_services/ast_data/alarms.mli
+++ b/src/kernel_services/ast_data/alarms.mli
@@ -20,8 +20,7 @@
(* *)
(**************************************************************************)
-(** Alarms Database.
- @modify Fluorine-20130401 fully re-implemented. *)
+(** Alarms Database. *)
open Cil_types
@@ -33,7 +32,6 @@ type overflow_kind =
type access_kind = For_reading | For_writing
type bound_kind = Lower_bound | Upper_bound
-(** @modify Fluorine-20130401 full re-implementation *)
type alarm =
| Division_by_zero of exp
| Memory_access of lval * access_kind
@@ -82,12 +80,7 @@ val register:
@return true if the given alarm has never been emitted before on the
same kinstr (without taking into consideration the status or
the emitter).
-
- @modify Oxygen-20120901 remove labeled argument ~deps
- @modify Fluorine-20130401 add the optional arguments [kf], [loc] and
- [save]; also returns the corresponding code_annotation
- @modify Aluminium-20160501 removed argument save. Use
- {!to_annot} instead. *)
+*)
val to_annot: kinstr -> ?loc:location -> alarm -> code_annotation * bool
(** Conversion of an alarm to a [code_annotation], without any registration.
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index cea099e3d89..79712871f4d 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -22,7 +22,6 @@
(** Annotations in the AST.
The AST should be computed before calling functions of this module.
- @modify Oxygen-20120901 fully rewritten.
@plugin development guide *)
open Cil_types
@@ -132,7 +131,6 @@ val iter_all_code_annot:
If [sorted] is [true] (the default), iteration is sorted according
to the location of the statements and by emitter. Note that the
sorted version is less efficient than the unsorted iteration.
- @modify Sodium-20150201: iteration is sorted
*)
val fold_all_code_annot:
@@ -140,7 +138,6 @@ val fold_all_code_annot:
(stmt -> Emitter.t -> code_annotation -> 'a -> 'a) -> 'a -> 'a
(** Fold on each code annotation of the program. See above for
the meaning of the [sorted] argument.
- @modify Sodium-20150201 sorted fold
*)
val iter_global:
@@ -347,22 +344,16 @@ val add_behaviors:
(** Add new behaviors into the given contract.
if [register_children] is [true] (the default), inner clauses of the
behavior will also be registered by the function.
-
- @modify Aluminium-20160501 restructuration of annotations management
*)
val add_decreases: Emitter.t -> kernel_function -> variant -> unit
(** Add a decrease clause into the contract of the given function.
No decrease clause must previously be attached to this function.
-
- @modify Aluminium-20160501 restructuration of annotations management
*)
val add_terminates: identified_predicate contract_component_addition
(** Add a terminates clause into a contract.
No terminates clause must previously be attached to this contract.
-
- @modify Aluminium-20160501 restructuration of annotations management
*)
val add_complete: string list contract_component_addition
@@ -372,8 +363,6 @@ val add_complete: string list contract_component_addition
@raise Fatal if one of the given name
is either an unknown behavior or {!Cil.default_behavior_name}.
-
- @modify Aluminium-20160501 restructuration of annotations management
*)
val add_disjoint: string list contract_component_addition
@@ -383,14 +372,10 @@ val add_disjoint: string list contract_component_addition
@raise Fatal if one of the given name
is either an unknown behavior or {!Cil.default_behavior_name}.
-
- @modify Aluminium-20160501 restructuration of annotations management
*)
val add_requires: identified_predicate list behavior_component_addition
(** Add new requires clauses into the given behavior.
-
- @modify Aluminium-20160501 restructuration of annotations management
*)
val add_assumes: identified_predicate list behavior_component_addition
@@ -398,15 +383,11 @@ val add_assumes: identified_predicate list behavior_component_addition
Does nothing but emitting a warning if an attempt is
made to add assumes clauses to the default behavior.
-
- @modify Aluminium-20160501 restructuration of annotations management
*)
val add_ensures:
(termination_kind * identified_predicate) list behavior_component_addition
(** Add new ensures clauses into the given behavior.
-
- @modify Aluminium-20160501 restructuration of annotations management
*)
val add_assigns:
@@ -417,8 +398,6 @@ val add_assigns:
the assigns clause remains empty. (That corresponds to the ACSL semantics of
an assigns clause: if no assigns is specified, that is equivalent to assigns
everything.)
-
- @modify Aluminium-20160501 restructuration of annotations management
*)
val add_allocates:
diff --git a/src/kernel_services/ast_data/ast.mli b/src/kernel_services/ast_data/ast.mli
index 5730dc5a08b..b8fbba2777c 100644
--- a/src/kernel_services/ast_data/ast.mli
+++ b/src/kernel_services/ast_data/ast.mli
@@ -40,7 +40,6 @@ module UntypedFiles: sig
@raise NoUntypedAst if no untyped AST is available. This is in
particular the case for projects obtained by code transformation from
original C files.
- @modify Nitrogen-20111001 raise NoUntypedAst
*)
val set: Cabs.file list -> unit
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 8f13b954a39..28e7ce49ef6 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1689,10 +1689,6 @@ and ext_code_annot_context =
(** Behavior of a function or statement. This type shares the name of its
constructors with {!Logic_ptree.behavior}.
- @since Oxygen-20120901 [b_allocation] has been added.
- @since Carbon-20101201 [b_requires] has been added.
- @modify Boron-20100401 [b_ensures] is replaced by [b_post_cond].
- Old [b_ensures] represent the [Normal] case of [b_post_cond].
*)
and behavior = {
mutable b_name : string; (** name of the behavior. *)
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index 0dbc5fed323..5e1be0e3bc8 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -54,7 +54,7 @@ val find_first_stmt : t -> stmt
val find_return : t -> stmt
(** Find the return statement of a kernel function.
@raise No_Statement is the kernel function is only a prototype.
- @modify Nitrogen-20111001 may raise No_Statement*)
+*)
val find_label : t -> string -> stmt ref
(** Find a given label in a kernel function.
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 77c5e587c41..6d9f38b4c4e 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -256,7 +256,6 @@ val o_loc_of_stmt: kernel_function -> kinstr -> other_loc
val ip_other: string -> other_loc -> identified_property
(** Create a non-standard property.
@since Nitrogen-20111001
- @modify 18.0-Argon Refine localisation argument
*)
val ip_reachable_stmt: kernel_function -> stmt -> identified_property
@@ -295,7 +294,6 @@ val ip_of_ensures:
(** Extended property.
@since Chlorine-20180501
- @modify 18.0-Argon refine localisation argument
*)
val ip_of_extended: extended_loc -> acsl_extension -> identified_property
@@ -314,7 +312,6 @@ val ip_of_allocation:
behavior [bhv], in the spec in function [kf], at statement [ki], under
active behaviors [active]
@since Oxygen-20120901
- @modify Aluminium-20160501 added active argument
*)
val ip_allocation_of_behavior:
kernel_function -> kinstr -> active:string list ->
@@ -330,7 +327,6 @@ val ip_of_assigns:
builds IPAssigns for a contract (if not WritesAny).
See {!ip_allocation_of_behavior} for signification of [active].
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_assigns_of_behavior:
kernel_function -> kinstr -> active:string list ->
@@ -338,7 +334,7 @@ val ip_assigns_of_behavior:
(** Builds the corresponding IPFrom (if not FromAny)
@since Carbon-20110201
- @modify Aluminium-20160501 returns an option. *)
+*)
val ip_of_from:
kernel_function -> kinstr ->
behavior_or_loop -> from -> identified_property option
@@ -347,7 +343,6 @@ val ip_of_from:
builds IPFrom for a behavior (if not ReadsAny).
See {!ip_from_of_behavior} for signification of [active]
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_from_of_behavior:
kernel_function -> kinstr -> active:string list ->
@@ -368,7 +363,6 @@ val ip_from_of_code_annot:
assigns and from). See {!ip_allocation_of_behavior} for the signification
of the [active] argument.
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_post_cond_of_behavior:
kernel_function -> kinstr -> active:string list ->
@@ -378,7 +372,6 @@ val ip_post_cond_of_behavior:
to the behavior itself.
See {!ip_allocation_of_behavior} for signification of [active]
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_of_behavior:
kernel_function -> kinstr -> active:string list ->
@@ -387,7 +380,6 @@ val ip_of_behavior:
(** [ip_all_of_behavior kf ki active bhv] builds all IP related to a behavior.
See {!ip_allocation_of_behavior} for signification of [active]
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_all_of_behavior:
kernel_function -> kinstr -> active:string list ->
@@ -396,7 +388,6 @@ val ip_all_of_behavior:
(** [ip_of_complete kf ki active complete] builds IPComplete.
See {!ip_allocation_of_behavior} for signification of [active]
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_of_complete:
kernel_function -> kinstr -> active:string list ->
@@ -405,7 +396,6 @@ val ip_of_complete:
(** [ip_complete_of_spec kf ki active spec] builds IPComplete of a given spec.
See {!ip_allocation_of_behavior} for signification of [active]
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_complete_of_spec:
kernel_function -> kinstr -> active:string list ->
@@ -414,7 +404,6 @@ val ip_complete_of_spec:
(** [ip_of_disjoint kf ki active disjoint] builds IPDisjoint.
See {!ip_allocation_of_behavior} for signification of [active]
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_of_disjoint:
kernel_function -> kinstr -> active:string list ->
@@ -423,7 +412,6 @@ val ip_of_disjoint:
(** [ip_disjoint_of_spec kf ki active spec] builds IPDisjoint of a given spec.
See {!ip_allocation_of_behavior} for signification of [active]
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_disjoint_of_spec:
kernel_function -> kinstr -> active:string list ->
@@ -452,7 +440,6 @@ val ip_decreases_of_spec:
builds all IP of post-conditions related to a spec.
See {!ip_post_cond_of_behavior} for more information.
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_post_cond_of_spec:
kernel_function -> kinstr -> active:string list ->
@@ -461,7 +448,6 @@ val ip_post_cond_of_spec:
(** [ip_of_spec kf ki active spec] builds all IP related to a spec.
See {!ip_allocation_of_behavior} for signification of [active]
@since Carbon-20110201
- @modify Aluminium-20160501 added active argument
*)
val ip_of_spec:
kernel_function -> kinstr -> active:string list ->
@@ -476,7 +462,6 @@ val ip_property_instance:
(** Build an IPLemma.
@since Nitrogen-20111001
- @modify Oxygen-20120901 takes an identified_lemma instead of a string
*)
val ip_lemma: identified_lemma -> identified_property
@@ -553,13 +538,10 @@ sig
val get_prop_name_id: identified_property -> string
(** returns a unique name identifying the property.
This name is built from the basename of the property.
- @modify 19.0-Potassium new naming scheme, Cf. LegacyNames
*)
val get_prop_basename: ?truncate:int -> identified_property -> string
- (** returns the basename of the property.
- @modify 19.0-Potassium additional truncation parameter
- *)
+ (** returns the basename of the property. *)
end
diff --git a/src/kernel_services/ast_printing/printer.mli b/src/kernel_services/ast_printing/printer.mli
index 887e1f154e4..0bf1ce55ba3 100644
--- a/src/kernel_services/ast_printing/printer.mli
+++ b/src/kernel_services/ast_printing/printer.mli
@@ -20,8 +20,7 @@
(* *)
(**************************************************************************)
-(** AST's pretty-printer.
- @modify Fluorine-20130401 fully change this API *)
+(** AST's pretty-printer. *)
include Printer_api.S
diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index 17c67011356..d8ff44a66c4 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -108,16 +108,12 @@ class type extensible_printer_type = object
method private require_braces: block_ctxt -> block -> bool
(** @return [true] if the given block must be enclosed in a pair of braces,
given the context in which it appears.
- @modify Fluorine-20130401 optional arguments has been modified.
- @modify Phosphorus-20170501-beta1 use proper context to determine result
*)
method private inline_block: block_ctxt -> block -> bool
(** @return [true] if the given block may be inlined in a single line.
[has_annot] indicates if the stmt corresponding to the block may have
annotations (default is [true]).
- @modify Fluorine-20130401 optional arguments has been modified.
- @modify Phosphorus-20170501-beta1 use proper context to determine result
*)
method private get_instr_terminator: unit -> string
@@ -226,9 +222,7 @@ class type extensible_printer_type = object
method next_stmt : stmt -> Format.formatter -> stmt -> unit
method block: Format.formatter -> block -> unit
- (** Prints a block.
- @modify Fluorine-20130401 optional arguments has been modified.
- @modify Phosphorus-20170501-beta1 no more options for pretty-printing *)
+ (** Prints a block. *)
method exp: Format.formatter -> exp -> unit
(** Print expressions *)
@@ -280,8 +274,7 @@ class type extensible_printer_type = object
method post_cond:
Format.formatter -> (termination_kind * identified_predicate) -> unit
- (** pretty prints a post condition according to the exit kind it represents
- @modify Boron-20100401 replaces [pEnsures] *)
+ (** pretty prints a post condition according to the exit kind it represents *)
method assumes: Format.formatter -> identified_predicate -> unit
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index 9413778ddbe..c39540eb78c 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -87,7 +87,6 @@ val behavior_postcondition :
goal:bool -> funbehavior -> termination_kind -> predicate
(** Builds the postcondition from [b_assumes] and [b_post_cond] clauses.
For flag [~goal] see {Ast_info.precondition} above.
- @modify Boron-20100401 added termination kind as filtering argument.
@modify 23.0-Vanadium introduce [goal] flag
*)
@@ -121,8 +120,8 @@ val merge_assigns_from_spec: ?warn:bool -> funspec -> assigns
val merge_assigns: ?warn:bool -> funbehavior list -> assigns
(** Returns the assigns of an unguarded behavior.
- @modify Oxygen-20120901 Optional [warn] argument added which can be used to
- force emitting or cancelation of warnings. *)
+ Optional [warn] argument can be used to force emitting or cancelation of
+ warnings. *)
val variable_term: location -> logic_var -> term
val constant_term: location -> Integer.t -> term
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 52f580d316e..2d4dcd14e79 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -168,7 +168,6 @@ val selfFormalsDecl: State.t
val makeFormalsVarDecl: ?ghost:bool -> (string * typ * attributes) -> varinfo
(** creates a new varinfo for the parameter of a prototype.
By default, this formal variable is not ghost.
- @modify 20.0-Calcium adds a parameter for ghost status
*)
(** Update the formals of a function declaration from its identifier and its
@@ -475,8 +474,7 @@ val integralPromotion : Cil_types.typ -> Cil_types.typ
val isAnyCharType: typ -> bool
(** True if the argument is a plain character type
- (but neither [signed char] nor [unsigned char]).
- @modify Chlorine-20180501 old behavior renamed as [isAnyCharType] *)
+ (but neither [signed char] nor [unsigned char]). *)
val isCharType: typ -> bool
(** True if the argument is a short type (i.e. signed or unsigned) *)
@@ -488,8 +486,7 @@ val isShortType: typ -> bool
val isAnyCharPtrType: typ -> bool
(** True if the argument is a pointer to a plain character type
- (but neither [signed char] nor [unsigned char]).
- @modify Chlorine-20180501 old behavior renamed as [isAnyCharPtrType] *)
+ (but neither [signed char] nor [unsigned char]). *)
val isCharPtrType: typ -> bool
(** True if the argument is a pointer to a constant character type,
@@ -504,7 +501,7 @@ val isAnyCharArrayType: typ -> bool
(** True if the argument is an array of a character type
(i.e. plain, signed or unsigned)
- @modify Chlorine-20180501 old behavior renamed as [isAnyCharArrayType] *)
+*)
val isCharArrayType: typ -> bool
(** True if the argument is an integral type (i.e. integer or enum) *)
@@ -524,28 +521,23 @@ val isLogicPureBooleanType: logic_type -> bool
val isIntegralOrPointerType: typ -> bool
(** True if the argument is an integral type (i.e. integer or enum), either
- C or mathematical one.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+ C or mathematical one. *)
val isLogicIntegralType: logic_type -> bool
(** True if the argument is a boolean type, either integral C type or
- mathematical boolean one.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+ mathematical boolean one. *)
val isLogicBooleanType: logic_type -> bool
(** True if the argument is a floating point type. *)
val isFloatingType: typ -> bool
-(** True if the argument is a floating point type.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+(** True if the argument is a floating point type. *)
val isLogicFloatType: logic_type -> bool
-(** True if the argument is a C floating point type or logic 'real' type.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+(** True if the argument is a C floating point type or logic 'real' type. *)
val isLogicRealOrFloatType: logic_type -> bool
-(** True if the argument is the logic 'real' type.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+(** True if the argument is the logic 'real' type. *)
val isLogicRealType: logic_type -> bool
(** True if the argument is an arithmetic type (i.e. integer, enum or
@@ -564,8 +556,7 @@ val isScalarType: typ -> bool
val isArithmeticOrPointerType: typ -> bool
(** True if the argument is a logic arithmetic type (i.e. integer, enum or
- floating point, either C or mathematical one.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+ floating point, either C or mathematical one. *)
val isLogicArithmeticType: logic_type -> bool
(** True if the argument is a function type *)
@@ -588,8 +579,7 @@ val isFunPtrType: typ -> bool
@since 18.0-Argon *)
val isLogicFunPtrType: logic_type -> bool
-(** True if the argument is the type for reified C types.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+(** True if the argument is the type for reified C types. *)
val isTypeTagType: logic_type -> bool
(** True if the argument denotes the type of ... in a variadic function.
@@ -686,7 +676,6 @@ val splitFunctionTypeVI:
[vdecl] .
The first unnamed argument specifies whether the varinfo is for a global and
the second is for formals.
- @modify 19.0-Potassium adds an optional ghost parameter
*)
val makeVarinfo:
?source:bool -> ?temp:bool -> ?referenced:bool -> ?ghost:bool -> ?loc:Location.t -> bool -> bool
@@ -705,8 +694,6 @@ val makeVarinfo:
- specifying ghost to false if the function is ghost leads to an error
- when [where] is specified, its status must be the same as the formal to
insert (else, it cannot be found in the list of ghost or non ghost formals)
-
- @modify 19.0-Potassium adds the optional ghost parameter
*)
val makeFormalVar: fundec -> ?ghost:bool -> ?where:string -> ?loc:Location.t -> string -> typ -> varinfo
@@ -717,9 +704,6 @@ val makeFormalVar: fundec -> ?ghost:bool -> ?where:string -> ?loc:Location.t ->
The variable is attached to the toplevel block if [scope] is not specified.
If the name passed as argument already exists within the function,
a fresh name will be generated for the varinfo.
-
- @modify Chlorine-20180501 the name of the variable is guaranteed to be fresh.
- @modify 20.0-Calcium add ghost optional argument
*)
val makeLocalVar:
fundec -> ?scope:block -> ?temp:bool -> ?referenced:bool -> ?insert:bool ->
@@ -742,15 +726,12 @@ val refresh_local_name: fundec -> varinfo -> unit
among other locals of the function. The value for [insert] should
only be changed if you are completely sure this is not useful.
- @modify 20.0-Calcium add ghost optional argument
*)
val makeTempVar: fundec -> ?insert:bool -> ?ghost:bool -> ?name:string ->
?descr:string -> ?descrpure:bool -> ?loc:Location.t -> typ -> varinfo
(** Make a global variable. Your responsibility to make sure that the name
is unique. [source] defaults to [true]. [temp] defaults to [false].
-
- @modify 20.0-Calcium add ghost optional arg
*)
val makeGlobalVar: ?source:bool -> ?temp:bool -> ?referenced:bool ->
?ghost:bool -> ?loc:Cil_datatype.Location.t -> string -> typ -> varinfo
@@ -967,7 +948,6 @@ val mkMem: addr:exp -> off:offset -> lval
casts between arithmetic types as needed, or between pointer
types, but do not attempt to cast pointer to int or
vice-versa. Use appropriate binop (PlusPI & friends) for that.
- @modify Chlorine-20180501 no systematic cast to uintptr_t for ptr comparisons.
*)
val mkBinOp: loc:location -> binop -> exp -> exp -> exp
@@ -991,14 +971,12 @@ val mkString: loc:location -> string -> exp
(modulo typedefs). If [force] is [false] (the default), other equivalences
are considered, in particular between an enum and its representative
integer type.
- @modify Fluorine-20130401 added [force] argument
*)
val need_cast: ?force:bool -> typ -> typ -> bool
(** Construct a cast when having the old type of the expression. If the new
type is the same as the old type, then no cast is added, unless [force]
is [true] (default is [false])
- @modify Fluorine-20130401 add [force] argument
@modify 23.0-Vanadium change order or arguments
*)
val mkCastT: ?force:bool -> oldt:typ -> newt:typ -> exp -> exp
@@ -1093,7 +1071,7 @@ val mkStmtOneInstr: ?ghost:bool -> ?valid_sid:bool -> ?sattr:attributes ->
(** Returns an empty statement (of kind [Instr]). See [mkStmt] for [ghost] and
[valid_sid] arguments.
- @modify Neon-20130301 adds the [valid_sid] optional argument. *)
+*)
val mkEmptyStmt: ?ghost:bool -> ?valid_sid:bool -> ?sattr:attributes ->
?loc:location -> unit -> stmt
@@ -1119,9 +1097,6 @@ val mkPureExprInstr:
See {!Cil.mkStmt} for information about [ghost] and [valid_sid], and
{!Cil.mkPureExprInstr} for information about [loc].
-
- @modify Chlorine-20180501 lift optional arg valid_sid from [mkStmt] instead
- of relying on ill-fated default.
*)
val mkPureExpr:
?ghost:bool -> ?valid_sid:bool -> fundec:fundec ->
@@ -1934,7 +1909,6 @@ val visitCilBlock: cilVisitor -> block -> block
and contain definitions of local variables that are not part of the block.
@since Phosphorus-20170501-beta1
- @modify 19.0-Potassium: do not raise fatal as soon as the block has locals
*)
val transient_block: block -> block
@@ -2009,7 +1983,6 @@ val visitCilBehaviors: cilVisitor -> funbehavior list -> funbehavior list
(** visit an extended clause of a behavior.
@since Nitrogen-20111001
- @modify Silicon-20161101
*)
val visitCilExtended: cilVisitor -> acsl_extension -> acsl_extension
@@ -2206,7 +2179,7 @@ exception Not_representable
(** @return the smallest kind that will hold the integer's value.
The kind will be unsigned if the 2nd argument is true.
@raise Not_representable if the bigint is not representable.
- @modify Neon-20130301 may raise Not_representable. *)
+*)
val intKindForValue: Integer.t -> bool -> ikind
(** The size of a type, in bytes. Returns a constant expression or a "sizeof"
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index 62d0b788fa4..a7063999574 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -59,7 +59,6 @@ val set_vid: varinfo -> unit
(** returns a copy of the varinfo with a fresh vid.
If the varinfo has an associated logic var, a copy of the logic var
is made as well.
- @modify Oxygen-20120901 take logic var into account
*)
val copy_with_new_vid: varinfo -> varinfo
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index 51b50f02949..222d02f902c 100644
--- a/src/kernel_services/ast_queries/file.mli
+++ b/src/kernel_services/ast_queries/file.mli
@@ -59,8 +59,6 @@ val new_machdep: string -> Cil_types.mach -> unit
[Cmdline.run_after_loading_stage
(fun () -> File.new_machdep "my_machdep" my_machdep_implem)]
@since Nitrogen-20111001
- @modify Fluorine-20130401 Receives the machdep (as a module) as argument
- @modify Sodium-20150201 Receives directly the machdep as argument
@raise Invalid_argument if the given name already exists
@plugin development guide *)
@@ -192,7 +190,6 @@ val init_project_from_visitor:
if [reorder] is [true] (default is [false]) the new AST in [prj]
will be reordered.
@since Oxygen-20120901
- @modify Fluorine-20130401 added reorder optional argument
@plugin development guide
*)
@@ -210,8 +207,6 @@ val create_project_from_visitor:
file (i.e. it should use {!Cil.copy_visit} at some point).
@raise File_types.Bad_Initialization if called more than once.
@since Beryllium-20090601-beta1
- @modify Fluorine-20130401 added [reorder] optional argument
- @modify Sodium-20150201 added [last] optional argument
@plugin development guide *)
val create_rebuilt_project_from_visitor:
@@ -228,7 +223,6 @@ val create_rebuilt_project_from_visitor:
@raise File_types.Bad_Initialization if called more than once.
@since Nitrogen-20111001
- @modify Fluorine-20130401 added reorder optional argument
*)
val prepare_cil_file: Cil_types.file -> unit
diff --git a/src/kernel_services/ast_queries/filecheck.mli b/src/kernel_services/ast_queries/filecheck.mli
index 908fda95755..65f5b195e09 100644
--- a/src/kernel_services/ast_queries/filecheck.mli
+++ b/src/kernel_services/ast_queries/filecheck.mli
@@ -31,7 +31,6 @@ val check_ast: ?is_normalized:bool -> ?ast:Cil_types.file -> string -> unit
Note that the check is only partial.
@since Aluminium-20160501
- @modify Silicon-20161101 adds optional ast argument
*)
module type Extensible_checker =
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 72cb93fb3b0..adf4ec86d56 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -233,8 +233,7 @@ val unroll_ltdef : logic_type -> logic_type
val isLogicCType : (typ -> bool) -> logic_type -> bool
(** returns [true] if the type is a list<t>.
- @since Aluminium-20160501
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+ @since Aluminium-20160501 *)
val is_list_type: logic_type -> bool
(** [make_type_list_of t] returns the type list<[t]>.
@@ -243,45 +242,38 @@ val make_type_list_of: logic_type -> logic_type
(** returns the type of elements of a list type.
@raise Failure if the input type is not a list type.
- @since Aluminium-20160501
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+ @since Aluminium-20160501 *)
val type_of_list_elem: logic_type -> logic_type
(** returns [true] if the type is a set<t>.
- @since Neon-20140301
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+ @since Neon-20140301 *)
val is_set_type: logic_type -> bool
(** [set_conversion ty1 ty2] returns a set type as soon as [ty1] and/or [ty2]
is a set. Elements have type [ty1], or the type of the elements of [ty1] if
it is itself a set-type ({i.e.} we do not build set of sets that way).
- @modify 18.0-Argon expands the logic type definitions if necessary. *)
+*)
val set_conversion: logic_type -> logic_type -> logic_type
(** converts a type into the corresponding set type if needed. Does nothing
- if the argument is already a set type.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+ if the argument is already a set type. *)
val make_set_type: logic_type -> logic_type
(** returns the type of elements of a set type.
- @raise Failure if the input type is not a set type.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+ @raise Failure if the input type is not a set type. *)
val type_of_element: logic_type -> logic_type
(** [plain_or_set f t] applies [f] to [t] or to the type of elements of [t]
- if it is a set type.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+ if it is a set type. *)
val plain_or_set: (logic_type -> 'a) -> logic_type -> 'a
(** [transform_element f t] is the same as
[set_conversion (plain_or_set f t) t]
@since Nitrogen-20111001
- @modify 18.0-Argon expands the logic type definition if necessary.
*)
val transform_element: (logic_type -> logic_type) -> logic_type -> logic_type
-(** [true] if the argument is not a set type.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+(** [true] if the argument is not a set type. *)
val is_plain_type: logic_type -> bool
(** [make_arrow_type args rt] returns a [rt] if [args] is empty or the
@@ -291,12 +283,10 @@ val is_plain_type: logic_type -> bool
*)
val make_arrow_type: logic_var list -> logic_type -> logic_type
-(** @return true if the argument is the boolean type.
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+(** @return true if the argument is the boolean type. *)
val is_boolean_type: logic_type -> bool
-(** @since Sodium-20150201
- @modify 18.0-Argon expands the logic type definition if necessary. *)
+(** @since Sodium-20150201 *)
val boolean_type: logic_type
(* ************************************************************************** *)
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 3ea227024a1..17d832a2aff 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -207,7 +207,6 @@ sig
@param explicit true if the cast is present in original source.
defaults to false
@since Nitrogen-20111001
- @modify 19.0-Potassium introduces explicit param
*)
val mk_cast:
?explicit:bool -> Cil_types.term -> Cil_types.logic_type -> Cil_types.term
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index ef79c06f510..088f865c4ed 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -67,7 +67,6 @@ val isLogicType : (typ -> bool) -> logic_type -> bool
(** {3 Predefined tests over types} *)
val isLogicArrayType : logic_type -> bool
-(** @modify Chlorine-20180501 old behavior renamed as [isLogicAnyCharType] *)
val isLogicCharType : logic_type -> bool
(** @since Chlorine-20180501 *)
@@ -123,8 +122,7 @@ val mk_logic_pointer_or_StartOf : term -> term
performed automatically. If [force] is [true], the cast will always
be inserted. Otherwise (which is the default), [mk_cast typ t] will return
[t] if it is already of type [typ]
-
- @modify Aluminium-20160501 added [force] optional argument *)
+*)
val mk_cast: ?loc:location -> ?force:bool -> typ -> term -> term
@@ -434,7 +432,6 @@ val merge_behaviors :
(** [merge_funspec ?oldloc oldspec newspec] merges [newspec] into [oldspec].
If the funspec belongs to a kernel function, do not forget to call
{!Kernel_function.set_spec} after merging.
- @modify 20.0-Calcium add optional parameter [oldloc].
*)
val merge_funspec :
?oldloc:location -> ?silent_about_merging_behav:bool ->
diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli
index 59303001395..0b2328bbdad 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.mli
+++ b/src/kernel_services/cmdline_parameters/cmdline.mli
@@ -118,8 +118,7 @@ val at_error_exit: (exn -> unit) -> unit
code is greater than 0). The argument of the hook is the exception at the
origin of the error.
@since Boron-20100401
- @modify Neon-20130301 add the exception as argument of the
- hook. *)
+*)
(** Group of command line options.
@since Beryllium-20090901 *)
@@ -175,11 +174,6 @@ val catch_toplevel_run:
unit
(** Run [f]. When done, either call [at_normal_exit] if running [f] was ok;
or call [on_error] (and exits) in other cases.
- @modify Boron-20100401 additional arguments. They are now
- labelled
- @modify Neon-20140301 add the exception as argument of
- [on_error].
- @modify Magnesium-20151001 Removed argument [~quit]
*)
val run_normal_exit_hook: unit -> unit
@@ -189,14 +183,13 @@ val run_normal_exit_hook: unit -> unit
val run_error_exit_hook: exn -> unit
(** Run all the hooks registered by {!at_normal_exit}.
@since Boron-20100401
- @modify Neon-20130301 add the exception as argument. *)
+*)
val error_occurred: exn -> unit
(** Remember that an error occurred.
So {!run_error_exit_hook} will be called when Frama-C will exit.
@since Boron-20100401
- @modify Neon-20130301 add the exception as argument,
- fix spelling. *)
+*)
val bail_out: unit -> 'a
(** Stop Frama-C with exit 0.
@@ -220,11 +213,7 @@ val parse_and_boot:
toplevel provided by [get_toplevel]. [on_from_name] is [Project.on] on the
project corresponding to the given (unique) name.
@since Beryllium-20090901
- @modify Carbon-20101201
- @modify Sodium-20150201 the first argument of the first functional is no
- more a string option, just a string
- @modify Aluminium-20160501 add labels and generalize the type of
- [on_from_name] *)
+*)
val nb_given_options: unit -> int
(** Number of options provided by the user on the command line.
@@ -290,8 +279,7 @@ val add_option:
registered option. If [help] is [None], then the option is not shown
in the help.
@since Beryllium-20090601-beta1
- @modify Carbon-20101201
- @modify Oxygen-20120901 change type of ~help and add ~visible. *)
+*)
val add_option_without_action:
string ->
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.mli b/src/kernel_services/cmdline_parameters/parameter_customize.mli
index 56cfa1694ff..16219ce23f2 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_customize.mli
@@ -93,7 +93,7 @@ val is_invisible: unit -> unit
(** Prevent -help from listing the parameter.
Also imply {!is_not_reconfigurable}.
@since Carbon-20101201
- @modify Nitrogen-20111001 does not appear in the help *)
+*)
val argument_is_function_name: unit -> unit
(** Indicate that the string argument of the parameter must be a valid function
@@ -101,8 +101,7 @@ val argument_is_function_name: unit -> unit
analysed C program. Do nothing if the following applied functor has not type
[String].
@since Oxygen-20120901
- @modify Sodium-20150201 do nothing when applied to [String_set] or
- [String_list]. *)
+*)
val argument_may_be_fundecl: unit -> unit
(** Indicate that the argument of the parameter can match a valid function
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index 13e4e754a2d..53b574e6921 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -431,7 +431,6 @@ module type Set = sig
end
-(** @modify Sodium-20150201 *)
module type String_set =
Set with type elt = string and type t = Datatype.String.Set.t
@@ -467,7 +466,6 @@ module type List = sig
end
-(** @modify Sodium-20150201 *)
module type String_list = List with type elt = string and type t = string list
module type Filepath_list =
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index 413cb1a91ff..545f1cc5147 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -377,7 +377,6 @@ type code_annot =
| AExtended of string list * bool * extension
(** extension in a code or loop (when boolean flag is true) annotation.
@since Silicon-20161101
- @modify 18.0-Argon
*)
(** all kind of annotations*)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index e595d96f0bc..0e70c27d980 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -75,7 +75,6 @@ val register_compute:
string ->
State.t list ->
(unit -> unit) ref -> (unit -> unit) -> State.t
-(** @modify Boron-20100401 now return the state of the computation. *)
val register_guarded_compute:
string ->
@@ -619,51 +618,37 @@ module Properties : sig
val term_lval_to_lval:
(result: Cil_types.varinfo option -> term_lval -> Cil_types.lval) ref
- (** @raise No_conversion if the argument is not a left value.
- @modify Aluminium-20160501 raises a custom exn instead of generic Invalid_arg
- *)
+ (** @raise No_conversion if the argument is not a left value. *)
val term_to_lval:
(result: Cil_types.varinfo option -> term -> Cil_types.lval) ref
- (** @raise No_conversion if the argument is not a left value.
- @modify Aluminium-20160501 raises a custom exn instead of generic Invalid_arg
- *)
+ (** @raise No_conversion if the argument is not a left value. *)
val term_to_exp:
(result: Cil_types.varinfo option -> term -> Cil_types.exp) ref
- (** @raise No_conversion if the argument is not a valid expression.
- @modify Aluminium-20160501 raises a custom exn instead of generic Invalid_arg
- *)
+ (** @raise No_conversion if the argument is not a valid expression. *)
val loc_to_exp:
(result: Cil_types.varinfo option -> term -> Cil_types.exp list) ref
(** @return a list of C expressions.
@raise No_conversion if the argument is not a valid set of
- expressions.
- @modify Aluminium-20160501 raises a custom exn instead of generic Invalid_arg
- *)
+ expressions. *)
val loc_to_lval:
(result: Cil_types.varinfo option -> term -> Cil_types.lval list) ref
(** @return a list of C locations.
@raise No_conversion if the argument is not a valid set of
- left values.
- @modify Aluminium-20160501 raises a custom exn instead of generic Invalid_arg
- *)
+ left values. *)
val term_offset_to_offset:
(result: Cil_types.varinfo option -> term_offset -> offset) ref
- (** @raise No_conversion if the argument is not a valid offset.
- @modify Aluminium-20160501 raises a custom exn instead of generic Invalid_arg
- *)
+ (** @raise No_conversion if the argument is not a valid offset. *)
val loc_to_offset:
(result: Cil_types.varinfo option -> term -> Cil_types.offset list) ref
(** @return a list of C offset provided the term denotes locations who
have all the same base address.
- @raise No_conversion if the given term does not match the precondition
- @modify Aluminium-20160501 raises a custom exn instead of generic Invalid_arg
- *)
+ @raise No_conversion if the given term does not match the precondition *)
(** {3 From logic terms to Locations.location} *)
@@ -671,10 +656,7 @@ module Properties : sig
val loc_to_loc:
(result: Cil_types.varinfo option -> Value.state -> term ->
Locations.location) ref
- (** @raise No_conversion if the translation fails.
- @modify Aluminium-20160501 raises a custom exn instead of generic
- Invalid_arg
- *)
+ (** @raise No_conversion if the translation fails. *)
val loc_to_loc_under_over:
(result: Cil_types.varinfo option -> Value.state -> term ->
@@ -687,8 +669,6 @@ module Properties : sig
Warning: This API is not stabilized, and may change in
the future.
@raise No_conversion if the translation fails.
- @modify Aluminium-20160501 raises a custom exn instead of generic
- Invalid_arg
*)
(** {3 From logic terms to Zone.t} *)
@@ -787,9 +767,6 @@ module Properties : sig
val add_assert: Emitter.t -> kernel_function -> stmt -> string -> unit
(** @deprecated since Oxygen-20120901
Ask for {ACSL_importer plug-in} if you need such functionality.
- @modify Boron-20100401 takes as additional argument the
- computation which adds the assert.
- @modify Oxygen-20120901 replaces the State.t list by an Emitter.t
*)
end
diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli
index 71f0267fcfc..ae7cb6424ba 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.mli
+++ b/src/kernel_services/plugin_entry_points/dynamic.mli
@@ -35,8 +35,6 @@ 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.
- @modify Boron-20100401 add the labeled argument "plugin"
- @modify Oxygen-20120901 add the optional labeled argument "comment"
@plugin development guide *)
(* ************************************************************************* *)
@@ -157,8 +155,7 @@ end
*)
val load_packages: string list -> unit
-(** Load the module specification. See -load-module option.
- @modify Magnesium-20151001 new API. *)
+(** Load the module specification. See -load-module option. *)
val load_module: string -> unit
(** Sets the load path for modules in FRAMAC_PLUGIN, prepending it with [path].
@@ -176,8 +173,7 @@ val is_loaded: string -> bool
val load_plugin_path: unit -> unit
(** Load all plugins in the path set with [set_module_load_path].
Must be invoked only once from boot during extending stage.
- @since Magnesium-20151001 new API.
- @modify Phosphorus-20170501-beta1 changed signature. *)
+ @since Magnesium-20151001 new API. *)
(**/**)
(*
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 28f166f0a9e..701a9e89cee 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -513,8 +513,6 @@ module Orig_name: Parameter_sig.Bool
val normalization_parameters: unit -> Typed_parameter.t list
(** All the normalization options that influence the AST (in particular,
changing one will reset the AST entirely.contents
-
- @modify Chlorine-20180501 make it non-constant
*)
module WarnDecimalFloat: Parameter_sig.String
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index 72740f68e89..8d4a951ac2b 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -129,7 +129,6 @@ module type Messages = sig
Enabling a category (via -plugin-msg-category) will enable all its
subcategories.
@since Fluorine-20130401
- @modify Chlorine-20180501 categories are an abstract type of each plug-in
*)
type warn_category
@@ -161,8 +160,6 @@ module type Messages = sig
val feedback : ?ontty:ontty -> ?level:int -> ?dkey:category -> 'a pretty_printer
(** Progress and feedback. Level is tested against the verbosity level.
@since Beryllium-20090601-beta1
- @modify Fluorine-20130401 Optional parameter [?dkey]
- @modify Magnesium-20151001 Optional parameter [?ontty]
@plugin development guide *)
val debug : ?level:int -> ?dkey:category -> 'a pretty_printer
@@ -170,7 +167,6 @@ module type Messages = sig
Default level is 1. The debugging key is used in message headers.
See also [set_debug_keys] and [set_debug_keyset].
@since Beryllium-20090601-beta1
- @modify Nitrogen-20111001 Optional parameter [dkey]
@plugin development guide *)
val warning : ?wkey:warn_category -> 'a pretty_printer
@@ -302,7 +298,6 @@ module type Messages = sig
(** returns the corresponding registered category or [None] if no
such category exists.
@since Fluorine-20130401
- @modify Chlorine-20180501 return an option
*)
val get_all_categories: unit -> category list
@@ -313,22 +308,17 @@ module type Messages = sig
subcategories) to the set of categories for which messages are
to be displayed. The string must have been registered beforehand.
@since Fluorine-20130401 use categories instead of plain string
- @modify Chlorine-20180501 accepts a string as argument. Takes care
- of propagating to subcategories.
*)
val del_debug_keys: category -> unit
(** removes the given categories from the set for which messages are printed.
The string must have been registered beforehand.
@since Fluorine-20130401
- @modify Chlorine-20180501 accepts a string category as argument, takes care
- of propagating to subcategories
*)
val get_debug_keys: unit -> category list
(** Returns currently active keys
@since Fluorine-20130401
- @modify Chlorine-20180501 returns a list instead of a set
*)
val is_debug_key_enabled: category -> bool
@@ -443,7 +433,6 @@ val log_channel : channel ->
?kind:kind -> 'a pretty_printer
(** logging function to user-created channel.
@since Beryllium-20090901
- @modify Chlorine-20180501 removed ~prefix
@plugin development guide *)
val kernel_channel_name: string
@@ -455,9 +444,7 @@ val kernel_label_name: string
@since Beryllium-20090601-beta1 *)
val source : file:Filepath.Normalized.t -> line:int -> Filepath.position
-(** @since Chlorine-20180501
- @modify 18.0-Argon change type of [file]
-*)
+(** @since Chlorine-20180501 *)
val get_current_source : unit -> Filepath.position
@@ -501,7 +488,6 @@ val print_on_output : (Format.formatter -> unit) -> unit
Can not be recursively invoked.
@since Beryllium-20090901
- @modify Nitrogen-20111001 signature changed
@plugin development guide *)
val print_delayed : (Format.formatter -> unit) -> unit
@@ -512,7 +498,6 @@ val print_delayed : (Format.formatter -> unit) -> unit
Can not be recursively invoked.
@since Beryllium-20090901
- @modify Nitrogen-20111001 signature changed
@plugin development guide *)
(**/**)
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index da7d795389d..fbfa5c34806 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -76,8 +76,6 @@ end
(** Provided plug-general services for plug-ins.
@since Beryllium-20090601-beta1
- @modify Chlorine-20180501 removed programmatic access to [Debug_category]:
- managing categories is now entirely done by Log.Messages
@plugin development guide *)
module type S = sig
include Log.Messages
diff --git a/src/libraries/datatype/structural_descr.mli b/src/libraries/datatype/structural_descr.mli
index 2d719984056..ff1106d9e59 100644
--- a/src/libraries/datatype/structural_descr.mli
+++ b/src/libraries/datatype/structural_descr.mli
@@ -34,9 +34,7 @@ type recursive
type single_pack = private Unmarshal.t
-(** Structural descriptor used inside structures.
- @modify Nitrogen-20111001 this type is now private. Use smart
- constructors instead. *)
+(** Structural descriptor used inside structures. *)
type pack = private
| Nopack (** Was impossible to build a pack. *)
| Pack of single_pack (** A standard pack. *)
diff --git a/src/libraries/datatype/type.mli b/src/libraries/datatype/type.mli
index 0cc7b1ff57f..cf324f26944 100644
--- a/src/libraries/datatype/type.mli
+++ b/src/libraries/datatype/type.mli
@@ -96,10 +96,7 @@ val register:
[ml_name] is the OCaml name of the registered type value.
@raise AlreadyExists if the given name is already used by another type.
@raise Invalid_argument if [reprs] is the empty list
- @modify Boron-20100401 request a list of representant, not only a single
- one
- @modify Carbon-20101201 [value_name] is now [ml_name]. Must provide a
- structural descriptor. Argument [pp] does not exist anymore. *)
+*)
exception No_abstract_type of string
@@ -324,7 +321,7 @@ module type Heterogeneous_table = sig
argument was dynamically registered, then it may raise
[Incompatible_Type].
@raise AlreadyExists if [s] is already bound in [tbl].
- @modify Nitrogen-20111001 returns [unit] now. *)
+ *)
exception Unbound_value of string
exception Incompatible_type of string
diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli
index 47d055df191..fd9f1db8287 100644
--- a/src/libraries/project/project.mli
+++ b/src/libraries/project/project.mli
@@ -110,8 +110,7 @@ val set_name: t -> string -> unit
exception Unknown_project
val from_unique_name: string -> t
(** Return a project based on {!unique_name}.
- @raise Unknown_project if no project has this unique name.
- @modify Sodium-20150201 *)
+ @raise Unknown_project if no project has this unique name. *)
val set_current: ?on:bool -> ?selection:State_selection.t -> t -> unit
(** Set the current project with the given one.
@@ -133,8 +132,6 @@ val on: ?selection:State_selection.t -> t -> ('a -> 'b) -> 'a -> 'b
(** [on p f x] sets the current project to [p], computes [f x] then
restores the current project. You should use this function if you use a
project different of [current ()].
- @modify Carbon-20101201 replace the optional arguments [only] and
- [except] by a single one [selection].
@plugin development guide *)
val set_keep_current: bool -> unit
@@ -151,8 +148,7 @@ val copy: ?selection:State_selection.t -> ?src:t -> t -> unit
()]. Replace the destination by [src].
For each state to copy, the function [copy] given at state registration
time must be fully implemented.
- @modify Carbon-20101201 replace the optional arguments [only] and
- [except] by a single one [selection]. *)
+*)
val create_by_copy:
?selection:State_selection.t -> ?src:t -> last:bool -> string -> t
@@ -164,9 +160,7 @@ val create_by_copy:
applied when loading a project are applied (see {!load}).
If [last], then remember that the returned project is the last created
one (see {!last_created_by_copy}).
- @modify Carbon-20101201 replace the optional arguments [only] and
- [except] by a single one [selection].
- @modify Sodium-20150201 add the labeled argument [last]. *)
+*)
val create_by_copy_hook: (t -> t -> unit) -> unit
(** Register a hook to call at the end of {!create_by_copy}. The first
@@ -177,8 +171,6 @@ val clear: ?selection:State_selection.t -> ?project:t -> unit -> unit
(** Clear the given project. Default project is [current ()]. All the
internal states of the given project are now empty (wrt the action
registered with {!register_todo_on_clear}).
- @modify Carbon-20101201 replace the optional arguments [only] and
- [except] by a single one [selection].
@plugin development guide *)
val register_todo_before_clear: (t -> unit) -> unit
@@ -212,8 +204,6 @@ exception IOError of string
val save: ?selection:State_selection.t -> ?project:t -> Filepath.Normalized.t -> unit
(** Save a given project in a file. Default project is [current ()].
@raise IOError if the project cannot be saved.
- @modify Carbon-20101201 replace the optional arguments [only] and
- [except] by a single one [selection].
@plugin development guide *)
val load: ?selection:State_selection.t -> ?name:string -> Filepath.Normalized.t -> t
@@ -228,14 +218,10 @@ val load: ?selection:State_selection.t -> ?name:string -> Filepath.Normalized.t
}
@raise IOError if the project cannot be loaded
@return the new project containing the loaded data.
- @modify Carbon-20101201 replace the optional arguments [only] and
- [except] by a single one [selection].
@plugin development guide *)
val save_all: ?selection:State_selection.t -> Filepath.Normalized.t -> unit
(** Save all the projects in a file.
- @modify Carbon-20101201 replace the optional arguments [only] and
- [except] by a single one [selection].
@raise IOError a project cannot be saved. *)
val load_all: ?selection:State_selection.t -> Filepath.Normalized.t -> unit
@@ -243,8 +229,6 @@ val load_all: ?selection:State_selection.t -> Filepath.Normalized.t -> unit
file. For each project to load, the specification is the same than
{!Project.load}. Furthermore, after loading, all the hooks registered by
[register_after_set_current_hook] are applied.
- @modify Carbon-20101201 replace the optional arguments [only] and
- [except] by a single one [selection].
@raise IOError if a project cannot be loaded. *)
val register_before_load_hook: (unit -> unit) -> unit
diff --git a/src/libraries/project/state.mli b/src/libraries/project/state.mli
index 2f2bc82b2f0..cc8bbff434a 100644
--- a/src/libraries/project/state.mli
+++ b/src/libraries/project/state.mli
@@ -180,8 +180,7 @@ val create:
unique_name:string ->
name:string ->
t
-(** @since Carbon-20101201
- @modify Nitrogen-20111001 add the [on_update] argument *)
+(** @since Carbon-20101201 *)
val delete: t -> unit
(** @since Carbon-20101201 *)
diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli
index fbcfb611ded..15b0fe12ff2 100644
--- a/src/libraries/project/state_builder.mli
+++ b/src/libraries/project/state_builder.mli
@@ -291,8 +291,7 @@ module type Hashconsing_tbl =
(** Weak hashtbl dedicated to hashconsing.
Note that the resulting table is not saved on disk.
- @since Boron-20100401
- @modify Aluminium-20160501, renamed *)
+ @since Boron-20100401 *)
module Hashconsing_tbl_weak: Hashconsing_tbl
(** Hash table for hashconsing, but the internal table is _not_ weak
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index d8551183ffe..a03806ca24a 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -222,7 +222,6 @@ val the: exn:exn -> 'a option -> 'a
(** @raise Exn if the value is [None] and [exn] is specified.
@raise Invalid_argument if the value is [None] and [exn] is not specified.
@return v if the value is [Some v].
- @modify Magnesium-20151001 add optional argument [exn]
@modify 23.0-Vanadium optional argument [exn] now mandatory; otherwise,
use [Option.get], which is equivalent.
@plugin development guide *)
@@ -345,14 +344,10 @@ val temp_file_cleanup_at_exit: ?debug:bool -> string -> string -> string
to true, in which case a message with the name of the kept file will be
printed.
@raise Temp_file_error if the temp file cannot be created.
- @modify Nitrogen-20111001 may now raise Temp_file_error
- @modify Oxygen-20120901 optional debug argument
*)
val temp_dir_cleanup_at_exit: ?debug:bool -> string -> string
-(** @raise Temp_file_error if the temp dir cannot be created.
- @modify Nitrogen-20111001 may now raise Temp_file_error
- @modify Neon-20130301 add optional debug flag *)
+(** @raise Temp_file_error if the temp dir cannot be created. *)
val safe_remove: string -> unit
(** Tries to delete a file and never fails. *)
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index 52645e14bd1..7863d6e262e 100644
--- a/src/libraries/utils/command.mli
+++ b/src/libraries/utils/command.mli
@@ -42,7 +42,6 @@ val bincopy : bytes -> in_channel -> out_channel -> unit
and copy it in [cout].
[buffer] is a temporary string used during the copy.
Recommended size is [2048].
- @modify Silicon-20161101 [buffer] has now type [bytes] instead of [string]
*)
val copy : string -> string -> unit
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 1f3de6c2705..32de3d07eeb 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -49,7 +49,6 @@ exception File_exists
- non-existing directories in [realpath] may lead to ENOTDIR errors,
but [normalize] may accept them.
- @modify Aluminium-20160501 optional base_name.
@modify 21.0-Scandium optional existence.
*)
val normalize: ?existence:existence -> ?base_name:string -> string -> string
diff --git a/src/libraries/utils/hook.mli b/src/libraries/utils/hook.mli
index 5ceb0c52335..519c5bad69c 100644
--- a/src/libraries/utils/hook.mli
+++ b/src/libraries/utils/hook.mli
@@ -35,9 +35,7 @@ module type S = sig
*)
val extend: (param -> result) -> unit
- (** Add a new function to the hook.
- @modify Oxygen-20120901 no more [once] optional arg (see [extend_once])
- *)
+ (** Add a new function to the hook. *)
val extend_once: (param -> result) -> unit
(** Same as [extend], but the hook is added only if it is not already
diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index 1434abb59f7..524c0c6a49d 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -82,8 +82,6 @@ val pp_list: ?pre:sformat -> ?sep:sformat -> ?last:sformat -> ?suf:sformat ->
- the last separator to be put just before the last element (default:sep)
- the suffix to output after a non-empty list (default: close box)
- what to print if the list is empty (default: nothing)
-
- @modify Silicon-20161101 new optional argument [empty]
*)
val pp_array: ?pre:sformat -> ?sep:sformat -> ?suf:sformat -> ?empty:sformat ->
@@ -93,8 +91,6 @@ val pp_array: ?pre:sformat -> ?sep:sformat -> ?suf:sformat -> ?empty:sformat ->
- the separator between two elements (default: nothing)
- the suffix to output after a non-empty array (default: close box)
- what to print if the array is empty (default: nothing)
-
- @modify Silicon-20161101 new optional argument [empty]
*)
val pp_iter:
@@ -121,8 +117,7 @@ val pp_iter2:
val pp_opt: ?pre:sformat -> ?suf:sformat -> ?none:sformat -> 'a formatter -> 'a option formatter
(** pretty-prints an optional value. Prefix and suffix default to "@[" and "@]"
respectively. If the value is [None], pretty-print using [none].
-
- @modify Silicon-20161101 new optional argument [none] *)
+*)
val pp_cond: ?pr_false:sformat -> bool -> sformat formatter
(** [pp_cond cond f s] pretty-prints [s] if cond is [true] and the optional
diff --git a/src/plugins/aorai/aorai_utils.mli b/src/plugins/aorai/aorai_utils.mli
index 381dbcb2d49..b83ddf24d75 100644
--- a/src/plugins/aorai/aorai_utils.mli
+++ b/src/plugins/aorai/aorai_utils.mli
@@ -170,7 +170,6 @@ val update_to_pred:
related to the possible values of the auxiliary variables at current point
the function, guarded by the fact that we have followed this path, from
the given program point
- @modify Neon-20130301 add logic_label argument
*)
val action_to_pred:
start:Cil_types.logic_label ->
@@ -179,7 +178,6 @@ val action_to_pred:
(** All actions that might have been performed on aux variables from the
given program point, guarded by the path followed.
- @modify Neon-20140301 add logic_label argument
*)
val all_actions_preds:
Cil_types.logic_label ->
diff --git a/src/plugins/gui/design.mli b/src/plugins/gui/design.mli
index ae4018e81bf..e833a41927a 100644
--- a/src/plugins/gui/design.mli
+++ b/src/plugins/gui/design.mli
@@ -46,9 +46,7 @@ class type view_code = object
(** Move the pretty-printed source viewer to the given localizable
if possible. Return a boolean indicating whether the operation
succeeded
-
- @modify Nitrogen-20111001 Now indicates whether the
- operation succeeded. *)
+ *)
method display_globals : global list -> unit
(** Display the given globals in the pretty-printed source viewer. *)
@@ -84,7 +82,6 @@ class protected_menu_factory:
Gtk_helper.host -> GMenu.menu -> [ GMenu.menu ] GMenu.factory
(** This is the type of extension points for the GUI.
- @modify Boron-20100401 new way of handling the menu and the toolbar
@plugin development guide *)
class type main_window_extension_points = object
inherit view_code
@@ -171,9 +168,7 @@ class type main_window_extension_points = object
between start and stop in the given buffer.
Priority of [Gtext.tags] is used to decide which tag is rendered on
top of the other.
-
- @modify Aluminium-20160501: receives a {!reactive_buffer} instead
- of a {!GSourceView.source_buffer} *)
+ *)
method register_panel :
(main_window_extension_points->(string*GObj.widget*(unit-> unit) option))
diff --git a/src/plugins/gui/filetree.mli b/src/plugins/gui/filetree.mli
index 654a47bae14..b0dc9a0d153 100644
--- a/src/plugins/gui/filetree.mli
+++ b/src/plugins/gui/filetree.mli
@@ -66,8 +66,6 @@ class type t = object
menu is returned.
@since Nitrogen-20111001
- @modify Oxygen-20120901 Signature change for the filter argument,
- return the menu.
*)
method get_file_globals:
@@ -87,9 +85,7 @@ class type t = object
(was_activated:bool -> activating:bool -> filetree_node -> unit) -> unit
(** Register a callback that is called whenever an element of the file tree
is selected or unselected.
-
- @modify Nitrogen-20111001 Changed argument from a list
- of globals to [filetree_node] *)
+ *)
method append_text_column:
title:string ->
@@ -121,9 +117,6 @@ class type t = object
can be used to force an update on the display of the column
[`Visibility] means that the column must be show or hidden. [`Contents]
means what it contains has changed.
-
- @modify Nitrogen-20111001 Add third argument, and change return type
- @modify Oxygen-20120901 Change return type
*)
method select_global : Cil_types.global -> bool
@@ -133,9 +126,7 @@ class type t = object
provided they are not filtered out.) Unless you known what your
are doing, prefer calling [main_ui#select_or_display_global],
which is more resilient to globals not displayed in the filetree.
-
- @modify Nitrogen-20111001 Takes a [global] as argument, instead of
- a [varinfo]. Returns a boolean to indicate success or failure. *)
+ *)
method selected_globals : Cil_types.global list
(** @since Carbon-20101201
diff --git a/src/plugins/gui/gtk_helper.mli b/src/plugins/gui/gtk_helper.mli
index 34c05fad076..8cf09cb23d1 100644
--- a/src/plugins/gui/gtk_helper.mli
+++ b/src/plugins/gui/gtk_helper.mli
@@ -221,8 +221,7 @@ val register_locking_machinery:
unlocking actions. Default is [false]. At least one "lock_last" action is
allowed.
@since Beryllium-20090901
- @modify Boron-20100401 new optional argument [lock_last] and new
- argument [()] *)
+*)
(* ************************************************************************** *)
(** 2 Tooltips *)
diff --git a/src/plugins/gui/menu_manager.mli b/src/plugins/gui/menu_manager.mli
index aff7abcebf2..0c65bdfc6c5 100644
--- a/src/plugins/gui/menu_manager.mli
+++ b/src/plugins/gui/menu_manager.mli
@@ -42,8 +42,7 @@ type callback_state =
| Unit_callback of (unit -> unit)
| Bool_callback of (bool -> unit) * (unit -> bool)
-(** @since Boron-20100401
- @modify Nitrogen-20111001 *)
+(** @since Boron-20100401 *)
type entry = private {
e_where: where;
e_callback: callback_state (** callback called when the button is clicked *);
diff --git a/src/plugins/slicing/Slicing.mli b/src/plugins/slicing/Slicing.mli
index fb4dda8b2f6..3b17ef709fd 100644
--- a/src/plugins/slicing/Slicing.mli
+++ b/src/plugins/slicing/Slicing.mli
@@ -34,8 +34,7 @@ module Api:sig
(** Sets slicing parameters related to command line options
[-slicing-level], [-slice-callers], [-slice-undef-functions],
[-slicing-keep-annotations].
- @modify Sulfur-20171101 the optional argument and the related
- deprecated option [-slice-print] have been removed. *)
+ *)
(* ---------------------------------------------------------------------- *)
@@ -83,7 +82,7 @@ module Api:sig
The entry point function is only exported once :
it is VERY recommended to give to it its original name,
even if it is sliced.
- @modify Sulfur-20171101 argument order and arity. *)
+ *)
(** {3 Not for casual users} *)
@@ -203,7 +202,7 @@ module Api:sig
The selection preserves the [~rd] and ~[wr] accesses contained into
the statement [ki].
Note: add also a transparent selection on the whole statement.
- @modify Magnesium-20151001 argument [~scope] removed. *)
+ *)
val select_stmt_lval :
(set -> Mark.t -> Datatype.String.Set.t -> before:bool -> stmt ->
@@ -216,7 +215,7 @@ module Api:sig
The selection preserve the value of these lvalues before or
after (c.f. boolean [~before]) the statement [ki].
Note: add also a transparent selection on the whole statement.
- @modify Magnesium-20151001 argument [~scope] removed. *)
+ *)
val select_stmt_annots :
(set -> Mark.t -> spare:bool -> threat:bool -> user_assert:bool ->
@@ -236,7 +235,7 @@ module Api:sig
done just before the execution of the statement [~eval].
The selection preserve the value of these lvalues into the whole
project.
- @modify Magnesium-20151001 argument [~scope] removed. *)
+ *)
val select_func_lval :
(set -> Mark.t -> Datatype.String.Set.t -> kernel_function -> set)
diff --git a/src/plugins/slicing/api.mli b/src/plugins/slicing/api.mli
index bba2afb4077..b489bb90605 100644
--- a/src/plugins/slicing/api.mli
+++ b/src/plugins/slicing/api.mli
@@ -190,8 +190,7 @@ module Select : sig
execution of the statement [~eval].
The selection preserve the [~rd] and ~[wr] accesses contained into the
statement [ki].
- Note: add also a transparent selection on the whole statement.
- @modify Magnesium-20151001 argument [~scope] removed. *)
+ Note: add also a transparent selection on the whole statement. *)
val select_stmt_lval_rw :
set ->
Mark.t ->
@@ -207,8 +206,7 @@ module Select : sig
execution of the statement [~eval].
The selection preserve the value of these lvalues before or after (c.f.
boolean [~before]) the statement [ki].
- Note: add also a transparent selection on the whole statement.
- @modify Magnesium-20151001 argument [~scope] removed. *)
+ Note: add also a transparent selection on the whole statement. *)
val select_stmt_lval :
set ->
Mark.t ->
@@ -272,7 +270,7 @@ module Select : sig
The interpretation of the address of the lvalues is done just before the
execution of the statement [~eval].
The selection preserve the value of these lvalues into the whole project.
- @modify Magnesium-20151001 argument [~scope] removed. *)
+ *)
val select_func_lval_rw :
set -> Mark.t -> rd:Datatype.String.Set.t -> wr:Datatype.String.Set.t ->
eval:Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
diff --git a/src/plugins/sparecode/Sparecode.mli b/src/plugins/sparecode/Sparecode.mli
index 079e468002f..2f2b503634d 100644
--- a/src/plugins/sparecode/Sparecode.mli
+++ b/src/plugins/sparecode/Sparecode.mli
@@ -37,7 +37,6 @@ module Register: sig
* (the current one if no project given).
* The source project is not modified.
* The result is in the returned new project.
- * @modify Carbon-20110201 optional argument [new_proj_name] added
* *)
end
diff --git a/src/plugins/sparecode/register.mli b/src/plugins/sparecode/register.mli
index 01757a9ab08..6a325cc662e 100644
--- a/src/plugins/sparecode/register.mli
+++ b/src/plugins/sparecode/register.mli
@@ -30,5 +30,4 @@ val rm_unused_globals : ?new_proj_name:string -> ?project:Project.t -> unit -> P
(** Remove unused global types and variables from the given project
(the current one if no project given).
The source project is not modified.
- The result is in the returned new project.
- @modify Carbon-20110201 optional argument [new_proj_name] added. *)
+ The result is in the returned new project. *)
--
GitLab