diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index b3a1cd537adee172e63ca1277749817319e304be..63070311232e05e20a6e0ff093d52a6f2ec581ea 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -9,6 +9,13 @@ release. First we list changes of the last release.
   \texttt{-keep-unused-specified-functions} and
   \texttt{-remove-unused-specified-functions} with
   \texttt{-keep-unused-functions}.
+\item \textbf{Preparing the Sources:} remove previously obsoleted
+  options \texttt{-continue-annot-error} (replaced by
+  \texttt{-kernel-warn-key annot-error}),
+  \texttt{-implicit-function-declaration} (replaced by
+  \texttt{-kernel-warn-key typing:implicit-function-declaration}),
+  and \texttt{-warn-decimal-float} (replaced by
+  \texttt{-kernel-warn-key parser:decimal-float}).
 \end{itemize}
 
 \section*{29.0 (Copper)}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index 6b6fbb73637d63a1e75f5bda809a874ed62aac91..78536cb5ac2052e404ab9fe57bafaf0422fb0442 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -205,16 +205,6 @@ opposite form \texttt{-no-collapse-call-cast} is more useful.
 constant expressions. For instance,
 the expression \texttt{1+2} is replaced by \texttt{3}.
 
-\item \deprecatedoptiondef{-}{continue-annot-error} \emph{Deprecated option.}
-  Just emits a warning and discards the annotation when it fails to type-check,
-  instead of generating an error (errors in \C are still fatal). This behavior
-  is now managed by warning category (Section~\ref{sec:feedback-options})
-\texttt{annot-error}, whose default status is ``abort''. Behavior of
-\texttt{-continue-annot-error} can thus be obtained with
-\texttt{-kernel-warn-key annot-error=active}, or even
-\texttt{-kernel-warn-key annot-error=inactive} to silently ignore any ill-formed
-annotations.
-
 \item \texttt{\optiondef{-}{enums} <repr name>} specifies which representation
 should be used for a given enumerated type. Namely, the C standard allows the use
 of any integral type in which all the corresponding tags can be represented.
@@ -618,38 +608,18 @@ As stated before, if you want to ensure the code analyzed by \FramaC is
 strictly equivalent to the one from the target system, you must either
 proofread the definitions, or provide your own library files.
 
-\section{Warnings during normalization}\label{sec:warnings-normalize}
+% \section{Warnings during normalization}\label{sec:warnings-normalize}
 
-\emph{Note: the options below are deprecated, replaced by the more general and
-  flexible mechanism of \emph{warning categories}, described in
-  Section~\ref{sec:feedback-options}.}
+% \emph{Note: the options below are deprecated, replaced by the more general and
+%   flexible mechanism of \emph{warning categories}, described in
+%   Section~\ref{sec:feedback-options}.}
 
-Some options can be used to influence the warnings that are
-emitted by \FramaC during the normalization phase.
+% Some options can be used to influence the warnings that are
+% emitted by \FramaC during the normalization phase.
 
-\begin{description}
-\item \texttt{\deprecatedoptiondef{-}{warn-decimal-float} <freq>}
-  (\emph{deprecated}) warns
-  when floating-point constants in the program cannot be exactly represented;
-  freq must be one of \texttt{none}, \texttt{once} or \texttt{all}.
-  Defaults to \texttt{once}.
-  \emph{Superseded by warning category \texttt{parser:decimal-float}.}
-
-\item \texttt{\deprecatedoptiondef{-}{implicit-function-declaration} <action>}
-  (\emph{deprecated}) defines
-  the action to perform (\texttt{ignore}, \texttt{warn} or \texttt{error})
-  whenever a call to a function that has not been previously declared is found.
-  This is invalid in C90 or in C99, but could be valid K\&R code.
-  Defaults to \texttt{warn}.
-  \emph{Superseded by warning category \texttt{typing:implicit-function-declaration}}.
-  \textbf{Note:} parsing is not guaranteed to succeed, regardless of
-  the emission of the warning. Upon encountering a call to an undeclared
-  function, \FramaC attempts to continue its parsing
-  phase by inferring a prototype corresponding to the type of the
-  arguments at the call (modulo default argument promotions).
-  If the real declaration does not match the
-  inferred prototype, parsing will later end with an error.
-\end{description}
+% \begin{description}
+
+% \end{description}
 
 \section{Testing the Source Code Preparation}
 
diff --git a/man/frama-c.1 b/man/frama-c.1
index af751133d7619229d9fe423b3b9f034859f5f1c7..fa12da7239932e0498a03fefaf777bf329ef3dce 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -168,20 +168,6 @@ variables with const qualifier must be actually constant.
 Defaults to yes.
 The opposite option is \f[B]-unsafe-writable\f[R].
 .TP
