diff --git a/src/kernel_internals/parsing/logic_lexer.mli b/src/kernel_internals/parsing/logic_lexer.mli
index 9b4d0aa4a0a84fa1f3d1a609e9e09ea36dc57e5a..137ddec9b08fc45f0988f6008228fc20ec71112d 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 5bbe24571ce738449348b68eb2860850bce369d4..df22d0880ef93afe96b86c7c505625118f8a169f 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 6c01bd47c149ea4f5d4f0bd221364b4177598aed..b594b7b61a1452018772c6effcc965ec866ddfb3 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 f15e3a97b31a45f205d88aad2d1c1a375f4b208a..868e4eb2284b47f3727fb0b9f04498ca1c1e6540 100644
--- a/src/kernel_internals/typing/cabs2cil.mli
+++ b/src/kernel_internals/typing/cabs2cil.mli
@@ -193,17 +193,6 @@ val find_field_offset:
*)
val logicConditionalConversion: Cil_types.typ -> Cil_types.typ -> Cil_types.typ
-(** returns the type of the result of an arithmetic operator applied to
- values of the corresponding input types.
- @deprecated Nitrogen-20111001 moved to Cil module
-*)
-val arithmeticConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ
-
-(** performs the usual integral promotions mentioned in C reference manual.
- @deprecated Nitrogen-20111001 moved to Cil module.
-*)
-val integralPromotion : Cil_types.typ -> Cil_types.typ
-
(** local information needed to typecheck expressions and statements *)
type local_env = private
{ authorized_reads: Cil_datatype.Lval.Set.t;
@@ -265,8 +254,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 bfc40abefa3e5327ebc6e0582a8ef3b8354cecac..845c74dc833cf1c89f6d156781cf797986311a4c 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/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index 24cc5937c02204c9648acca91748a1e45af24b13..60f2723a6eb11233802f814d92069d23baf28c40 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -759,7 +759,7 @@ struct
method! vpredicate_node p =
let fail () =
- raise (NYI (Pretty_utils.sfprintf
+ raise (NYI (Format.asprintf
"[logic_interp] %a" Printer.pp_predicate_node p))
in
match p with
diff --git a/src/kernel_services/analysis/service_graph.mli b/src/kernel_services/analysis/service_graph.mli
index 56a7ce927f5a4e4efe65ffc631fbe977c7feb699..f67019460cfae9a9f2ea32aaac2e809731f37bba 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 decbfbaad9c0808f42eecab6a0c89862504c94c7..e7e0eeaa9ed6fa757e8e65b6007a930df4d7653a 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 53ffb88c69613f001d0372bdaa3d1548c8aef836..adfe341aaf4c5b959955bf27e3c78bbf0c80f308 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 cea099e3d89ba723c173ff56b3e19656aafe96d0..485a8c2c3b6724503330b3f0468ae381ee4ad0f5 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:
@@ -284,7 +281,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 22.0-Titanium: add keep_empty argument
+ @before 22.0-Titanium there was no [keep_empty] optional argument
*)
val add_assert:
@@ -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,15 +398,13 @@ 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:
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 22.0-Titanium add keep_empty argument
+ @before 22.0-Titanium there is no [keep_empty] argument
*)
val add_extended: acsl_extension behavior_component_addition
diff --git a/src/kernel_services/ast_data/ast.mli b/src/kernel_services/ast_data/ast.mli
index 5730dc5a08b706789f55fad83e176e2820e544a2..b8fbba2777c77e3f1b1f7196c5bb437d1d8f36b2 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 8f13b954a39d7337a3a5e7eca15af4964316c234..28e7ce49ef681900375afdce3a27b3a91e361f51 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/globals.ml b/src/kernel_services/ast_data/globals.ml
index b83a9a114ec2a7a38152282f60d6733e00e040e6..cc79e169f7a5eec485c4d144ac0dad50bbf343c3 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -548,10 +548,6 @@ module FileIndex = struct
compute ();
S.find path
- let find path =
- let l = get_symbols path in
- path, List.rev l
-
(** get all global variables as (varinfo, initinfo) list with only one
occurrence of a varinfo *)
let get_globals path =
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index ecaa1a639af77ca4e75e652f7a15222004d17ee1..46d72094eb9539a39ec22c32c2dfb4d819ced3e5 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -185,12 +185,6 @@ module FileIndex : sig
(** All global C symbols of the given module.
@since Boron-20100401 *)
- val find : Datatype.Filepath.t -> Datatype.Filepath.t * global list
- [@@deprecated "Use FileIndex.get_symbols instead."]
- (** [find path] returns all global C symbols associated with [path],
- plus [path] itself. The returned [global] list is reversed.
- @deprecated 18.0-Argon use [get_symbols] instead. *)
-
val get_files: unit -> Datatype.Filepath.t list
(** Get the files list containing all [global] C symbols. *)
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index 0dbc5fed323e0e8c5b68528f94a8b40b21f1463d..5e1be0e3bc823de0d48cbd0bc8ffaf20230bff12 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 77c5e587c416d9f39bd7d5881a5644378f32b250..6d9f38b4c4eb2f6c042f597bdbeeab29ebbf9a24 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 887e1f154e495f50327fdcb4efd9ff9087feec3a..0bf1ce55ba3574589529ecb7fd605c308ce9000a 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 17c67011356f8414442a4cb73246944af38c8d70..d8ff44a66c4f7fcecd41018c40d44a4a0fe01af6 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 9413778ddbe3e79d27a575dabb02f63564c4904e..df6e83336874b7a7fd735a30a60fbf3bb0c214ff 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -69,7 +69,7 @@ val precondition : goal:bool -> funspec -> predicate
With [~goal:true], only returns assert and check predicates.
With [~goal:false], only returns assert and admit predicates.
@since Carbon-20101201
- @modify 23.0-Vanadium introduce [goal] flag
+ @before 23.0-Vanadium no [goal] flag.
*)
val behavior_assumes : funbehavior -> predicate
@@ -80,15 +80,14 @@ val behavior_precondition : goal:bool -> funbehavior -> predicate
(** Builds the precondition from [b_assumes] and [b_requires] clauses.
For flag [~goal] see {!Ast_info.precondition} above.
@since Carbon-20101201
- @modify 23.0-Vanadium introduce [goal] flag
+ @before 23.0-Vanadium no [goal] flag.
*)
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
+ @before 23.0-Vanadium no [goal] flag.
*)
val disjoint_behaviors : funspec -> string list -> predicate
@@ -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.ml b/src/kernel_services/ast_queries/cil.ml
index bf022633db1f6a546a8bf468044281657b8eb624..ed1d22069662f63a5336e00c980814240a001273 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6939,19 +6939,6 @@ let typeDeepDropAllAttributes t =
let vis = new dropAttributes () in
visitCilType vis t
-(** {1 Deprecated} *)
-
-let typeDeepDropAttributes =
- Kernel.deprecated "Cil.typeDeepDropAttributes"
- ~now:"Cil.typeRemoveAttributesDeep"
- (fun select t ->
- let vis = new dropAttributes ~select () in visitCilType vis t)
-
-let typeHasAttributeDeep t =
- Kernel.deprecated "Cil.typeHasAttributeDeep"
- ~now:"Cil.typeHasAttributeMemoryBlock"
- typeHasAttributeMemoryBlock t
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 52f580d316e9e9ed45f2ef4def06748e8afc773a..8d67ee88685af49156bd0db736a208211b7f8418 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
@@ -441,10 +440,10 @@ val isCompleteType: ?allowZeroSizeArrays:bool -> typ -> bool
@since 18.0-Argon
*)
val has_flexible_array_member: typ -> bool
-(** [true] iff the given type has flexible array member.
+(** [true] iff the given type has flexible array member, in GCC/MSVC mode, this
+ function mode recursively searches in the type of the last field.
- @modify 24.0-Chromium in GCC/MSVC mode recursively searches in the type of the
- last field.
+ @before 24.0-Chromium this function didn't take in account the GCC/MSVC mode
*)
(** Unroll a type until it exposes a non
@@ -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,20 +971,18 @@ 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
+ @before 23.0-Vanadium different order of arguments.
*)
val mkCastT: ?force:bool -> oldt:typ -> newt:typ -> exp -> exp
(** Like {!Cil.mkCastT} but uses typeOf to get [oldt]
- @modify 23.0-Vanadium change order or arguments
+ @before 23.0-Vanadium different order of arguments.
*)
val mkCast: ?force:bool -> 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 ->
@@ -1130,8 +1105,8 @@ val mkPureExpr:
(** Make a loop. Can contain Break or Continue.
The kind of loop (while, for, dowhile) is given by [sattr]
(none by default). Use {!Cil.mkWhile} for a While loop.
- @modify 23.0-Vanadium add unit argument. Default type is no longer While,
- use {!Cil.mkWhile} instead.
+ @before 23.0-Vanadium no unit argument, and default type was While
+ (for while loops, there is now {!Cil.mkWhile}).
*)
val mkLoop: ?sattr:attributes -> guard:exp -> body:stmt list -> unit ->
stmt list
@@ -1140,14 +1115,14 @@ val mkLoop: ?sattr:attributes -> guard:exp -> body:stmt list -> unit ->
can contain Break but not Continue. Can be used with i a pointer
or an integer. Start and done must have the same type but incr
must be an integer
- @modify 23.0-Vanadium add unit argument
+ @before 23.0-Vanadium did not have unit argument.
*)
val mkForIncr: ?sattr:attributes -> iter:varinfo -> first:exp -> stopat:exp ->
incr:exp -> body:stmt list -> unit -> stmt list
(** Make a for loop for(start; guard; next) \{ ... \}. The body can
contain Break but not Continue !!!
- @modify 23.0-Vanadium add unit argument
+ @before 23.0-Vanadium did not have unit argument.
*)
val mkFor: ?sattr:attributes -> start:stmt list -> guard:exp -> next: stmt list ->
body: stmt list -> unit -> stmt list
@@ -1304,17 +1279,6 @@ val isGhostFormalVarDecl: (string * typ * attributes) -> bool
*)
val isGlobalInitConst: varinfo -> bool
-(** Remove attributes whose name appears in the first argument that are
- present anywhere in the fully expanded version of the type.
- @since Oxygen-20120901
- @deprecated Chlorine-20180501 use {!Cil.typeRemoveAttributesDeep} instead,
- which does not traverse pointers and function types, or
- {!Cil.typeDeepDropAllAttributes}, which will give a pristine version of the
- type, without any attributes.
-*)
-val typeDeepDropAttributes: string list -> typ -> typ
-[@@ ocaml.deprecated "Use Cil.typeRemoveAttributesDeep"]
-
(** Remove any attribute appearing somewhere in the fully expanded
version of the type.
@since Oxygen-20120901
@@ -1387,14 +1351,6 @@ val typeHasQualifier: string -> typ -> bool
have array type.
@since Sodium-20150201 *)
-val typeHasAttributeDeep: string -> typ -> bool
-[@@ deprecated "Use Cil.typeHasAttributeMemoryBlock instead"]
-(** Does the type or one of its subtypes have the given attribute. Does
- not recurse through pointer types, nor inside function prototypes.
- @since Oxygen-20120901
- @deprecated Chlorine-20180501 see {!Cil.typeHasAttributeMemoryBlock}
-*)
-
val typeHasAttributeMemoryBlock: string -> typ -> bool
(** [typeHasAttributeMemoryBlock attr t] is
[true] iff at least one component of an object of type [t] has attribute
@@ -1934,7 +1890,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 +1964,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 +2160,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.ml b/src/kernel_services/ast_queries/cil_const.ml
index e5e57b1738d4a64a76e9f38265b59122ff589173..41ad002c8f3c36694caca652b57ee54f08b310b7 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -152,12 +152,6 @@ let make_logic_var_formal x t = make_logic_var_kind x LVFormal t
let make_logic_var_quant x t = make_logic_var_kind x LVQuant t
let make_logic_var_local x t = make_logic_var_kind x LVLocal t
-let make_logic_var =
- Kernel.deprecated "Cil_const.make_logic_var"
- ~now:"Use one of Cil_const.make_logic_var_* to indicate \
- the origin of the variable"
- make_logic_var_quant
-
let make_logic_info k x =
{ l_var_info = make_logic_var_kind x k (Ctype voidType);
(* we should put the right type when fields
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index 62d0b788fa40d1cd1c15cb4d5d82031d7828a542..bc7db0a6014b200a8c553af918149ded974959a4 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
@@ -109,12 +108,6 @@ val copyCompInfo: ?fresh:bool -> compinfo -> string -> compinfo
*)
val make_logic_var_kind : string -> logic_var_kind -> logic_type -> logic_var
-(** Create a fresh logical variable giving its name and type.
- @deprecated Fluorine-20130401 You should use a specific
- make_logic_var_[kind] function below, or {! Cil.cvar_to_lvar}
-*)
-val make_logic_var : string -> logic_type -> logic_var
-
(** Create a new global logic variable
@since Fluorine-20130401 *)
val make_logic_var_global: string -> logic_type -> logic_var
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index 51b50f029492710349cb2bbcbd8493186d7bb396..8042cf4420e9f471b83b2c6d9dc6ae000bd45e90 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 *)
@@ -148,7 +146,7 @@ val get_name: t -> string
val get_preprocessor_command: unit -> string
(** Return the preprocessor command to use.
- @modify 23.0-Vanadium return type now contains only the command
+ @before 23.0-Vanadium return type also contained cpp_opt_kind.
*)
val pre_register: t -> unit
@@ -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 908fda957556c8256582c4c201f44a64c9ac3ce6..65f5b195e09bbfcfcfafd420775ab81515503519 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.ml b/src/kernel_services/ast_queries/logic_const.ml
index 78fcbdb2cb8319794ccf435ec231bfba949dd8dd..8b0030707084d570c0765af217a5a9fe898789a8 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -268,11 +268,6 @@ let term ?(loc=Cil_datatype.Location.unknown) term typ =
term_name = [];
term_loc = loc }
-let taddrof ?(loc=Cil_datatype.Location.unknown) lv typ =
- match lv with
- | TMem h, TNoOffset -> h
- | _ -> term ~loc (TAddrOf lv) typ
-
(** range of integers *)
let trange ?(loc=Cil_datatype.Location.unknown) (low,high) =
term ~loc (Trange(low,high))
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 72cb93fb3b0461c228d31d7d7e265327dee538eb..1fc039f8df1bfa13787e8c3f71d030c3fd09b4b4 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -59,7 +59,8 @@ val refresh_spec: funspec -> funspec
val toplevel_predicate: ?kind:predicate_kind -> predicate -> toplevel_predicate
(** creates a new identified predicate with a fresh id.
- @modify 22.0-Titanium add [only_check] optional parameter
+ @before 22.0-Titanium no [only_check] parameter.
+ @before 23.0-Vanadium [kind] parameter was named [only_check].
*)
val new_predicate: ?kind:predicate_kind -> predicate -> identified_predicate
@@ -233,8 +234,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 +243,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 +284,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
(* ************************************************************************** *)
@@ -306,10 +297,6 @@ val boolean_type: logic_type
(** returns a anonymous term of the given type. *)
val term : ?loc:Location.t -> term_node -> logic_type -> term
-(** &
- @deprecated Neon-20130301 {!Logic_utils.mk_AddrOf} is easier to use.*)
-val taddrof: ?loc:Location.t -> term_lval -> logic_type -> term
-
(** [..] of integers *)
val trange: ?loc:Location.t -> term option * term option -> term
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index f9a791246133b23cd59af97a6de9523ccbdfe68a..ad5da768177477c5df00713c9a654c3231b3ddcf 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -33,12 +33,6 @@ exception Backtrack
let ($) = Extlib.($)
-let add_offset_lval =
- Kernel.deprecated
- "Logic_typing.add_offset_lval"
- ~now:"Logic_const.addTermOffsetLval"
- Logic_const.addTermOffsetLval
-
let loc_join (b,_) (_,e) = (b,e)
let unescape s = Logic_lexer.chr (Lexing.from_string s)
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 3ea227024a1f08a8a2387c7e183b9ff1d6524dd2..9a86583db31e9f56d1f8b9e70eed25b579e71ba8 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -60,11 +60,6 @@ val type_of_set_elem: logic_type -> logic_type
val ctype_of_pointed: logic_type -> typ
val ctype_of_array_elem: logic_type -> typ
-(**
- @deprecated Neon-20130301 use Logic_const.addTermOffsetLval instead
-*)
-val add_offset_lval: term_offset -> term_lval -> term_lval
-
val arithmetic_conversion:
Cil_types.logic_type -> Cil_types.logic_type -> Cil_types.logic_type
@@ -147,7 +142,7 @@ type typing_context = {
a text message indicating the issue) and the exception will be re-raised.
@since Chlorine-20180501
- @modify Frama-C+dev rollback takes as argument the error
+ @before Frama-C+dev [rollback] didn't take [loc] and [cause] as argument
*)
}
@@ -207,7 +202,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.ml b/src/kernel_services/ast_queries/logic_utils.ml
index c9775138c1983f756ddfe885a5cfe1115caf46ef..63f04f73e88fa0885d24c1401a9746ab15fc2bc7 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -129,8 +129,6 @@ let coerce_type typ =
else if Cil.isFloatingType ty then Lreal
else Ctype typ
-let predicate_of_identified_predicate ip = ip.ip_content.tp_statement
-
let translate_old_label s p =
let get_label () =
match s.labels with
@@ -874,8 +872,6 @@ let compare_logic_ctor_info ci1 ci2 =
else res
else res
-let is_same_constant = Cil.compareConstant
-
let is_same_pconstant c1 c2 =
let open Logic_ptree in
match c1, c2 with
@@ -2750,10 +2746,6 @@ end
let () = Cil_datatype.punrollLogicType := unroll_type
-(* ************************************************************************** *)
-(** {1 Deprecated} *)
-let instantiate = Logic_const.instantiate
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index ef79c06f510414ea50d57d1a24f4484cea12a90a..307d889ee9baf44ceba4c59e987148605fc3c068 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -41,12 +41,6 @@ val add_logic_function : logic_info -> unit
(** {2 Types} *)
-(** instantiate type variables in a logic type. *)
-val instantiate :
- (string * logic_type) list ->
- logic_type -> logic_type
-[@@deprecated "Use Logic_const.instantiate instead."]
-
(** [is_instance_of poly t1 t2] returns [true] if [t1] can be derived from [t2]
by instantiating some of the type variable in [poly].
@@ -67,7 +61,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 *)
@@ -92,10 +85,6 @@ val coerce_type : typ -> logic_type
(** {2 Predicates} *)
-(** @deprecated use Logic_const.pred_of_id_pred instead *)
-val predicate_of_identified_predicate: identified_predicate -> predicate
-[@@ deprecated "Use Logic_const.pred_of_id_pred instead"]
-
(** transforms \old and \at(,Old) into \at(,L) for L a label pointing
to the given statement, creating one if needed. *)
val translate_old_label: stmt -> predicate -> predicate
@@ -123,8 +112,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
@@ -146,7 +134,7 @@ val remove_logic_coerce: term -> term
set type.
@since Magnesium-20151001
- @modify 21.0-Scandium
+ @before 21.0-Scandium was ambiguous (coercion vs. conversion).
*)
val numeric_coerce: logic_type -> term -> term
@@ -179,7 +167,7 @@ val expr_to_term : ?coerce:bool -> exp -> term
To obtain a boolean or predicate, use [expr_to_boolean] or
[expr_to_predicate] instead.
- @modify 21.0-Scandium
+ @before 21.0-Scandium was unsound in many cases.
*)
val expr_to_predicate: exp -> predicate
@@ -192,7 +180,7 @@ val expr_to_predicate: exp -> predicate
@raise Fatal error if the expression is not a comparison and cannot be
compared to zero.
@since Sulfur-20171101
- @modify 21.0-Scandium
+ @before 21.0-Scandium was unsound in many cases.
*)
val expr_to_ipredicate: exp -> identified_predicate
@@ -204,7 +192,7 @@ val expr_to_ipredicate: exp -> identified_predicate
@raise Fatal error if the expression is not a comparison and cannot be
compared to zero.
@since Sulfur-20171101
- @modify 21.0-Scandium
+ @before 21.0-Scandium was unsound in many cases.
*)
val expr_to_boolean: exp -> term
@@ -217,7 +205,7 @@ val expr_to_boolean: exp -> term
@raise Fatal error if the expression is not a comparison and cannot be
compared to zero.
@since Sulfur-20171101
- @modify 21.0-Scandium
+ @before 21.0-Scandium was unsound in many cases.
*)
val is_zero_comparable: term -> bool
@@ -347,8 +335,6 @@ val is_same_builtin_profile :
val is_same_logic_ctor_info :
logic_ctor_info -> logic_ctor_info -> bool
-(** @deprecated Nitrogen-20111001 use {!Cil.compareConstant} instead. *)
-val is_same_constant : constant -> constant -> bool
val is_same_term : term -> term -> bool
val is_same_logic_info : logic_info -> logic_info -> bool
val is_same_logic_body : logic_body -> logic_body -> bool
@@ -434,7 +420,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 593030013953876e2785ddb547c7d7f07f623e52..572ee38ca0221df19644f0e79d27e961e1b6d87e 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 ->
@@ -323,7 +311,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 22.0-Titanium add [visible] and [deprecated] arguments. *)
+ @before 22.0-Titanium no [visible] and [deprecated] arguments. *)
val replace_option_setting:
string -> plugin:string -> group:Group.t -> option_setting -> unit
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.ml b/src/kernel_services/cmdline_parameters/parameter_customize.ml
index 5233a3bd0d9717c443f4df14654e9ea207da379c..26a72c9253e3a7803b76946e8c7ea78407175b02 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_customize.ml
@@ -54,13 +54,6 @@ let do_not_projectify () =
let empty_format = ("": (unit, Format.formatter, unit) format)
let optional_help_ref = ref empty_format
-let set_optional_help fmt = optional_help_ref := fmt
-let set_optional_help fmt =
- Cmdline.Kernel_log.deprecated
- "Plugin.set_optional_help"
- ~now:"<none>"
- set_optional_help
- fmt
let module_name_ref = ref empty_string
let set_module_name s = module_name_ref := s
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.mli b/src/kernel_services/cmdline_parameters/parameter_customize.mli
index 56cfa1694ff6256e82f2b8503b07dc5e086561fe..2d2d03cc876ed18a95b05afd0f0e1a012a1163dd 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_customize.mli
@@ -79,12 +79,6 @@ val set_unset_option_help: string -> unit
has not been called before. No default.
@since Fluorine-20130401 *)
-val set_optional_help: (unit, Format.formatter, unit) format -> unit
-(** Concatenate an additional description just after the default one.
- @since Beryllium-20090601-beta1
- @deprecated since Oxygen-20120901: directly use the help string
- instead. *)
-
val set_group: Cmdline.Group.t -> unit
(** Affect a group to the parameter.
@since Beryllium-20090901 *)
@@ -93,7 +87,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 +95,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
@@ -129,7 +122,7 @@ val is_reconfigurable: unit -> unit
only parameters corresponding to options registered at the
{!Cmdline.Configuring} stage are reconfigurable.
@since Nitrogen-20111001
- @modify 22.0-Titanium [do_iterate] renamed to [is_reconfigurable]
+ @before 22.0-Titanium this function was called [do_iterate].
*)
val is_not_reconfigurable: unit -> unit
@@ -137,7 +130,7 @@ val is_not_reconfigurable: unit -> unit
parameters corresponding to options registered at the
{!Cmdline.Configuring} stage are reconfigurable.
@since Nitrogen-20111001
- @modify 22.0-Titanium [do_iterate] renamed to [is_reconfigurable]
+ @before 22.0-Titanium this function was called [do_not_iterate].
*)
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 13e4e754a2d155a8a300913aae812136da1b67c1..b5558a5aa42f0b5a808ff2402cb2480d6afc9354 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -190,7 +190,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 22.0-Titanium add [visible] and [deprecated] arguments. *)
+ @before 22.0-Titanium no [visible] and [deprecated] arguments. *)
(**/**)
val is_set: unit -> bool
@@ -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 413cb1a91ff2b622f4f533f4de7bc8b30068b513..545f1cc5147c6b1775d3ebe31e3704ee5312346c 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.ml b/src/kernel_services/plugin_entry_points/db.ml
index 454c4e069fbc6ad467395384204082ad63382093..aa88f10322091cd8ea4672057d06ec95299aa840 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -970,13 +970,6 @@ module Properties = struct
mk_fun "Properties.Interp.to_result_from_pred"
end
- let add_assert emitter kf kinstr prop =
- Kernel.deprecated "Db.Properties.add_assert" ~now:"ACSL_importer plug-in"
- (fun () ->
- let interp_prop = !Interp.code_annot kf kinstr prop in
- Annotations.add_code_annot emitter kinstr interp_prop)
- ()
-
end
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index e595d96f0bc6d567de1e130b8a743a89c0f4d5ef..0c37f844ea026f80172eb505e9d567e5c5d63b7d 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} *)
@@ -782,16 +762,6 @@ module Properties : sig
end
- (** {3 Assertions} *)
-
- 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 71f0267fcfc3b9f3bbf3bcb234bde5b58b82ac11..ae7cb6424ba157e60f331e76f20496aa7a95b018 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.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 057ba6786496350a2e133b771f3ee7e68feccc7f..3ef630f87377615d376089c541fcb003c681f604 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -584,14 +584,6 @@ module Unicode = struct
r
end
-module UseUnicode = struct
- include Unicode
- let set = deprecated "UseUnicode.set" ~now:"Unicode.set" set
- let on = deprecated "UseUnicode.on" ~now:"Unicode.on" on
- let off = deprecated "UseUnicode.off" ~now:"Unicode.off" off
- let get = deprecated "UseUnicode.get" ~now:"Unicode.get" get
-end
-
let () = Parameter_customize.set_group messages
let () = Parameter_customize.do_not_projectify ()
let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 28f166f0a9e829e848fabb05321a332484a2a476..b58ecaa79ad262e327b13fb21811893d43e33080 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -294,10 +294,6 @@ end
(** Behavior of option "-unicode".
@plugin development guide *)
-module UseUnicode: Parameter_sig.Bool
-(** Behavior of option "-unicode"
- @deprecated since Nitrogen-20111001 use module {!Unicode} instead. *)
-
module Time: Parameter_sig.String
(** Behavior of option "-time" *)
@@ -339,7 +335,8 @@ module AstDiff: Parameter_sig.Bool
(** Behavior of option "-add-symbolic-path"
@since Neon-20140301
- @modify 23.0-Vanadium inversed argument order (now uses path:name) *)
+ @before 23.0-Vanadium argument order was inversed (name:path); now it is
+ (path:name). *)
module SymbolicPath: Parameter_sig.Filepath_map with type value = string
module FloatNormal: Parameter_sig.Bool
@@ -387,13 +384,13 @@ end
module Session_dir: Parameter_sig.Filepath
(** Directory in which session files are searched.
@since Neon-20140301
- @modify 23.0-Vanadium parameter type is now Filepath instead of string
+ @before 23.0-Vanadium parameter type was string instead of Filepath.
*)
module Config_dir: Parameter_sig.Filepath
(** Directory in which config files are searched.
@since Neon-20140301
- @modify 23.0-Vanadium parameter type is now Filepath instead of string
+ @before 23.0-Vanadium parameter type was string instead of Filepath.
*)
(* this stop special comment does not work as expected (and as explained in the
@@ -513,8 +510,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.ml b/src/kernel_services/plugin_entry_points/log.ml
index 3daac4379d69558c708f6e108cde453d3f0c1b00..932b1e506f5b33e817e62c0aa2d52f9f54c34776 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -847,8 +847,6 @@ sig
val is_debug_key_enabled: category -> bool
- val get_debug_keyset : unit -> category list
-
val register_warn_category: string -> warn_category
val is_warn_category: string -> bool
@@ -1221,11 +1219,6 @@ struct
name now ;
f x
- let get_debug_keyset =
- deprecated "Log.get_debug_key_set"
- ~now:"Log.get_all_categories"
- (fun () -> get_all_categories ())
-
let noprint _fmt = ()
let spynewline bol output buffer start length =
@@ -1275,11 +1268,6 @@ struct
end
-(* Deprecated -- backward compatibity only. *)
-let null = Pretty_utils.null
-let with_null = Pretty_utils.with_null
-let nullprintf = Pretty_utils.nullprintf
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index 72740f68e89e8842d5fa7b6c60ae5b4246d12f93..b2a2b5289f63e294a7aed91fb6c023545f0609f7 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
@@ -336,12 +326,6 @@ module type Messages = sig
@since Fluorine-20130401
*)
- val get_debug_keyset : unit -> category list
- (** Returns currently active keys
- @since Nitrogen-20111001
- @deprecated Fluorine-20130401 use get_debug_keys instead
- *)
-
val register_warn_category: string -> warn_category
val is_warn_category: string -> bool
@@ -443,7 +427,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 +438,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
@@ -470,24 +451,6 @@ val get_current_source : unit -> Filepath.position
val clean : unit -> unit
(** Flushes the last transient message if necessary. *)
-val null : formatter
-[@@ deprecated "Use 'Pretty_utils.null' instead"]
-(** Prints nothing.
- @since Beryllium-20090901
- @deprecated Chlorine-20180501 use {!Pretty_utils} instead. *)
-
-val nullprintf : ('a,formatter,unit) format -> 'a
-[@@ deprecated "Use 'Pretty_utils.nullprintf' instead"]
-(** Discards the message and returns unit.
- @since Beryllium-20090901
- @deprecated Chlorine-20180501 use {!Pretty_utils} instead. *)
-
-val with_null : (unit -> 'b) -> ('a,formatter,unit,'b) format4 -> 'a
-[@@ deprecated "Use 'Pretty_utils.with_null' instead"]
-(** Discards the message and call the continuation.
- @since Beryllium-20090901
- @deprecated Chlorine-20180501 use {!Pretty_utils} instead. *)
-
val set_output : ?isatty:bool -> (string -> int -> int -> unit) -> (unit -> unit) -> unit
(** This function has the same parameters as Format.make_formatter.
@since Beryllium-20090901
@@ -501,7 +464,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 +474,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.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index fad270e1c3e7f214042529ae3b42bbc5f8ca97eb..493cea1aaf76821266d0ebe68c52c132dbc5a7a5 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -36,7 +36,6 @@ let config_ref = Extlib.mk_fun "config_ref"
module type S_no_log = sig
val add_group: ?memo:bool -> string -> Cmdline.Group.t
- module Help: Parameter_sig.Bool
module Verbose: Parameter_sig.Int
module Debug: Parameter_sig.Int
module Share: Parameter_sig.Specific_dir
@@ -91,9 +90,6 @@ let plugin_subpath s = plugin_subpath_ref := Some s
let default_msg_keys_ref = ref []
-let default_msg_keys l = default_msg_keys_ref := l
-[@@ deprecated "Manage msg keys with Log interface"]
-
let reset_plugin () =
kernel := false;
share_visible_ref := false;
@@ -132,10 +128,6 @@ let fold_on_plugins (f : (plugin -> 'a -> 'a)) (acc : 'a) : 'a =
let is_present s = List.exists (fun p -> p.p_shortname = s) !plugins
let get_from_name s = List.find (fun p -> p.p_name = s) !plugins
let get_from_shortname s = List.find (fun p -> p.p_shortname = s) !plugins
-let get s =
- Cmdline.Kernel_log.deprecated
- "Plugin.get" ~now:"Plugin.get_from_name" get_from_name s
-[@@ deprecated "Use Plugin.get_from_name"]
(* ************************************************************************* *)
(** {2 Global data structures} *)
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index da7d795389d76899763eb37e2670329f8d149f15..0851fea085914da838db93143510ee60324ed74b 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -38,9 +38,6 @@ module type S_no_log = sig
[memo] defaults to [false]
@since Beryllium-20090901 *)
- module Help: Parameter_sig.Bool
- (** @deprecated since Oxygen-20120901 *)
-
module Verbose: Parameter_sig.Int
module Debug: Parameter_sig.Int
@@ -71,13 +68,12 @@ module type S_no_log = sig
[add_plugin_output_aliases [alias]] adds the aliases -alias-help,
-alias-verbose, etc.
@since 18.0-Argon
- @modify 22.0-Titanium add [visible] and [deprecated] arguments. *)
+ @before 22.0-Titanium no [visible] and [deprecated] arguments.
+ *)
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
@@ -90,8 +86,8 @@ type plugin = private
p_help: string;
p_parameters: (string, Typed_parameter.t list) Hashtbl.t }
(** @since Beryllium-20090901
- @modify 22.0-Titanium previously only "iterable" parameters were included,
- now all parameters are.
+ @before 22.0-Titanium only "iterable" parameters were included;
+ now all parameters are.
*)
module type General_services = sig
@@ -144,14 +140,6 @@ val plugin_subpath: string -> unit
directories [Share], [Session] and [Config] above.
@since Neon-20140301 *)
-val default_msg_keys: string list -> unit
-(** Debug message keys set by default for the plugin.
- @since Silicon-20161101
- @deprecated since Chlorine-20180501 use directly functions from Log
- (add_debug_keys and del_debug_keys) to manage the default status of each
- category
-*)
-
(* ************************************************************************* *)
(** {2 Handling plugins} *)
(* ************************************************************************* *)
@@ -169,11 +157,6 @@ val is_present: string -> bool
Plugins are identified by their short name.
@since Magnesium-20151001 *)
-val get: string -> plugin
-[@@ deprecated "Use Plugin.get_from_name"]
-(** Get a plug-in from its name.
- @deprecated since Oxygen-20120901 *)
-
val iter_on_plugins: (plugin -> unit) -> unit
(** Iterate on each registered plug-in.
@since Beryllium-20090901 *)
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 34026478a1a927da4afaf3547b4eb8731d96f1a9..fb520585b8f4155b5c48fc2210699e5c7f033c87 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -340,10 +340,6 @@ val string: string Type.t
module Formatter: S with type t = Format.formatter
val formatter: Format.formatter Type.t
-(* module Big_int: S_with_collections with type t = Integer.t *)
-(* val big_int: Big_int.t Type.t *)
-(** @deprecated use Integer instead. *)
-
module Integer: S_with_collections with type t = Integer.t
val integer: Integer.t Type.t
diff --git a/src/libraries/datatype/structural_descr.mli b/src/libraries/datatype/structural_descr.mli
index 2d71998405649ad9f2755a880eed56c195830da2..ff1106d9e5902956e1636f8bd0d578d813372021 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 0cc7b1ff57f7b15825f0d3d5345f128eb616e94d..cf324f26944eb0cf20340eb7424cbb243dcd2a0f 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 47d055df191824a5b9f2dd30413e873997d7a04b..fd9f1db82879143f6a5c4e248924fe4124cff279 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 2f2bc82b2f0ecd9a3797d4223a729bd81f1cd723..cc8bbff434a8554900d9beb62461e2d1e2de79e4 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 fbcfb611dedcd1f455444bd07712f0f702b2d183..15b0fe12ff2369fe4cfc40107615e50341db6023 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.ml b/src/libraries/stdlib/extlib.ml
index 0041598a6571d5898fef1213033c9eba880bfa6c..c83b934e6631ce49d57b217bf7dd79352cba1269 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -169,13 +169,6 @@ let opt_of_list =
| [a] -> Some a
| _ -> raise (Invalid_argument "Extlib.opt_of_list")
-let rec find_opt f = function
- | [] -> raise Not_found
- | e :: q ->
- match f e with
- | None -> find_opt f q
- | Some v -> v
-
let iteri f l = let i = ref 0 in List.iter (fun x -> f !i x; incr i) l
let mapi f l =
@@ -183,8 +176,6 @@ let mapi f l =
snd (List.fold_left (fun (i,acc) x -> (i+1,f i x :: acc)) (0,[]) l)
in List.rev res
-let sort_unique cmp l = List.sort_uniq cmp l
-
let subsets k l =
let rec aux k l len =
if k = 0 then [[]]
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index d8551183ffe17a263faf75b9e971f34c7c69fc2f..6eac85cefbcefc87840ff81837a86325286a7e01 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -148,15 +148,6 @@ val opt_of_list: 'a list -> 'a option
@raise Invalid_argument on lists with more than one argument
@since Oxygen-20120901 *)
-val find_opt : ('a -> 'b option) -> 'a list -> 'b
-[@@deprecated "Use List.find_opt instead."]
-(** [find_option p l] returns the value [p e], [e] being the first
- element of [l] such that [p e] is not [None]. Raise [Not_found] if there
- is no such value the list l.
-
- @since Nitrogen-20111001
- @deprecated 18.0-Argon use [List.find_opt] instead *)
-
val iteri: (int -> 'a -> unit) -> 'a list -> unit
(** Same as iter, but the function to be applied take also as argument the
index of the element (starting from 0). Tail-recursive
@@ -167,11 +158,6 @@ val mapi: (int -> 'a -> 'b) -> 'a list -> 'b list
index of the element (starting from 0). Tail-recursive
@since Oxygen-20120901 *)
-val sort_unique: ('a -> 'a -> int) -> 'a list -> 'a list
-(** Same as List.sort , but also remove duplicates.
- @deprecated use List.sort_uniq instead
-*)
-
val subsets: int -> 'a list -> 'a list list
(** [subsets k l] computes the combinations of [k] elements from list [l].
E.g. subsets 2 [1;2;3;4] = [[1;2];[1;3];[1;4];[2;3];[2;4];[3;4]].
@@ -222,9 +208,7 @@ 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.
+ @before 23.0-Vanadium [exn] was an optional argument.
@plugin development guide *)
val opt_hash: ('a -> int) -> 'a option -> int
@@ -345,14 +329,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/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 33ec8281a3a85c2e36b1690ac67a444cdb485cb6..835c3fd4268c9caf3eb258c157e6c90a9004504e 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -214,10 +214,15 @@ val to_string : t -> string
val of_string : string -> t
(** @raise Invalid_argument when the string cannot be parsed. *)
-(** @modify Frama-C+dev remove optional `hexa` argument *)
+(** Prints the integer in decimal format. See also {!pretty_hex}.
+
+ @before Frama-C+dev there was an optional [hexa] argument. *)
val pretty : t formatter
-(** @since Frama-C+dev *)
+(** Prints the integer in hexadecimal format (replaces [hexa] optional
+ argument of {!pretty} from older versions).
+
+ @since Frama-C+dev *)
val pretty_hex : t formatter
val pp_bin : ?nbits:int -> ?sep:string -> t formatter
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index 52645e14bd181810e376fd56c345fee907de3e54..7863d6e262e83a8fdd1feff875263fdf6b727809 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 1f3de6c270500d72aca8b2058b5aef77a2ba48fb..ac31e18e9d1602df4a494e1fde3d8a680fc7f9a5 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -49,8 +49,7 @@ 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.
+ @before 21.0-Scandium no [existence] argument.
*)
val normalize: ?existence:existence -> ?base_name:string -> string -> string
@@ -71,7 +70,7 @@ module Normalized: sig
(** [of_string s] converts [s] into a normalized path.
@raise Invalid_argument if [s] is the empty string.
- @modify 21.0-Scandium add optional existence parameter.
+ @before 21.0-Scandium no [existence] argument.
*)
val of_string: ?existence:existence -> ?base_name:string -> string -> t
@@ -170,7 +169,7 @@ end
(that is, it is prefixed by [base_name]), or to the current
working directory if no base is specified.
@since Aluminium-20160501
- @modify 23.0-Vanadium argument types changed from string to Normalized.t
+ @before 23.0-Vanadium argument types were string instead of Normalized.t.
*)
val is_relative: ?base_name:Normalized.t -> Normalized.t -> bool
diff --git a/src/libraries/utils/hook.mli b/src/libraries/utils/hook.mli
index 5ceb0c52335cb7630a60f6237c175d805dce0ac8..519c5bad69c30beb63b6a09d68f70e6420063215 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.ml b/src/libraries/utils/pretty_utils.ml
index 9d53c5b454227b46247659b7150bde3b84be3d64..53b7cbb1a7cafbf79141a60706b6a73b82d502e8 100644
--- a/src/libraries/utils/pretty_utils.ml
+++ b/src/libraries/utils/pretty_utils.ml
@@ -29,8 +29,6 @@ let ksfprintf f fmt =
let return fmt = Format.pp_print_flush fmt (); f (Buffer.contents b) in
Format.kfprintf return (Format.formatter_of_buffer b) fmt
-let sfprintf = Format.asprintf
-
let to_string ?margin pp x =
let b = Buffer.create 20 in
let f = Format.formatter_of_buffer b in
diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index 1434abb59f7609ebc978c098e5fef779d422146c..9520988353c06d43fb3e27b64638c83a59ac0fa0 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -43,10 +43,6 @@ val with_null : (unit -> 'b) -> ('a,Format.formatter,unit,'b) format4 -> 'a
(** {2 pretty-printing to a string} *)
(* ********************************************************************** *)
-val sfprintf: ('a,Format.formatter,unit,string) format4 -> 'a
-(** Equivalent to Format.asprintf. Used for compatibility with OCaml < 4.01.
- @deprecated Silicon-20161101 use Format.asprintf *)
-
val ksfprintf:
(string -> 'b) -> ('a, Format.formatter, unit, 'b) format4 -> 'a
(** similar to Format.kfprintf, but the continuation is given the result
@@ -82,8 +78,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 +87,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 +113,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.ml b/src/plugins/aorai/aorai_utils.ml
index 0a4289a46b76496213cbdc5aca302fcb21576349..93c470161d88005c3f0c528537f4cc785ed273a4 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -753,13 +753,6 @@ let mk_gvar_enum ?init name name_enuminfo =
(** Return an integer constant term from the given value. *)
let mk_int_term value = Cil.lconstant (Integer.of_int value)
-(** Return an integer constant term with the 0 value.
- @deprecated use directly Cil.lzero
-*)
-let zero_term() = Cil.lzero ()
-
-let one_term () = Cil.lconstant Integer.one
-
(** Returns a term representing the variable associated to the given varinfo *)
let mk_term_from_vi vi =
Logic_const.term
@@ -819,7 +812,7 @@ let is_state_pred state =
Logic_const.prel (Req,state_term(),int2enumstate state.nums)
else
Logic_const.prel
- (Req,one_term(),
+ (Req,Cil.lone (),
Logic_const.tvar (Data_for_aorai.get_state_logic_var state))
let is_state_non_det_stmt (_,copy) loc =
@@ -847,7 +840,7 @@ let is_out_of_state_pred state =
Logic_const.prel (Rneq,state_term(),int2enumstate state.nums)
else
Logic_const.prel
- (Req,zero_term(),
+ (Req,Cil.lzero (),
Logic_const.tvar (Data_for_aorai.get_state_logic_var state))
(* In the deterministic case, we only assign the unique state variable
diff --git a/src/plugins/aorai/aorai_utils.mli b/src/plugins/aorai/aorai_utils.mli
index 381dbcb2d493dfdb65f7a607a623a4a0e23a9583..25407680af310b2523b6922269a432c9470ab509 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,15 +178,11 @@ 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 ->
Data_for_aorai.state -> predicate list
-(** Return an integer constant term with the 0 value. *)
-val zero_term : unit -> Cil_types.term
-
(** Given an lval term 'host' and an integer value 'off', it returns a lval term host[off]. *)
val mk_offseted_array : Cil_types.term_lval -> int -> Cil_types.term
val mk_offseted_array_states_as_enum :
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 081427844d371f4ca0640d49ddb31a73004d6148..a64b4387b31e62061893af26c137382d65bda1df 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -1028,7 +1028,7 @@ class visit_adding_pre_post_from_buch treatloops =
pimplies
(prel(operator,
Aorai_utils.mk_term_from_vi vi_init,
- Aorai_utils.zero_term()),
+ Cil.lzero()),
predicate)
in
(* The loop invariant is :
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 96f4b22d28ff03e4d2913087d47212a6109d2fa9..2fb166151250623148259f3b087a508891f3ef4c 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -823,14 +823,14 @@ let type_expr metaenv env ?tr ?current e =
"Invalid operand for bitwise not: unexpected %a" Printer.pp_term t
| PUnop(Logic_ptree.Uamp,e) ->
let env, t, cond = aux env cond e in
- let ptr =
- try Ctype (TPtr (Logic_utils.logicCType t.term_type,[]))
- with Failure _ ->
- Aorai_option.abort "Cannot take address: not a C type(%a): %a"
- Printer.pp_logic_type t.term_type Printer.pp_term t
- in
(match t.term_node with
- | TLval v | TStartOf v -> env, Logic_const.taddrof v ptr, cond
+ | TLval v | TStartOf v ->
+ begin try
+ env, Logic_utils.mk_logic_AddrOf v t.term_type, cond
+ with Failure _ ->
+ Aorai_option.abort "Cannot take address: not a C type(%a): %a"
+ Printer.pp_logic_type t.term_type Printer.pp_term t
+ end
| _ ->
Aorai_option.abort "Cannot take address: not an lvalue %a"
Printer.pp_term t
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 28c79c7a0fd5a49a619817597983744a2cf08252..5e7c6b27d43866895b1a93aad79263d56a319013 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -367,13 +367,14 @@ let extract_quantifiers ~loc args =
eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers
in
let lty_noset =
+ Logic_typing.type_of_pointed @@
if Logic_const.is_set_type arg.term_type then
Logic_const.type_of_element arg.term_type
else
arg.term_type
in
let arg' =
- Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset
+ Logic_utils.mk_logic_AddrOf ~loc (TVar lv, toffset') lty_noset
in
arg', quantifiers'
with Range_elimination_exception ->
diff --git a/src/plugins/gui/design.mli b/src/plugins/gui/design.mli
index ae4018e81bf4f4fac9d8d4cb6cac0932494c5d4a..e833a41927ad1ad20372d8e3bd8e03ef4ad81347 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 654a47bae14a9a036dcff42ada7fea8a550fb273..b0dc9a0d1535d10ced36751dbeb0c3907ae290a1 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 34c05fad0767b5bac34c87c041d1fad594efe36a..8cf09cb23d1d209f0371b51cd673904114e636a8 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 aff7abcebf2a0bc69907af6fcbfda29ca8ae89cd..0c65bdfc6c5f8cb0ac63c41fb9f749e664a6f02e 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/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml
index dbecd7887f93d798f55858a988d443fbdb78f377..60001c8cb08e1a278abb7728942d23836dcc38b0 100644
--- a/src/plugins/instantiate/stdlib/calloc.ml
+++ b/src/plugins/instantiate/stdlib/calloc.ml
@@ -65,7 +65,8 @@ let pinitialized_len ?loc alloc_type num size =
let result = tresult ?loc (ptr_of alloc_type) in
let initialized ?loc t =
let t = match t.term_node, Logic_utils.unroll_type t.term_type with
- | TLval (lv), Ctype t -> taddrof ?loc lv (Ctype (ptr_of t))
+ | TLval (lv), (Ctype _ as t) ->
+ Logic_utils.mk_logic_AddrOf ?loc lv t
| _ -> unexpected "non lvalue or non c-type during initialized generation"
in
pinitialized ?loc (here_label, t)
diff --git a/src/plugins/qed/logic.mli b/src/plugins/qed/logic.mli
index a59161af28f80b0b0239375df045a90820d706bb..f481bf9030c29a002df93d1d4996e8d67236adfe 100644
--- a/src/plugins/qed/logic.mli
+++ b/src/plugins/qed/logic.mli
@@ -280,12 +280,6 @@ sig
type path = int list (** position of a subterm in a term. *)
- val subterm: term -> path -> term
- [@@deprecated "Path-access might be unsafe in presence of binders"]
-
- val change_subterm: term -> path -> term -> term
- [@@deprecated "Path-access might be unsafe in presence of binders"]
-
(** {3 Basic constructors} *)
val e_true : term
@@ -336,9 +330,6 @@ sig
(** Bind the given variable if it appears free in the term,
or return the term unchanged. *)
- val lc_open : var -> lc_term -> term
- [@@deprecated "Use e_unbind instead"]
-
val e_unbind : var -> lc_term -> term
(** Opens the top-most bound variable with a (fresh) variable.
Can be only applied on top-most lc-term from `Bind(_,_,_)`,
@@ -460,7 +451,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 22.0-Titanium add optional [force] parameter
+ @before 22.0-Titanium the optional [force] parameter does not exist
*)
val set_builtin' :
@@ -476,7 +467,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 22.0-Titanium add optional [force] parameter
+ @before 22.0-Titanium the optional [force] parameter does not exist
*)
val set_builtin_get :
@@ -488,7 +479,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 22.0-Titanium add optional [force] parameter
+ @before 22.0-Titanium the optional [force] parameter does not exist
*)
val set_builtin_eq :
@@ -503,7 +494,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 22.0-Titanium add optional [force] parameter
+ @before 22.0-Titanium the optional [force] parameter does not exist
*)
val set_builtin_leq :
@@ -519,7 +510,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 22.0-Titanium add optional [force] parameter
+ @before 22.0-Titanium the optional [force] parameter does not exist
*)
(** {3 Specific Patterns} *)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 59274b0b72d622d0fd2904445ba60229bc7ef73e..188886fc5ff3f2e249a3c361f148555afab81d7d 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -910,23 +910,6 @@ struct
let insert _ = assert false (* [insert] should not be used afterwards *)
[@@@ warning "+32"]
- let rec subterm e = function
- [] -> e
- | n :: l ->
- let children = match e.repr with
- | True | False | Kint _ | Kreal _ | Bvar _ | Fvar _ -> []
- | Times (n,e) -> [ e_zint n; e]
- | Add l | Mul l | And l | Or l | Fun (_,l) -> l
- | Div (e1,e2) | Mod (e1,e2) | Eq(e1,e2) | Neq(e1,e2)
- | Leq (e1,e2) | Lt(e1,e2) | Aget(e1,e2) -> [e1;e2]
- | Not e | Bind(_,_,e) | Acst(_,e) -> [e]
- | Imply(l,e) -> l @ [e]
- | If(e1,e2,e3) | Aset(e1,e2,e3) -> [e1;e2;e3]
- | Rget(e,_) -> [e]
- | Rdef fxs -> List.map snd fxs
- | Apply(e,es) -> e::es
- in subterm (List.nth children n) l
-
let is_primitive e =
match e.repr with
| True | False | Kint _ | Kreal _ -> true
@@ -2586,89 +2569,6 @@ struct
let e_fun ?result f xs = e_fungen f xs result
- (* -------------------------------------------------------------------------- *)
- (* --- Sub-terms --- *)
- (* -------------------------------------------------------------------------- *)
-
- let change_subterm e pos child =
- let bad_position () = failwith "cannot replace subterm at given position" in
- let rec change_in_list children cur_pos rest =
- match children, cur_pos with
- | [], _ -> bad_position ()
- | e::l, 0 -> (aux e rest) :: l
- | e::l, n -> e :: (change_in_list l (n-1) rest)
- (* since all repr might be shared, better work on an immutable copy than
- on the original array.
- *)
- and aux e pos =
- match pos with
- [] -> child
- | i::l -> begin
- match e.repr with
- | True | False | Kint _ | Kreal _ | Fvar _ | Bvar _ ->
- bad_position ()
- | Times (_,e) when i = 0 && l = [] ->
- begin
- match child.repr with
- Kint n -> times n e
- | _ -> e_mul child e
- end
- | Times(n,e) when i = 1 -> times n (aux e l)
- | Times _ -> bad_position ()
- | Add ops -> e_sum (change_in_list ops i l)
- | Mul ops -> e_prod (change_in_list ops i l)
- | Div (e1,e2) when i = 0 -> e_div (aux e1 l) e2
- | Div (e1,e2) when i = 1 -> e_div e1 (aux e2 l)
- | Div _ -> bad_position ()
- | Mod (e1,e2) when i = 0 -> e_mod (aux e1 l) e2
- | Mod (e1,e2) when i = 1 -> e_mod e1 (aux e2 l)
- | Mod _ -> bad_position ()
- | Eq (e1,e2) when i = 0 -> e_eq (aux e1 l) e2
- | Eq (e1,e2) when i = 1 -> e_eq e1 (aux e2 l)
- | Eq _ -> bad_position ()
- | Neq (e1,e2) when i = 0 -> e_neq (aux e1 l) e2
- | Neq (e1,e2) when i = 1 -> e_neq e1 (aux e2 l)
- | Neq _ -> bad_position ()
- | Leq (e1,e2) when i = 0 -> e_leq (aux e1 l) e2
- | Leq (e1,e2) when i = 1 -> e_leq e1 (aux e2 l)
- | Leq _ -> bad_position ()
- | Lt (e1,e2) when i = 0 -> e_lt (aux e1 l) e2
- | Lt (e1,e2) when i = 1 -> e_lt e1 (aux e2 l)
- | Lt _ -> bad_position ()
- | Acst (k,v) when i = 0 -> e_const k v
- | Acst _ -> bad_position ()
- | Aget (e1,e2) when i = 0 -> e_get (aux e1 l) e2
- | Aget (e1,e2) when i = 1 -> e_get e1 (aux e2 l)
- | Aget _ -> bad_position ()
- | And ops -> e_and (change_in_list ops i l)
- | Or ops -> e_or (change_in_list ops i l)
- | Not e when i = 0 -> e_not (aux e l)
- | Not _ -> bad_position ()
- | Imply(ops,e) ->
- let nb = List.length ops in
- if i < nb then e_imply (change_in_list ops i l) e
- else if i = nb then e_imply ops (aux e l)
- else bad_position ()
- | If(e1,e2,e3) when i = 0 -> e_if (aux e1 l) e2 e3
- | If(e1,e2,e3) when i = 1 -> e_if e1 (aux e2 l) e3
- | If(e1,e2,e3) when i = 2 -> e_if e1 e2 (aux e3 l)
- | If _ -> bad_position ()
- | Aset(e1,e2,e3) when i = 0 -> e_set (aux e1 l) e2 e3
- | Aset(e1,e2,e3) when i = 1 -> e_set e1 (aux e2 l) e3
- | Aset(e1,e2,e3) when i = 2 -> e_set e1 e2 (aux e3 l)
- | Aset _ -> bad_position ()
- | Rdef _ | Rget _ ->
- failwith "change in place for records not yet implemented"
- | Fun (f,ops) -> e_fungen f (change_in_list ops i l) e.tau
- | Bind(q,x,t) when i = 0 -> c_bind q x (aux t l)
- | Bind _ -> bad_position ()
- | Apply(f,args) when i = 0 ->
- e_apply (aux f l) args
- | Apply (f,args) ->
- e_apply f (change_in_list args i l)
- end
- in aux e pos
-
let () = pretty_debug := debug
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/report/csv.ml b/src/plugins/report/csv.ml
index ad65b15419b50c99538dbb545db6d7bded011840..2ed83a86b0a0f81a85364ad77bcfccf153d44a4b 100644
--- a/src/plugins/report/csv.ml
+++ b/src/plugins/report/csv.ml
@@ -66,7 +66,7 @@ let lines () =
emitted on statements copied through loop unrolling. This is the desired
semantics for now. However, since we compare entire locations, textually
identical lines that refer to different expressions are kept separate *)
- Extlib.sort_unique Stdlib.compare l
+ List.sort_uniq Stdlib.compare l
let output file =
let ch = open_out file in
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index dce2cdd9512711ca3a9da433c35d8381edb2310c..479ed60f40766d58b89b0f80a9f57b1c5ef50e40 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -25,9 +25,6 @@
open Cil_types
-let cat_rm_asserts_name = "rm_asserts"
-let () = Plugin.default_msg_keys [cat_rm_asserts_name]
-
let name = "scope"
module R =
@@ -38,7 +35,8 @@ module R =
let help = "data dependencies higher level functions"
end)
-let cat_rm_asserts = R.register_category cat_rm_asserts_name
+let cat_rm_asserts = R.register_category "rm_asserts"
+let () = R.add_debug_keys cat_rm_asserts
(** {2 Computing a mapping between zones and modifying statements}
We first go through all the function statements in other to build
diff --git a/src/plugins/slicing/Slicing.mli b/src/plugins/slicing/Slicing.mli
index fb4dda8b2f6efbdfd7089b4a51d07c1ce9b7b53b..3b17ef709fdb50f3f6dc147f12c5f42151d6542f 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 bba2afb4077e1b3c97f97c1bf787a860faa1d2d5..b489bb90605a8bc465dc42b3ac37f82ca83ed428 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 079e468002f8bf311c3bb758cf65f5aa15782f93..2f2b503634d6963779eee23c1ec856c8e0aa4222 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 01757a9ab0851e3f2418fc598dddb1c32f473dd9..6a325cc662e75fb7071ab6519e1dce221bc0eed8 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. *)
diff --git a/src/plugins/value/self.ml b/src/plugins/value/self.ml
index 430ed2dfde6c190fe6d58c1fca3c4af01cadfcf1..cf109376c8d05157ea5bf5e21d2d9e153e99658e 100644
--- a/src/plugins/value/self.ml
+++ b/src/plugins/value/self.ml
@@ -28,8 +28,8 @@ include Plugin.Register
"automatically computes variation domains for the variables of the program"
end)
-let () = Help.add_aliases ~visible:false [ "-value-h"; "-val-h" ]
-let () = add_plugin_output_aliases ~visible:false ~deprecated:true [ "value" ]
+let () =
+ add_plugin_output_aliases ~visible:false ~deprecated:true [ "value" ; "val" ]
(* Do not add dependencies to Kernel parameters here, but at the top of
Parameters. *)
diff --git a/src/plugins/value_types/widen_type.ml b/src/plugins/value_types/widen_type.ml
index 2af4ed266e7f5f2460c0827afd4bb9cd4ae1c215..c486eda25e387f53e331b4b40459d388d3f2050e 100644
--- a/src/plugins/value_types/widen_type.ml
+++ b/src/plugins/value_types/widen_type.ml
@@ -128,7 +128,7 @@ let pretty fmt wh =
Format.fprintf fmt "%a" (pp_bindings Base.pretty pp_elt) (Base.Map.bindings m)
in
let pp_stmt fmt stmt =
- let stmt_str = Pretty_utils.sfprintf "%a" Stmt.pretty stmt in
+ let stmt_str = Format.asprintf "%a" Stmt.pretty stmt in
let len = String.length stmt_str in
Format.fprintf fmt "[sid:%d<%s>]" stmt.Cil_types.sid
(if len < 10 then stmt_str else String.sub stmt_str 0 10 ^ "...")
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index dc7936786aa9dd36a3146bfe9b8033c9989292b9..b13a16a59b802d03e3210c8f613d390e9da47ee3 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -332,8 +332,8 @@ module Compute = WpContext.StaticGenerator
let name = op_name op in
let phi = match op with
| LT | EQ | LE | NE ->
- let prop = Pretty_utils.sfprintf "%s_%a" name pp_suffix ft in
- let bool = Pretty_utils.sfprintf "%s_%ab" name pp_suffix ft in
+ let prop = Format.asprintf "%s_%a" name pp_suffix ft in
+ let bool = Format.asprintf "%s_%ab" name pp_suffix ft in
extern_p ~library ~bool ~prop ()
| _ ->
let result = return_type ft op in
diff --git a/src/plugins/wp/Footprint.ml b/src/plugins/wp/Footprint.ml
index 8111979b297bc8f548f068e833fd30659fe16817..0768281a8967dff0937d8aa6a88a8ccda54acf41 100644
--- a/src/plugins/wp/Footprint.ml
+++ b/src/plugins/wp/Footprint.ml
@@ -82,8 +82,8 @@ let head e =
| Aget _ -> "[]"
| Acst _ -> "[.]"
| Aset _ -> "[=]"
- | Rget(_,fd) -> Pretty_utils.sfprintf ".%a" Lang.Field.pretty fd
- | Rdef fds -> Pretty_utils.sfprintf "{%s}" (head_fields fds)
+ | Rget(_,fd) -> Format.asprintf ".%a" Lang.Field.pretty fd
+ | Rdef fds -> Format.asprintf "{%s}" (head_fields fds)
| Fun(f,_) -> Pretty_utils.to_string Lang.Fun.pretty f
| Apply _ -> "()"
| Bind(Forall,_,_) -> "\\F"
diff --git a/src/plugins/wp/GuiTactic.ml b/src/plugins/wp/GuiTactic.ml
index 3d96eecd618867c225d159bc38776d99ba7cd99c..1b55cb72197980d47abf7eb2886491953d604f9a 100644
--- a/src/plugins/wp/GuiTactic.ml
+++ b/src/plugins/wp/GuiTactic.ml
@@ -158,7 +158,7 @@ class mkcomposer
Pretty_utils.ksfprintf head#set_text "%s: -" wtitle
| value ->
let text =
- Pretty_utils.sfprintf "@[<hov 2>%s: %a@]" wtitle pp value in
+ Format.asprintf "@[<hov 2>%s: %a@]" wtitle pp value in
let msg =
if String.length text <= 20 then text else
String.sub text 0 17 ^ "..." in
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 9587d9eac5de4175c7f3de5b56c764c3d86d818e..2f0396b4d33dab2df87dde6d0ff01f22d1164b09 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -149,7 +149,7 @@ struct
[ (Trigger.of_term value1 :: triggers );
(Trigger.of_term value2 :: triggers ) ]
in
- let l_name = Pretty_utils.sfprintf "%s_%s_%s%d"
+ let l_name = Format.asprintf "%s_%s_%s%d"
prefix name (Chunk.basename_of_chunk chunk) i in
let l_lemma = F.p_hyps conditions (p_equal value1 value2) in
Definitions.define_lemma {
diff --git a/src/plugins/wp/RegionDump.ml b/src/plugins/wp/RegionDump.ml
index acd421a0e7baeeb4c3a85f9066ae7cfbe8973a9b..b2dd992a2fc4072523cec566a98c2383e888e83a 100644
--- a/src/plugins/wp/RegionDump.ml
+++ b/src/plugins/wp/RegionDump.ml
@@ -68,7 +68,7 @@ let cluster_key = Wp.register_category "cluster"
let chunk_key = Wp.register_category "chunk"
let offset_key = Wp.register_category "offset"
-let sfprintf = Pretty_utils.sfprintf
+let sfprintf = Format.asprintf
let dotpointed ~label r =
let attr =
diff --git a/src/plugins/wp/TacCompound.ml b/src/plugins/wp/TacCompound.ml
index 7c02f932f1b4a1cc615244a1f963d9c7d154bfbe..42657be9b5df68c07a30ce5d0e92d4eb91b38697 100644
--- a/src/plugins/wp/TacCompound.ml
+++ b/src/plugins/wp/TacCompound.ml
@@ -113,7 +113,7 @@ let get_compound_equality e =
(* -------------------------------------------------------------------------- *)
let field a b f =
- Pretty_utils.sfprintf "Field %a" Lang.Field.pretty f ,
+ Format.asprintf "Field %a" Lang.Field.pretty f ,
F.p_equal (F.e_getfield a f) (F.e_getfield b f)
let index ~pool tau =
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index e66d3b23e05354fe9527c633aad8c5112abdf927..3c06882c26ddcfa79837a05c468dd09b691b0e47 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -135,7 +135,7 @@ let filter tau e =
with Not_found -> true (* allowed to not restrict usage *)
let fieldname ~range k x =
- Pretty_utils.sfprintf "%s (%a)%t"
+ Format.asprintf "%s (%a)%t"
(descr k) F.Tau.pretty (F.tau_of_var x)
(fun fmt -> if range then Format.pp_print_string fmt "(accept range)")
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index a30d3798e06589c1e4ed673a63cda1e608de72bf..91a99a5418dd011990574ef607bf9d6b011a3016 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/src/plugins/wp/TacUnfold.ml
@@ -56,7 +56,7 @@ let rec applicable ?at e f es = function
begin
try
let v = phi f es in
- let d = Pretty_utils.sfprintf "Unfold '%a'" Lang.Fun.pretty f in
+ let d = Format.asprintf "Unfold '%a'" Lang.Fun.pretty f in
Applicable (Tactical.rewrite ?at [d,F.p_true,e,v])
with Not_found | Invalid_argument _ ->
applicable ?at e f es others
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index dce4e1951a75d5d475b14484f09a4a1b4905e139..07645004d587aa7a93c6f4fa1f722b17d2029043 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -93,7 +93,7 @@ let print_wp s =
let prv = String.split_on_char ',' name in
String.concat ":" prv
-let title p = Pretty_utils.sfprintf "%a" Why3.Whyconf.print_prover p
+let title p = Format.asprintf "%a" Why3.Whyconf.print_prover p
let name p = p.Why3.Whyconf.prover_name
let compare = Why3.Whyconf.Prover.compare
let is_mainstream p = p.Why3.Whyconf.prover_altern = ""
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index 1069e9ef7a4757bb69778f0747839f80dbab700a..3cfbe68d578f68e48d2c82ca7106195dadda3111 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -275,8 +275,8 @@ let dump ~dir kf reached =
match s.skind with
| Instr _ | Return _ | Break _ | Continue _ | Goto _ ->
Pu.to_string Pr.pp_stmt s
- | If(e,_,_,_) -> Pu.sfprintf "@[<hov 2>if (%a)@]" Pr.pp_exp e
- | Switch(e,_,_,_) -> Pu.sfprintf "@[<hov 2>switch (%a)@]" Pr.pp_exp e
+ | If(e,_,_,_) -> Format.asprintf "@[<hov 2>if (%a)@]" Pr.pp_exp e
+ | Switch(e,_,_,_) -> Format.asprintf "@[<hov 2>switch (%a)@]" Pr.pp_exp e
| Loop _ -> Printf.sprintf "Loop s%d" s.sid
| Block _ -> Printf.sprintf "Block s%d" s.sid
| UnspecifiedSequence _ -> Printf.sprintf "Seq. s%d" s.sid