diff --git a/Makefile b/Makefile
index 77433b677c0f16679408e43853e1e56de7579ce5..d8e4d6405e58be280bce04571ebebad065f92984 100644
--- a/Makefile
+++ b/Makefile
@@ -860,8 +860,8 @@ endif
 # General rules for ordering files within PLUGIN_CMO:
 # - try to keep the legacy Value before Eva
 PLUGIN_CMO:= partitioning/split_strategy value_parameters \
-	utils/value_perf utils/partitioning_annots \
-        utils/value_util utils/red_statuses \
+	utils/value_perf utils/eva_annotations \
+	utils/value_util utils/red_statuses \
 	utils/mark_noresults \
 	utils/widen_hints_ext utils/widen \
 	partitioning/split_return \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index ad7a910447dba8edf011c15b02746bd9e3a48721..3e89f12518e8ee6a37d47076c045a8dd2c137848 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1328,8 +1328,8 @@ src/plugins/value/utils/red_statuses.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/utils/library_functions.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/utils/library_functions.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/utils/mark_noresults.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/partitioning_annots.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/partitioning_annots.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_annotations.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_annotations.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/utils/state_import.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/utils/state_import.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index 33ad321a5cba2cdbbf4c053b7f77fb153a91656b..6b5a0bee6b8a079dd2ac24d98997e3a05d406f1f 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -21,7 +21,7 @@
 (**************************************************************************)
 
 open Value_parameters
-open Partitioning_annots
+open Eva_annotations
 open Cil_types
 
 let is_return s = match s.skind with Return _ -> true | _ -> false
diff --git a/src/plugins/value/partitioning/per_stmt_slevel.ml b/src/plugins/value/partitioning/per_stmt_slevel.ml
index ca504df3baeb37c32d6aa5048117373d27e3afb6..d93674f6e63b5429a3a18fb2dd1b76c992117c48 100644
--- a/src/plugins/value/partitioning/per_stmt_slevel.ml
+++ b/src/plugins/value/partitioning/per_stmt_slevel.ml
@@ -21,7 +21,7 @@
 (**************************************************************************)
 
 open Cil_types
-open Partitioning_annots
+open Eva_annotations
 
 module G = struct
   type t = kernel_function
diff --git a/src/plugins/value/utils/partitioning_annots.ml b/src/plugins/value/utils/eva_annotations.ml
similarity index 100%
rename from src/plugins/value/utils/partitioning_annots.ml
rename to src/plugins/value/utils/eva_annotations.ml
diff --git a/src/plugins/value/utils/partitioning_annots.mli b/src/plugins/value/utils/eva_annotations.mli
similarity index 87%
rename from src/plugins/value/utils/partitioning_annots.mli
rename to src/plugins/value/utils/eva_annotations.mli
index 3d86f2f40076ea0f421cc2c55287f9a5dfa8e62c..9c29a1612aa26943e112d925fe38fce12502be31 100644
--- a/src/plugins/value/utils/partitioning_annots.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -20,6 +20,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Registers Eva annotations:
+    - slevel annotations: "slevel default", "slevel merge" and "slevel i"
+    - loop unroll annotations: "loop unroll term"
+    - value partitioning annotations: "split term" and "merge term"
+    - subdivision annotations: "subdivide i"
+
+    Widen hints annotations are still registered in !{widen_hints_ext.ml}. *)
+
 type slevel_annotation =
   | SlevelMerge
   | SlevelDefault
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 6db4c29ae6781d1a00ab709c5a73a5918439f254..545c6bfc12471b277f1da3c25e57623db1b473ae 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -78,7 +78,7 @@ let get_subdivision_option stmt =
   with Not_found -> Value_parameters.LinearLevel.get ()
 
 let get_subdivision stmt =
-  match Partitioning_annots.get_subdivision_annot stmt with
+  match Eva_annotations.get_subdivision_annot stmt with
   | [] -> get_subdivision_option stmt
   | [x] -> x
   | x :: _ ->