-[-no]-continue-annot-error
-when analyzing an annotation, the default behavior (the \f[B]-no\f[R]
-version of this option) when a typechecking error occurs is to reject
-the source file as is the case for typechecking errors within the C
-code.
-With this option on, the typechecker will only output a warning and
-discard the annotation but type‐checking will continue (errors in C code
-are still fatal, though).
-.PD 0
-.P
-.PD
-\f[B]Deprecated\f[R]: use \f[B]-kernel-warn-key annot-error\f[R]
-instead.
-.TP
 -cpp-command \f[I]cmd\f[R]
 uses \f[I]cmd\f[R] as the command to preprocess C files.
 Defaults to the \f[B]CPP\f[R] environment variable or to
@@ -261,17 +247,6 @@ If \f[B]-cpp-frama-c-compliant\f[R] is not false, also adds
 header files.
 Defaults to yes.
 .TP
--implicit-function-declaration \f[I]action\f[R]
-warns or aborts when a function is called before it has been declared.
-\f[I]action\f[R] can be one of \f[B]ignore\f[R], \f[B]warn\f[R], or
-\f[B]error\f[R].
-Defaults to \f[B]warn\f[R].
-.PD 0
-.P
-.PD
-\f[B]Deprecated\f[R]: use \f[B]-kernel-warn-key
-typing:implicit-function-declaration\f[R] instead.
-.TP
 -initialized-padding-locals
 implicit initialization of locals sets padding bits to 0.
 If false, padding bits are left uninitialized.
@@ -548,17 +523,6 @@ case (this is the default).
 -version
 outputs the version string of Frama-C.
 .TP
--warn-decimal-float \f[I]freq\f[R]
-warns when a floating-point constant cannot be exactly represented
-(e.g.\ 0.1).
-\f[I]freq\f[R] can be one of \f[B]none\f[R], \f[B]once\f[R], or
-\f[B]all\f[R].
-.PD 0
-.P
-.PD
-\f[B]Deprecated\f[R]: use \f[B]-kernel-warn-key
-parser:decimal-float=once\f[R] (and variants) instead.
-.TP
 [-no]-warn-invalid-pointer
 generate alarms for invalid pointer arithmetic.
 Defaults to no.
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 9b4007641b51fedc8f0c62a42913e9fc58d6867d..21609dfc7c82daea5b78d37f7df0f29be26ea647 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -155,14 +155,6 @@ Defaults to no.
 : variables with const qualifier must be actually constant. Defaults to yes.
 The opposite option is **-unsafe-writable**.
 
-[-no]-continue-annot-error
-: when analyzing an annotation, the default behavior (the **-no** version of
-this option) when a typechecking error occurs is to reject the source file as
-is the case for typechecking errors within the C code. With this option on,
-the typechecker will only output a warning and discard the annotation but
-type‐checking will continue (errors in C code are still fatal, though). \
-**Deprecated**: use **-kernel-warn-key annot-error** instead.
-
 -cpp-command *cmd*
 : uses *cmd* as the command to preprocess C files.
 Defaults to the **CPP** environment variable or to
@@ -228,13 +220,6 @@ Default is **gcc-enums**.
 If **-cpp-frama-c-compliant** is not false, also adds **-nostdinc** to prevent
 an inconsistent mix of system and Frama-C header files. Defaults to yes.
 
--implicit-function-declaration *action*
-: warns or aborts when a function is called before it has been declared.
-*action* can be one of **ignore**, **warn**, or **error**.
-Defaults to **warn**.\
-**Deprecated**: use **-kernel-warn-key typing:implicit-function-declaration**
-instead.
-
 -initialized-padding-locals
 : implicit initialization of locals sets padding bits to 0.
 If false, padding bits are left uninitialized. Defaults to yes.
@@ -469,12 +454,6 @@ the case (this is the default).
 -version
 : outputs the version string of Frama-C.
 
--warn-decimal-float *freq*
-: warns when a floating-point constant cannot be exactly represented
-(e.g. 0.1). *freq* can be one of **none**, **once**, or **all**. \
-**Deprecated**: use **-kernel-warn-key parser:decimal-float=once**
-(and variants) instead.
-
 [-no]-warn-invalid-pointer
 : generate alarms for invalid pointer arithmetic. Defaults to no.
 
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 826000ae54ffa9595eedb80f6b79a4ffc35b6861..8bd77a0e771906eda26d66cda8b0d0e37a6b2386 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3606,10 +3606,10 @@ struct
 
   let integral_cast = integral_cast
 
