diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unfold_loops.ml similarity index 99% rename from src/kernel_internals/typing/unroll_loops.ml rename to src/kernel_internals/typing/unfold_loops.ml index 6357d6e25cdd60b5e8168ed55d2ab7d94e18ab37..60d3ede0535983b5f740fc36331e4e246e1e16f6 100644 --- a/src/kernel_internals/typing/unroll_loops.ml +++ b/src/kernel_internals/typing/unfold_loops.ml @@ -738,18 +738,18 @@ let apply_transformation ?(force=true) nb file = (* Performs and closes all syntactic transformations *) let compute file = - let nb = Kernel.UnrollingLevel.get () in - let force = Kernel.UnrollingForce.get () in + let nb = Kernel.UnfoldingLevel.get () in + let force = Kernel.UnfoldingForce.get () in apply_transformation ~force nb file -let unroll_transform = +let transform = File.register_code_transformation_category "loop unfolding" let () = File.add_code_transformation_after_cleanup - ~deps:[(module Kernel.UnrollingLevel:Parameter_sig.S); - (module Kernel.UnrollingForce:Parameter_sig.S)] - unroll_transform compute + ~deps:[(module Kernel.UnfoldingLevel:Parameter_sig.S); + (module Kernel.UnfoldingForce:Parameter_sig.S)] + transform compute let unroll_typer (ctxt: Logic_typing.typing_context) (_loc:location) args = let open Logic_typing in diff --git a/src/kernel_internals/typing/unroll_loops.mli b/src/kernel_internals/typing/unfold_loops.mli similarity index 92% rename from src/kernel_internals/typing/unroll_loops.mli rename to src/kernel_internals/typing/unfold_loops.mli index 2f2c4a12fe61c76b562303f37a7f0dad1ea60d0d..a078e24300671da75cbb351bc43ae7fe759b6102 100644 --- a/src/kernel_internals/typing/unroll_loops.mli +++ b/src/kernel_internals/typing/unfold_loops.mli @@ -20,14 +20,14 @@ (* *) (**************************************************************************) -(** Syntactic loop unrolling. +(** Syntactic loop unfolding. Uses code transformation hook mechanism (after-cleanup phase) of {!File} and exports nothing. - Name of the transformation is "loop unrolling" + Name of the transformation is "loop unfolding" *) -val unroll_transform: File.code_transformation_category +val transform: File.code_transformation_category (* Local Variables: diff --git a/src/kernel_services/ast_data/ast.ml b/src/kernel_services/ast_data/ast.ml index 0efd2a914145390064e50e7cec3d46b5cf62188d..5dbe5309e22766f5b5793b08ac3550a6761d88c8 100644 --- a/src/kernel_services/ast_data/ast.ml +++ b/src/kernel_services/ast_data/ast.ml @@ -38,7 +38,7 @@ include Kernel.ReadAnnot.self; Kernel.PreprocessAnnot.self; Kernel.Files.self; - Kernel.UnrollingLevel.self; + Kernel.UnfoldingLevel.self; Kernel.Keep_unused_specified_functions.self; Kernel.Keep_unused_types.self; Cil.selfFormalsDecl ] diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 3ff75f40f3f26a1cf725b91259b5698966c22d39..73cf18ce7ce6c6d819a0edfd36438dda468d6fee 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -1268,26 +1268,26 @@ module JsonCompilationDatabase = let normalisation = add_group "Customizing Normalization" let () = Parameter_customize.set_group normalisation -module UnrollingLevel = +module UnfoldingLevel = Zero (struct - let module_name = "UnrollingLevel" + let module_name = "UnfoldingLevel" let option_name = "-ulevel" let arg_name = "l" let help = - "unroll loops n times (defaults to 0) before analyzes. \ - A negative value hides UNROLL loop pragmas." + "unfold loops n times (defaults to 0) before analyzes. \ + A negative value hides loop unfold annotations." end) let () = Parameter_customize.set_group normalisation -module UnrollingForce = +module UnfoldingForce = Bool (struct - let module_name = "UnrollingForce" + let module_name = "UnfoldingForce" let default = false let option_name = "-ulevel-force" let help = - "ignore loop unfold \"done\" specifications (force unrolling)." + "ignore loop unfold \"done\" specifications (force unfolding)." end) let () = Parameter_customize.set_group normalisation diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli index 8d4f1b47e79dd226d3e29c18508bedf45e474369..2e8856d2e52a1be2828459e7d8946faeacd7d2f3 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -438,10 +438,10 @@ module Set_project_as_default: Parameter_sig.Bool (** {2 Customizing Normalization and parsing} *) (* ************************************************************************* *) -module UnrollingLevel: Parameter_sig.Int +module UnfoldingLevel: Parameter_sig.Int (** Behavior of option "-ulevel" *) -module UnrollingForce: Parameter_sig.Bool +module UnfoldingForce: Parameter_sig.Bool (** Behavior of option "-ulevel-force" @since Neon-20140301 *)