From 63c33248d87750cd35bb23b30918ce1497a4b53a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 27 Sep 2019 11:00:19 +0200
Subject: [PATCH] [Eva] Renames partitioning_annots into eva_annotations.
---
Makefile | 4 ++--
headers/header_spec.txt | 4 ++--
src/plugins/value/partitioning/partitioning_parameters.ml | 2 +-
src/plugins/value/partitioning/per_stmt_slevel.ml | 2 +-
.../utils/{partitioning_annots.ml => eva_annotations.ml} | 0
.../{partitioning_annots.mli => eva_annotations.mli} | 8 ++++++++
src/plugins/value/utils/value_util.ml | 2 +-
7 files changed, 15 insertions(+), 7 deletions(-)
rename src/plugins/value/utils/{partitioning_annots.ml => eva_annotations.ml} (100%)
rename src/plugins/value/utils/{partitioning_annots.mli => eva_annotations.mli} (87%)
diff --git a/Makefile b/Makefile
index 77433b677c0..d8e4d6405e5 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 ad7a910447d..3e89f12518e 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 33ad321a5cb..6b5a0bee6b8 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 ca504df3bae..d93674f6e63 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 3d86f2f4007..9c29a1612aa 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 6db4c29ae67..545c6bfc124 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 :: _ ->
--
GitLab