-  (* This function raises a non-recoverable when [-continue-annot-error] is not
-     set, and [LogicTypeError] otherwise. This exception must *not* escape
-     Cabs2cil. Hence, each call to a function of module [Ltyping] below must
-     catch it. *)
+  (* This function raises a non-recoverable when [-kernel-warn-key annot-error]
+     is not set, and [LogicTypeError] otherwise. This exception must *not*
+     escape Cabs2cil. Hence, each call to a function of module [Ltyping] below
+     must catch it. *)
   let error loc msg =
     Pretty_utils.ksfprintf (fun e -> raise (LogicTypeError (loc,e))) msg
 
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 4c8f43f3d8aa503737740d4af436769737b767e7..132d30d68c5e67a30f5ee892952e95ba6a38a3c0 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3597,8 +3597,6 @@ let isPointerType t =
 (* ISO 6.2.5.21 *)
 let isScalarType t = isArithmeticType t || isPointerType t
 
-let isArithmeticOrPointerType = isScalarType
-
 
 (********** TRANSPARENT UNION ******)
 (* Check if a type is a transparent union, and return the first field if it
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index f39332dfbd8e58788cd8cf63424d606c16af3296..cb016440a6ce183d18b3732dd68c6bbf700b15ec 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -559,11 +559,6 @@ val isArithmeticType: typ -> bool
 *)
 val isScalarType: typ -> bool
 
