[LoopAnalysis] Renames region_analysis_sig as a .mli interface file.

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

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
 

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

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

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. *)

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

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