From f9b178187faf1b1e66ce5a97b63b8887f69f1281 Mon Sep 17 00:00:00 2001 From: Thibault Martin <thi.martin.pro@pm.me> Date: Thu, 5 Oct 2023 16:04:26 +0200 Subject: [PATCH] Rename get_spec to generate_spec --- tests/misc/vis_spec.ml | 7 +++---- tests/spec/default_spec_combine.ml | 7 +++---- tests/spec/default_spec_custom.ml | 7 +++---- tests/spec/default_spec_mode.ml | 4 ++-- 4 files changed, 11 insertions(+), 14 deletions(-) diff --git a/tests/misc/vis_spec.ml b/tests/misc/vis_spec.ml index a0a298fc83c..d8d0b2b0373 100644 --- a/tests/misc/vis_spec.ml +++ b/tests/misc/vis_spec.ml @@ -36,11 +36,10 @@ class pathcrawlerVisitor prj = end let startup () = - let open Populate_spec in - let get_spec kf = - populate_funspec ~do_body:true kf [`Exits] + let generate_spec kf = + Populate_spec.populate_funspec ~do_body:true kf [`Exits] in - Globals.Functions.iter get_spec; + Globals.Functions.iter generate_spec; Format.printf "Starting visit@."; let prj = File.create_project_from_visitor "pcanalyzer" (fun prj -> new pathcrawlerVisitor prj) diff --git a/tests/spec/default_spec_combine.ml b/tests/spec/default_spec_combine.ml index 8357f1034bf..5c2cd6c0ccb 100644 --- a/tests/spec/default_spec_combine.ml +++ b/tests/spec/default_spec_combine.ml @@ -12,11 +12,10 @@ let gen_allocates _ _ = FreeAllocAny let status_allocates = Property_status.Dont_know let run () = - let open Populate_spec in - let get_spec kf = - populate_funspec kf [`Exits; `Assigns; `Requires; `Allocates] + let generate_spec kf = + Populate_spec.populate_funspec kf [`Exits; `Assigns; `Requires; `Allocates] in - Globals.Functions.iter get_spec + Globals.Functions.iter generate_spec let populate () = Format.printf "Registering an mode that does nothing@."; diff --git a/tests/spec/default_spec_custom.ml b/tests/spec/default_spec_custom.ml index 146c4fcdea2..964e4bd7e15 100644 --- a/tests/spec/default_spec_custom.ml +++ b/tests/spec/default_spec_custom.ml @@ -27,12 +27,11 @@ let status_allocates = Property_status.Dont_know let status_terminates = Property_status.Dont_know let run () = - let open Populate_spec in - let get_spec kf = - populate_funspec ~do_body:true kf + let generate_spec kf = + Populate_spec.populate_funspec ~do_body:true kf [`Exits; `Assigns; `Requires; `Allocates; `Terminates] in - Globals.Functions.iter get_spec + Globals.Functions.iter generate_spec let populate () = Format.printf "Registering an empty spec generation mode@."; diff --git a/tests/spec/default_spec_mode.ml b/tests/spec/default_spec_mode.ml index 68cc157aee8..1ebbd226e90 100644 --- a/tests/spec/default_spec_mode.ml +++ b/tests/spec/default_spec_mode.ml @@ -1,6 +1,6 @@ let run () = let open Populate_spec in - let get_spec kf = + let generate_spec kf = let funspec = Annotations.funspec kf in populate_funspec ~do_body:true kf [`Exits]; (* Populates assigns using old deprecated API function. *) @@ -13,7 +13,7 @@ let run () = populate_funspec ~do_body:true kf [`Exits; `Assigns; `Requires; `Allocates; `Terminates] in - Globals.Functions.iter get_spec + Globals.Functions.iter generate_spec [@@ warning "-3"] let () = Db.Main.extend run -- GitLab