diff --git a/tests/misc/vis_spec.ml b/tests/misc/vis_spec.ml index a0a298fc83c5e21f12a5e219dbb514a2911935f4..d8d0b2b0373de8cdb41233441db0c85f0099395b 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 8357f1034bf3aebfbe78c33a077903a82744b797..5c2cd6c0ccbc488e12917a4b33ba866d09b1d65a 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 146c4fcdea2565fd2e443ac260cbc5a13ab574a6..964e4bd7e1546e51f9b1d0424ecc7e2fdec5d000 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 68cc157aee8fba6462543e5be9cf6bbb4ad72fb7..1ebbd226e9059736d7af1124fb3f44f65f4925b2 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