diff --git a/headers/header_spec.txt b/headers/header_spec.txt index cea13556cb6d26cec2497fb7d12d7f7db31969f9..d6a09d8640603e516ed054bd874cf9f86c8676be 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 74a6af00dbb2f68843f0feba4e28737dba0145cc..4cb7ceebdc781357e9221147bad002aae4d4c284 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 b97bd62b23f89ccc3695b52442ae65d1584996bb..43a3fd5b4913cfa2ccb8e7653694cbabe38e1ed2 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 c04f9f6ec334804ad68163320611d5063f7fe9d4..2906d0e5fe3eb7d5101891ff8b94b3155d407df3 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 6b4feeb6c8143b74197eb1da945f934e44d824e9..02a957af9f4d8cce3980f451301b6a7d1c4fdc32 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 b9db0a8032b4b90af9badd2ef66b37bdefa0131c..dad5e1806545d018aeef682a81724486d3c88b5e 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 a52050d3e067bab4e2d7c3e67f51a4dc966371c2..23b37e7dcb3fab00600ecebe707e02dca580c616 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