From 91fed3f16f7f954081e964c836ae86a3679ae2db Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 15 Sep 2021 15:23:21 +0200
Subject: [PATCH] [LoopAnalysis] Renames region_analysis_sig as a .mli
interface file.
---
headers/header_spec.txt | 2 +-
src/plugins/loop_analysis/Makefile.in | 3 ++-
src/plugins/loop_analysis/loop_analysis.ml | 8 ++++----
src/plugins/loop_analysis/region_analysis.ml | 8 +++-----
src/plugins/loop_analysis/region_analysis.mli | 3 +--
.../{region_analysis_sig.ml => region_analysis_sig.mli} | 0
src/plugins/loop_analysis/region_analysis_stmt.ml | 2 +-
src/plugins/loop_analysis/region_analysis_stmt.mli | 2 +-
8 files changed, 13 insertions(+), 15 deletions(-)
rename src/plugins/loop_analysis/{region_analysis_sig.ml => region_analysis_sig.mli} (100%)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index cea13556cb6..d6a09d86406 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -941,7 +941,7 @@ src/plugins/loop_analysis/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/region_analysis_sig.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/loop_analysis/region_analysis_sig.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis_stmt.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis_stmt.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/register.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/loop_analysis/Makefile.in b/src/plugins/loop_analysis/Makefile.in
index 74a6af00dbb..4cb7ceebdc7 100644
--- a/src/plugins/loop_analysis/Makefile.in
+++ b/src/plugins/loop_analysis/Makefile.in
@@ -31,7 +31,8 @@ PLUGIN_ENABLE:=@ENABLE_LOOP_ANALYSIS@
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_NAME:= LoopAnalysis
-PLUGIN_CMO:= options region_analysis_sig region_analysis region_analysis_stmt loop_analysis register
+PLUGIN_CMO:= options region_analysis region_analysis_stmt loop_analysis register
+PLUGIN_CMI:= region_analysis_sig
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure test.c test.oracle README.org
PLUGIN_TESTS_DIRS:=loop_analysis
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index b97bd62b23f..43a3fd5b491 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -324,21 +324,21 @@ module Store(* (B:sig *)
let value = (mem,conds) in
let open Cil_types in
let map_on_all_succs (mem,conds) =
- List.map (fun x -> (Region_analysis.Edge(stmt,x),(mem,conds,x))) stmt.succs in
+ List.map (fun x -> (Region_analysis_sig.Edge(stmt,x),(mem,conds,x))) stmt.succs in
match stmt.skind with
| Instr(i) -> map_on_all_succs (do_instr i (mem,conds))
| Return _ ->
- [Region_analysis.Exit stmt, (mem,conds,Cil.dummyStmt)]
+ [Region_analysis_sig.Exit stmt, (mem,conds,Cil.dummyStmt)]
| Loop _ | Goto _ | Break _ | Continue _ | Block _ | UnspecifiedSequence _ ->
map_on_all_succs value
| If _ ->
let result = Dataflows.transfer_if_from_guard do_guard stmt value in
List.map (fun (succ,(mem,cond)) ->
- (Region_analysis.Edge(stmt,succ),(mem,cond,succ))) result
+ (Region_analysis_sig.Edge(stmt,succ),(mem,cond,succ))) result
| Switch _ ->
let result = Dataflows.transfer_switch_from_guard do_guard stmt value in
List.map (fun (succ,(mem,cond)) ->
- (Region_analysis.Edge(stmt,succ),(mem,cond,succ))) result
+ (Region_analysis_sig.Edge(stmt,succ),(mem,cond,succ))) result
| Throw _ | TryCatch _ | TryExcept _ | TryFinally _ ->
Options.abort "unsupported exception-related statement: %a"
Printer.pp_stmt stmt
diff --git a/src/plugins/loop_analysis/region_analysis.ml b/src/plugins/loop_analysis/region_analysis.ml
index c04f9f6ec33..2906d0e5fe3 100644
--- a/src/plugins/loop_analysis/region_analysis.ml
+++ b/src/plugins/loop_analysis/region_analysis.ml
@@ -48,9 +48,7 @@
of Nodes". It is maybe also possible to use the wto ordering of
bourdoncle for this purpose. *)
-include Region_analysis_sig;;
-
-module Make(N:Node):sig
+module Make(N:Region_analysis_sig.Node):sig
(* Function computing from an entry abstract value the "after"
state, which is a map from each outgoing edge to its respective
value. *)
@@ -192,7 +190,7 @@ struct
(* Compute for previous node if result not yet available. *)
and get_edge pred n =
- let edge = Edge(pred, n) in
+ let edge = Region_analysis_sig.Edge(pred, n) in
try N.Edge_Dict.get edge_term edge
with Not_found -> do_node pred; N.Edge_Dict.get edge_term edge
in
@@ -215,7 +213,7 @@ struct
N.Graph.iter_preds header (fun pred ->
if (N.Set.mem pred tset) && (is_back_edge pred header)
then
- let edge = Edge(pred,header) in
+ let edge = Region_analysis_sig.Edge(pred,header) in
let input = N.Edge_Dict.get edge_term edge in
inputs := input::!inputs );
N.join !inputs
diff --git a/src/plugins/loop_analysis/region_analysis.mli b/src/plugins/loop_analysis/region_analysis.mli
index 6b4feeb6c81..02a957af9f4 100644
--- a/src/plugins/loop_analysis/region_analysis.mli
+++ b/src/plugins/loop_analysis/region_analysis.mli
@@ -31,9 +31,8 @@
reached.
TODO: The algorithm does not handle non-natural loops for now. *)
-include module type of Region_analysis_sig;;
-module Make(N:Node):sig
+module Make(N:Region_analysis_sig.Node):sig
(* Function computing from an entry abstract value the "after"
state, which is a map from each outgoing edge to its respective
value. *)
diff --git a/src/plugins/loop_analysis/region_analysis_sig.ml b/src/plugins/loop_analysis/region_analysis_sig.mli
similarity index 100%
rename from src/plugins/loop_analysis/region_analysis_sig.ml
rename to src/plugins/loop_analysis/region_analysis_sig.mli
diff --git a/src/plugins/loop_analysis/region_analysis_stmt.ml b/src/plugins/loop_analysis/region_analysis_stmt.ml
index b9db0a8032b..dad5e180654 100644
--- a/src/plugins/loop_analysis/region_analysis_stmt.ml
+++ b/src/plugins/loop_analysis/region_analysis_stmt.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Region_analysis
+open Region_analysis_sig
module type M = sig
val kf: Kernel_function.t
diff --git a/src/plugins/loop_analysis/region_analysis_stmt.mli b/src/plugins/loop_analysis/region_analysis_stmt.mli
index a52050d3e06..23b37e7dcb3 100644
--- a/src/plugins/loop_analysis/region_analysis_stmt.mli
+++ b/src/plugins/loop_analysis/region_analysis_stmt.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Region_analysis
+open Region_analysis_sig
open Cil_types
module type M = sig
--
GitLab