-(** alias of isScalarType.
-    @deprecated 22.0-Titanium use isScalarType instead
-*)
-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. *)
 val isLogicArithmeticType: logic_type -> bool
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index b1b29a889bfa8bbd453c4e0a271ec540911264c6..0b255b0fd0482ba9355d71f6d95f4edb657c8dc1 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -138,9 +138,10 @@ type typing_context = {
 
   on_error: 'a 'b. ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
   (** [on_error f rollback x] will attempt to evaluate [f x]. If this triggers
-      an error while in [-continue-annot-error] mode, [rollback (loc,cause)]
-      will be executed (where [loc] is the location of the error and [cause]
-      a text message indicating the issue) and the exception will be re-raised.
+      an error while in [-kernel-warn-key annot-error] mode, [rollback
+      (loc,cause)] will be executed (where [loc] is the location of the error
+      and [cause] a text message indicating the issue) and the exception will
+      be re-raised.
 
       @since Chlorine-20180501
       @before 25.0-Manganese [rollback] didn't take [loc] and [cause] as argument
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 7d43c5cb2aac0210cf28e992340746724eb7d86b..072c245325c87aa19ce8e08e782c8407da1fc4d3 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -246,7 +246,7 @@ let mk_cast ?loc ?(force=false) newt t =
                (Ctype newt')
         -> unroll_cast e
       | TCast(true,Linteger,e)
-        when Cil.isArithmeticOrPointerType newt'
+        when Cil.isScalarType newt'
         -> unroll_cast e
       | TCast(true,Lreal,e)
         when Cil.isFloatingType newt'
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index fdc4828f50e784b01d34b48f7dd99b09972c93a1..86bb74a82b3a7b84659215afdda5a8e5b1c2b8f3 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1147,26 +1147,6 @@ module FramaCStdLib =
          inconsistent mix of system and Frama-C header files"
     end)
 
-let () = Parameter_customize.set_group parsing
-let () = Parameter_customize.do_not_reset_on_copy ()
-module ContinueOnAnnotError =
-  False(struct
-    let module_name = "ContinueOnAnnotError"
-    let option_name = "-continue-annot-error"
-    let help =
-      "[DEPRECATED: Use -kernel-warn-key annot-error instead] \
-       When an annotation fails to type-check, emit a warning \
-       and discard the annotation instead of generating an error \
-       (errors in C are still fatal)"
-  end)
-let () =
-  ContinueOnAnnotError.add_set_hook
-    (fun _ f ->
-       warning ~once:true
-         "-continue-annot-error is deprecated. \
-          Use -kernel-warn-key annot-error (or similar option) instead";
-       set_warn_status wkey_annot_error (if f then Log.Wactive else Log.Wabort))
-
 let () = Parameter_customize.set_group parsing
 module Orig_name =
   False(struct
@@ -1175,61 +1155,6 @@ module Orig_name =
     let help = "prints a message each time a variable is renamed"
   end)
 
-let () = Parameter_customize.set_group parsing
-let () = Parameter_customize.do_not_reset_on_copy ()
-module ImplicitFunctionDeclaration =
-  String(struct
-    let option_name = "-implicit-function-declaration"
-    let arg_name = "action"
-    let help =
-      "[DEPRECATED: Use \
-       -kernel-warn-key typing:implicit-function-declaration=error instead] \
-       Warn or abort when a function is called before it has been declared \
-       (non-C99 compliant); action must be ignore, warn, or error"
-    let default = "warn"
-    let module_name = "ImplicitFunctionDeclaration"
-  end)
-let () = ImplicitFunctionDeclaration.set_possible_values ["ignore"; "warn"; "error"]
-let () =
-  ImplicitFunctionDeclaration.add_set_hook
-    (fun _ s ->
-       warning ~once:true
-         "-implicit-function-declaration is deprecated, \
-          use '-kernel-warn-key typing:implicit-function-declaration' \
-          (or similar options) instead.";
-       let status =
-         if s = "ignore" then Log.Winactive else
-         if s = "warn" then Log.Wactive else
-         if s = "error" then Log.Wabort
-         else fatal "invalid value: %s" s
-       in
-       set_warn_status wkey_implicit_function_declaration status)
-
-
-let () = Parameter_customize.set_group parsing
-let () = Parameter_customize.do_not_reset_on_copy ()
-module WarnDecimalFloat =
-  String(struct
-    let option_name = "-warn-decimal-float"
-    let arg_name = "freq"
-    let help = "[DEPRECATED: Use -kernel-warn-key \
-                parser:decimal-float=active (or inactive) instead] \
-                Warn when floating-point constants cannot be exactly \
-                represented; freq must be one of none, once or all"
-    let default = "once"
-    let module_name = "WarnDecimalFloat"
-  end)
-let () = WarnDecimalFloat.set_possible_values ["none"; "once"; "all"]
-let () = WarnDecimalFloat.add_set_hook
-    (fun _ s ->
-       let status =
-         if s = "none" then Log.Winactive
-         else if s = "once" then Log.Wonce
-         else if s = "all" then Log.Wactive
-         else fatal "invalid value: %s" s
-       in
-       set_warn_status wkey_decimal_float status)
-
 let () = Parameter_customize.set_group parsing
 let () = Parameter_customize.do_not_reset_on_copy ()
 module C11 =
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index c0359ebf232f021d47ad6ac2c60958c5f88036a4..940ff68224fd6a3bc668c24f323072a3619a25fe 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -491,10 +491,6 @@ module ReadAnnot: Parameter_sig.Bool
 module PreprocessAnnot: Parameter_sig.Bool
 (** Behavior of option "-pp-annot" *)
 
-module ContinueOnAnnotError: Parameter_sig.Bool
-[@@ deprecated "Use Kernel.wkey_annot_error instead"]
-(** Behavior of option "-continue-annot-error" *)
-
 module SimplifyCfg: Parameter_sig.Bool
 (** Behavior of option "-simplify-cfg" *)
 
@@ -540,14 +536,6 @@ val normalization_parameters: unit -> Typed_parameter.t list
     changing one will reset the AST entirely.contents
 *)
 
-module WarnDecimalFloat: Parameter_sig.String
-[@@ deprecated "Uses kernel.wkey_decimal_float instead."]
-(** Behavior of option "-warn-decimal-float" *)
-
-module ImplicitFunctionDeclaration: Parameter_sig.String
-[@@ deprecated "Uses kernel.wkey_implicit_function_declaration instead."]
-(** Behavior of option "-implicit-function-declaration" *)
-
 module C11: Parameter_sig.Bool
 (** Behavior of option "-c11" *)
 
diff --git a/src/libraries/stdlib/integer.ml b/src/libraries/stdlib/integer.ml
index 7cd8055eaeed25bb8bcd20b051ff8a50b53d187b..4aac7d3b5019910cfe1481b6a3ad20a2301a635a 100644
--- a/src/libraries/stdlib/integer.ml
+++ b/src/libraries/stdlib/integer.ml
@@ -105,12 +105,6 @@ let to_int_exn = Z.to_int
 let to_int64_exn = Z.to_int64
 let to_int32_exn = Z.to_int32
 
-(* These functions are deprecated (renamed to *_exn) and will be removed
-   in a future version. *)
-let to_int = to_int_exn
-let to_int64 = to_int64_exn
-let to_int32 = to_int32_exn
-
 let wrap to_int i = try Some (to_int i) with Z.Overflow -> None
 let to_int_opt = wrap Z.to_int
 let to_int64_opt = wrap Z.to_int64
@@ -202,9 +196,9 @@ let pretty_hex fmt v =
     if gt v two_power_60 then
       let quo, rem = Z.ediv_rem v two_power_60 in
       aux quo;
-      Format.fprintf fmt "%015LX" (to_int64 rem)
+      Format.fprintf fmt "%015LX" (to_int64_exn rem)
     else
-      Format.fprintf fmt "%LX" (to_int64 v)
+      Format.fprintf fmt "%LX" (to_int64_exn v)
   in
   if equal v zero then Format.pp_print_string fmt "0"
   else if gt v zero then (Format.pp_print_string fmt "0x"; aux v)
@@ -229,7 +223,7 @@ let length u v = succ (sub v u)
 let extract_bits ~start ~stop v =
   assert (ge start zero && ge stop start);
   (*Format.printf "%a[%a..%a]@\n" pretty v pretty start pretty stop;*)
-  let r = Z.extract v (to_int start) (to_int (length start stop)) in
+  let r = Z.extract v (to_int_exn start) (to_int_exn (length start stop)) in
   (*Format.printf "%a[%a..%a]=%a@\n" pretty v pretty start pretty stop pretty r;*)
   r
 
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 73bab4037654230580768e8c8c41c07209f55eba..43df286f2abd31437aff6faae54908ee558be632 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -124,27 +124,6 @@ val of_int : int -> t
 val of_int64 : Int64.t -> t
 val of_int32 : Int32.t -> t
 
-(**
-   @raise Z.Overflow if too big
-   @deprecated 24.0-Chromium Renamed to [to_int_exn].
-                           Also consider using [to_int_opt].
-*)
-val to_int : t -> int [@@deprecated]
-
-(**
-   @raise Z.Overflow if too big
-   @deprecated 24.0-Chromium Renamed to [to_int64_exn].
-                           Also consider using [to_int64_opt].
-*)
-val to_int64 : t -> int64 [@@deprecated]
-
-(**
-   @raise Z.Overflow if too big
-   @deprecated 24.0-Chromium Renamed to [to_int32_exn].
-                           Also consider using [to_int32_opt].
-*)
-val to_int32 : t -> int32 [@@deprecated]
-
 (**
    @raise Z.Overflow if too big
    @since 24.0-Chromium
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 30fe58b34cd0d96ce9ad20056d61d3ec8d04b538..40ecb41ec45848503214b0b3ab4552066b2d3310 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -297,9 +297,7 @@ module Normalized = struct
         (String.lowercase_ascii s2)
 
   let empty = normalize ""
-  let unknown = empty
   let is_empty fp = equal fp empty
-  let is_unknown = is_empty
   let special_stdout = normalize "-"
   let is_special_stdout fp = equal fp special_stdout
 
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index e41e6940082440037bf97db038080b74b39cdded..9f0e8a8e1b37b8365149968910fd5bfd18a0329a 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -135,18 +135,6 @@ module Normalized: sig
   (** Pretty-prints the normalized (absolute) path. *)
   val pp_abs: Format.formatter -> t -> unit
 
-  (** Unknown filepath, used as 'dummy' for [Datatype.Filepath].
-      @deprecated 23.0-Vanadium use 'empty' instead
-  *)
-  val unknown: t
-  [@@alert deprecated "Use Filepath.Normalized.empty instead"]
-
-  (** @since 20.0-Calcium
-      @deprecated 23.0-Vanadium use 'is_empty' instead
-  *)
-  val is_unknown: t -> bool
-  [@@alert deprecated "Use Filepath.Normalized.is_empty instead"]
-
   (** Empty filepath, used as 'dummy' for [Datatype.Filepath].
       @since 23.0-Vanadium.
   *)
diff --git a/src/plugins/eva/domains/cvalue/builtins_split.ml b/src/plugins/eva/domains/cvalue/builtins_split.ml
index e688ca723c4e4593178251c30ee536b508d59467..ea9da3c02c4f8ac3c9495b978bc815759bcc82ca 100644
--- a/src/plugins/eva/domains/cvalue/builtins_split.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_split.ml
@@ -72,7 +72,7 @@ let warning warn s =
    singleton location with an arithmetic type, and that it contains no more than
    [max_card] elements. *)
 let split_v ~warn lv state max_card =
-  if Cil.isArithmeticOrPointerType lv.typ then
+  if Cil.isScalarType lv.typ then
     let loc = Cvalue_queries.lval_to_loc state lv in
     if Locations.Location_Bits.cardinal_zero_or_one loc.Locations.loc then
       let v_indet = Cvalue.Model.find_indeterminate state loc in
@@ -132,7 +132,7 @@ let rec gather_lv_in_exp acc e =
 and gather_lv_in_lv acc lv =
   let (host, offset) = lv.node in
   let acc =
-    if Cil.isArithmeticOrPointerType lv.typ
+    if Cil.isScalarType lv.typ
     then lv :: acc
     else acc
   in
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index 2ee6847b25d290ca8c6aaf871a2303ea7572505b..c11f27519b99259adde35f7ba9d2d9965adf71b3 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -118,7 +118,7 @@ module Queries = struct
         v, alarms
 
   let extract_lval ~oracle:_ _context state lval loc =
-    if Cil.isArithmeticOrPointerType lval.Eva_ast.typ
+    if Cil.isScalarType lval.Eva_ast.typ
     then extract_scalar_lval state lval loc
     else extract_aggregate_lval state lval loc
 
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index adf3a68221646a5e5ec2e086c1881840c05b88ec..78c7105fe3e4e427486d9eb47a826ff0e0c026c8 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -381,7 +381,7 @@ struct
   let assign_eq left_lval right_expr value valuation state =
     if Eva_ast.lval_contains_volatile left_lval ||
        Eva_ast.exp_contains_volatile right_expr ||
-       not (Cil.isArithmeticOrPointerType left_lval.typ) ||
+       not (Cil.isScalarType left_lval.typ) ||
        indeterminate_copy value
     then state
     else
@@ -457,7 +457,7 @@ struct
           and e2 = Eva_ast.const_fold e2 in
           if Eva_ast.exp_contains_volatile e1
           || Eva_ast.exp_contains_volatile e2
-          || not (Cil.isArithmeticOrPointerType e1.typ)
+          || not (Cil.isScalarType e1.typ)
           || (expr_is_cardinal_zero_or_one_loc valuation e1 &&
               expr_cardinal_zero_or_one valuation e2)
           || (expr_is_cardinal_zero_or_one_loc valuation e2 &&
diff --git a/src/plugins/eva/domains/offsm_domain.ml b/src/plugins/eva/domains/offsm_domain.ml
index 190deb18e576daa29788328186cc7a57c88bcf1e..4c5051422b7f219dc3a8c4aab69e1c262e088611 100644
--- a/src/plugins/eva/domains/offsm_domain.ml
+++ b/src/plugins/eva/domains/offsm_domain.ml
@@ -186,7 +186,7 @@ module D : Abstract_domain.Leaf
   let extract_lval ~oracle:_ _context state lv locs =
     let o =
       if Cil.typeHasQualifier "volatile" lv.Eva_ast.typ ||
-         not (Cil.isArithmeticOrPointerType lv.Eva_ast.typ)
+         not (Cil.isScalarType lv.Eva_ast.typ)
       then
         `Value (Top, None)
       else
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index 2bbe125a610fa13f0c632f1e3afff9b207bd7ac9..e2a72839350ab113656827bb2ccccea3ae867ddb 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -543,7 +543,7 @@ module D : Abstract_domain.Leaf
     `Value (Memory.kill loc state)
 
   let store_copy valuation lv loc state fv =
-    if Cil.isArithmeticOrPointerType lv.lval.typ then
+    if Cil.isScalarType lv.lval.typ then
       match fv.v, fv.initialized, fv.escaping with
       | `Value v, true, false -> store_value valuation lv.lval loc state v
       | _ -> store_indeterminate state loc
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 23b1d1dbac4fedc925047c3a2254092056d320a5..33fc8fc4c3abc07ded45489725070c179790d20e 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -365,7 +365,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
     let written_formals = Backward_formals.written_formals call.kf in
     let is_safe argument =
       not (Varinfo.Set.mem argument.formal written_formals)
-      && Cil.isArithmeticOrPointerType argument.formal.vtype
+      && Cil.isScalarType argument.formal.vtype
       && is_safe_argument valuation argument.concrete
     in
     List.filter is_safe call.arguments
@@ -496,7 +496,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
         Self.abort ~current:true
           "Function argument %a has unknown size. Aborting"
           Eva_ast.pp_exp expr;
-      if determinate && Cil.isArithmeticOrPointerType lv.typ
+      if determinate && Cil.isScalarType lv.typ
       then assign_by_eval ~subdivnb state valuation expr
       else assign_by_copy ~subdivnb state valuation lv loc
     | _ -> assign_by_eval ~subdivnb state valuation expr
@@ -645,7 +645,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
         (Bottom.pretty Cvalue.V.pretty) fmt value
 
   let pretty_arguments ~subdivnb state arguments =
-    let is_scalar lval = Cil.isArithmeticOrPointerType lval.Eva_ast.typ in
+    let is_scalar lval = Cil.isScalarType lval.Eva_ast.typ in
     let pretty fmt (expr : Eva_ast.exp) =
       match expr.node with
       | Lval lval | StartOf lval when not (is_scalar lval) ->
diff --git a/src/plugins/eva/legacy/eval_op.ml b/src/plugins/eva/legacy/eval_op.ml
index 8573642195cac4b0701a71bc726642759e15decc..5b5ed54e071b9898aa542ab3ca6542c05fac722f 100644
--- a/src/plugins/eva/legacy/eval_op.ml
+++ b/src/plugins/eva/legacy/eval_op.ml
@@ -191,7 +191,7 @@ let apply_on_all_locs f loc state =
 (* Display [o] as a single value, when this is more readable and more precise
    than the standard display. *)
 let pretty_stitched_offsetmap fmt typ o =
-  if Cil.isArithmeticOrPointerType typ &&
+  if Cil.isScalarType typ &&
      not (Cvalue.V_Offsetmap.is_single_interval o)
   then
     let v = v_uninit_of_offsetmap ~typ o in
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 62539f594e42587fbaf01d4fdddd3bf50b0012c6..b8b8e8f1dbf3dbc1754fb58b2fe825196bdb2eed 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -508,7 +508,7 @@ let rec isLogicNonCompositeType t =
     (try isLogicNonCompositeType (Logic_const.type_of_element t)
      with Failure _ -> false)
   | Linteger | Lreal -> true
-  | Ctype t -> Cil.isArithmeticOrPointerType t
+  | Ctype t -> Cil.isScalarType t
 
 let rec infer_type = function
   | Ctype t ->
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 0432d1d2785b88e6baa85fae55ed024218b11be1..466dfd85c3670e535458db438b935ea46340ea20 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -438,7 +438,7 @@ struct
                padding bits. The 100 limit is arbitrary. *)
             let implicit =
               not (Cil.isArrayType ct &&
-                   (Cil.isArithmeticOrPointerType (Cil.typeOf_array_elem ct)
+                   (Cil.isScalarType (Cil.typeOf_array_elem ct)
                     || Ast_info.array_size ct > (Integer.of_int 100)))
             in
             let r = Cil.foldLeftCompound ~implicit ~doinit ~ct ~initl ~acc in
diff --git a/src/plugins/inout/cumulative_analysis.ml b/src/plugins/inout/cumulative_analysis.ml
index fe7eba811ec90b257007807bf5e84be6c6bde9dd..9f3629c6a1ed1f7bf17b731f78e9be648e97fb8b 100644
--- a/src/plugins/inout/cumulative_analysis.ml
+++ b/src/plugins/inout/cumulative_analysis.ml
@@ -32,7 +32,7 @@ open Visitor
 let fold_implicit_initializer typ =
   not
     (Cil.isArrayType typ &&
-     (Cil.isArithmeticOrPointerType (Cil.typeOf_array_elem typ)
+     (Cil.isScalarType (Cil.typeOf_array_elem typ)
       || Ast_info.array_size typ > (Integer.of_int 100)))
 
 let specialize_state_on_call ?stmt kf =
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index ef3514c844b85d222bb7e2cb5142a3b9dca67e02..5b44ee61a5da89feff5d5c2e5d9ecd77bca94223 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -215,7 +215,7 @@ let field = function
 let load = function
   | Loc_var x -> Val_var x (* E.access x ByValue E.bot *)
   | Loc_shift(x,e) ->
-    if Cil.isArithmeticOrPointerType x.vtype then
+    if Cil.isScalarType x.vtype then
       E (E.access x ByAddr e)
     else
       E (E.access x ByValue e)
diff --git a/tests/float/const.i b/tests/float/const.i
index ee5cbc9b58c86f7f6f443cb77a92a04f49cfbbb0..33f7177cdd3c76517c73e9352de095e3e3a49702 100644
--- a/tests/float/const.i
+++ b/tests/float/const.i
@@ -1,5 +1,5 @@
 /* run.config*
-   OPT: -eva @EVA_CONFIG@ -float-hex -warn-decimal-float all -then -out -deps
+   OPT: -eva @EVA_CONFIG@ -float-hex -kernel-warn-key parser:decimal-float=active -then -out -deps
 */
 typedef double mydouble;
 
diff --git a/tests/float/const3.i b/tests/float/const3.i
index 4e06fb90429a435a24a5ca0d21bbe6d7bb7a307c..45ac71323e1005c504ca3363bdafa0176ccf5090 100644
--- a/tests/float/const3.i
+++ b/tests/float/const3.i
@@ -1,6 +1,6 @@
 /* run.config*
-  STDOPT: #"-warn-decimal-float all"
-  STDOPT: #"-warn-decimal-float all -eva-all-rounding-modes-constants -float-hex"
+  STDOPT: #"-kernel-warn-key parser:decimal-float=active"
+  STDOPT: #"-kernel-warn-key parser:decimal-float=active -eva-all-rounding-modes-constants -float-hex"
 */
 
 double f1 = 1e-40f;
diff --git a/tests/float/const4.i b/tests/float/const4.i
index 605bad01de2fd3490a144ba6fc2f01c551ed731f..7473cc2be83ef48a5a3c1d7b4e7bb29948dac909 100644
--- a/tests/float/const4.i
+++ b/tests/float/const4.i
@@ -1,6 +1,6 @@
 /* run.config*
-  STDOPT: #"-warn-decimal-float all"
-  STDOPT: #"-warn-decimal-float all -eva-all-rounding-modes-constants"
+  STDOPT: #"-kernel-warn-key parser:decimal-float=active"
+  STDOPT: #"-kernel-warn-key parser:decimal-float=active -eva-all-rounding-modes-constants"
 */
 
 double f1 = 3.4e38f;
diff --git a/tests/float/cte_overflow.i b/tests/float/cte_overflow.i
index e8ecc2ab47a5e2a361746aee8799d35fd74b5306..cb98e601ccf93f8c83c9d01662e4af347ef3bd57 100644
--- a/tests/float/cte_overflow.i
+++ b/tests/float/cte_overflow.i
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: #"-warn-decimal-float all"
+   STDOPT: #"-kernel-warn-key parser:decimal-float=active"
 */
 
 int volatile v;
diff --git a/tests/float/dr_infinity.i b/tests/float/dr_infinity.i
index facb979b78946b390362ef71c7fd21666ee0fe3d..9ed727829827a3fb01cf0807fc4f37b54bd5edc5 100644
--- a/tests/float/dr_infinity.i
+++ b/tests/float/dr_infinity.i
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: #"-warn-decimal-float all -float-hex"
+   STDOPT: #"-kernel-warn-key parser:decimal-float=active -float-hex"
 */
 volatile v;
 void main(void)
diff --git a/tests/float/extract_bits.i b/tests/float/extract_bits.i
index 083727447193a64d526f1560c853c0a34b6c084e..d348c9e0abb3ee4d5f2b6817de21fec8488e800b 100644
--- a/tests/float/extract_bits.i
+++ b/tests/float/extract_bits.i
@@ -1,6 +1,6 @@
 /* run.config*
-  OPT: -eva @EVA_CONFIG@ -eva-slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -warn-decimal-float all
-  OPT: -eva @EVA_CONFIG@ -eva-slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -warn-decimal-float all
+  OPT: -eva @EVA_CONFIG@ -eva-slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -kernel-warn-key parser:decimal-float=active
+  OPT: -eva @EVA_CONFIG@ -eva-slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -kernel-warn-key parser:decimal-float=active
 */
 
 float f = 3.14;
diff --git a/tests/float/logic.i b/tests/float/logic.i
index 2f72dc3a4b4155737cdc46d4966bfb4a88bd935a..52402c55205cb4e7b577cadbac371de3a6687a1c 100644
--- a/tests/float/logic.i
+++ b/tests/float/logic.i
@@ -1,6 +1,6 @@
 /* run.config*
-   STDOPT: #"-warn-decimal-float all -float-hex"
-   STDOPT: #"-warn-decimal-float all -float-hex -warn-special-float none"
+   STDOPT: #"-kernel-warn-key parser:decimal-float=active -float-hex"
+   STDOPT: #"-kernel-warn-key parser:decimal-float=active -float-hex -warn-special-float none"
 */
 
 volatile v;
diff --git a/tests/float/parse.i b/tests/float/parse.i
index 5ddf3a15d551048ae63112d37efaa0d57c62ef68..d4fab9c06ab6cb3394fa86071557cec9e0ebbdc3 100644
--- a/tests/float/parse.i
+++ b/tests/float/parse.i
@@ -1,5 +1,5 @@
 /* run.config*
-   STDOPT: #"-warn-decimal-float all -float-hex"
+   STDOPT: #"-kernel-warn-key parser:decimal-float=active -float-hex"
 */
 
 volatile v;