[Eva] Renames partitioning_annots into eva_annotations.

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 \

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

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

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

src/plugins/value/utils/partitioning_annots.mli → 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

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 :: _ ->