From d910cea4e9f3c4b9dee1db03b06e581d9e4a81cb Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 6 Sep 2023 17:54:24 +0200
Subject: [PATCH] Remove generic_funspec population, now populate is called
manually
---
src/kernel_internals/typing/ghost_accesses.ml | 2 +-
src/kernel_internals/typing/populate_spec.mli | 8 ++---
.../typing/translate_lightweight.ml | 2 +-
src/kernel_services/ast_data/annotations.ml | 29 +++++--------------
src/kernel_services/ast_data/annotations.mli | 14 ++++-----
.../ast_data/statuses_by_call.ml | 2 +-
src/kernel_services/ast_printing/printer.ml | 2 +-
src/kernel_services/ast_queries/file.ml | 8 -----
src/kernel_services/ast_queries/filecheck.ml | 2 +-
.../ast_queries/logic_parse_string.ml | 1 +
.../ast_transformations/clone.ml | 2 +-
.../ast_transformations/filter.ml | 4 +--
.../ast_transformations/inline.ml | 2 +-
.../plugin_entry_points/kernel.ml | 14 ---------
.../plugin_entry_points/kernel.mli | 3 --
src/kernel_services/visitors/visitor.ml | 25 ++++++++--------
src/plugins/aorai/aorai_visitors.ml | 1 +
src/plugins/aorai/data_for_aorai.ml | 2 +-
.../e-acsl/src/analyses/e_acsl_visitor.ml | 1 +
.../e-acsl/src/code_generator/injector.ml | 4 ++-
.../src/project_initializer/prepare_ast.ml | 4 +--
.../e-acsl/src/project_initializer/rtl.ml | 2 +-
src/plugins/eva/domains/cvalue/builtins.ml | 1 +
src/plugins/eva/engine/compute_functions.ml | 7 +++--
src/plugins/eva/engine/function_calls.ml | 5 +++-
src/plugins/eva/engine/recursion.ml | 10 +++----
src/plugins/eva/engine/transfer_logic.ml | 3 ++
src/plugins/eva/legacy/logic_inout.ml | 3 ++
src/plugins/markdown-report/md_gen.ml | 4 ++-
src/plugins/metrics/metrics_cilast.ml | 2 +-
src/plugins/metrics/metrics_coverage.ml | 2 +-
src/plugins/report/tests/report/one_hyp.ml | 1 +
.../report/tests/report/several_hyps.ml | 2 ++
src/plugins/wp/RefUsage.ml | 1 +
src/plugins/wp/RegionAnalysis.ml | 1 +
src/plugins/wp/StmtSemantics.ml | 2 ++
src/plugins/wp/cfgAnnot.ml | 9 ++++--
src/plugins/wp/cfgCalculus.ml | 1 +
src/plugins/wp/cfgGenerator.ml | 3 ++
src/plugins/wp/cfgInfos.ml | 10 ++++++-
src/plugins/wp/wpTarget.ml | 2 ++
tests/libc/check_const.ml | 2 +-
tests/misc/add_assigns.ml | 1 +
tests/misc/ensures.ml | 1 +
tests/misc/vis_spec.ml | 8 +++--
tests/spec/assigns_from_kf.ml | 5 +++-
tests/spec/expr_to_term.ml | 2 ++
tests/spec/non_ast_spec_copy.ml | 2 +-
tests/spec/pp_empty_spec.ml | 5 ++--
49 files changed, 121 insertions(+), 108 deletions(-)
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index 57fa079e8c3..aba019286b2 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -130,7 +130,7 @@ class visitor = object(self)
&& not (Kernel_function.has_definition kf)
then begin
let spec =
- try Annotations.funspec ~populate:false kf
+ try Annotations.funspec kf
with _ -> empty_funspec ()
in
if is_empty_funspec spec then self#bad_ghost_function kf
diff --git a/src/kernel_internals/typing/populate_spec.mli b/src/kernel_internals/typing/populate_spec.mli
index 74bada5d9c5..cf51410e75c 100644
--- a/src/kernel_internals/typing/populate_spec.mli
+++ b/src/kernel_internals/typing/populate_spec.mli
@@ -78,11 +78,11 @@ val register :
?status_terminates:status ->
string -> unit
-(** [populate_funspec ~do_body ?funspec kf] generates missing
- specifications for the [kf].
- By default ~do_body is false, meaning only specification of prototypes will
+(** [populate_funspec ~do_body ?funspec kf] generates missing specifications for
+ [kf].
+ By default [do_body] is false, meaning only specification of prototypes will
be generated.
- If None, [Annotations.funspec kf] will be used to get kf's funspec.
+ If [funspec] is None, [Annotations.funspec kf] will be used to get kf's funspec.
*)
val populate_funspec :
?do_body:bool -> ?funspec:funspec -> kernel_function -> clause list -> unit
diff --git a/src/kernel_internals/typing/translate_lightweight.ml b/src/kernel_internals/typing/translate_lightweight.ml
index 25366eb037c..7d6fadf10a9 100644
--- a/src/kernel_internals/typing/translate_lightweight.ml
+++ b/src/kernel_internals/typing/translate_lightweight.ml
@@ -193,7 +193,7 @@ class annotateFunFromDeclspec =
behavior.b_post_cond <- ens;
List.iter Property_status.register (ppt_ensures behavior);
in
- let spec = Annotations.funspec ~populate:false kf in
+ let spec = Annotations.funspec kf in
List.iter insert_spec spec.spec_behavior
in
object
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index dd0e4788566..d71a3451ea0 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -162,17 +162,6 @@ let () =
(** {2 Getting annotations} *)
(**************************************************************************)
-let populate_spec_ref = Extlib.mk_fun "Annotations.populate_spec"
-
-let populate_spec populate kf spec =
- match kf.fundec with
- | Definition _ -> false
- | Declaration _ ->
- if populate then begin
- !populate_spec_ref kf spec;
- end else
- false
-
let merge_from from1 from2 =
match from1, from2 with
| FromAny, FromAny -> FromAny
@@ -447,7 +436,7 @@ let register_funspec ?emitter ?force kf =
pre_register_funspec ?emitter ?force kf
exception No_funspec of Emitter.t
-let generic_funspec merge get ?emitter ?(populate=true) kf =
+let generic_funspec merge get ?emitter kf =
let merge tbl =
(* Kernel.feedback "Getting spec of function %a" Kf.pretty kf; *)
match emitter with
@@ -461,9 +450,7 @@ let generic_funspec merge get ?emitter ?(populate=true) kf =
merge spec s) tbl;
spec
in
- let spec = merged_spec () in
- let do_it = populate_spec populate kf spec in
- get (if do_it then merged_spec () else spec)
+ get (merged_spec ())
| Some e ->
try
let s = Emitter.Usable_emitter.Hashtbl.find tbl (Emitter.get e) in
@@ -479,12 +466,12 @@ let generic_funspec merge get ?emitter ?(populate=true) kf =
pre_register_funspec ~tbl kf;
merge tbl
-let funspec ?emitter ?populate kf =
- generic_funspec merge_funspec ?emitter ?populate (fun x -> x) kf
+let funspec ?emitter kf =
+ generic_funspec merge_funspec ?emitter (fun x -> x) kf
let has_funspec kf =
try
- not (Cil.is_empty_funspec (funspec ~populate:false kf))
+ not (Cil.is_empty_funspec (funspec kf))
with No_funspec _ -> false
(* Do not share behaviors with outside world if there's a single emitter. *)
@@ -1115,7 +1102,7 @@ let get_spec_e e kf ?stmt ?(active=[]) () =
let get_spec_all kf ?stmt ?(active=[]) () =
match stmt with
- | None -> funspec ~populate:false kf
+ | None -> funspec kf
| Some stmt ->
let filter = filter_stmt_spec active in
let spec = Cil.empty_funspec () in
@@ -1402,7 +1389,7 @@ let add_ensures e kf ?stmt ?active ?behavior l =
let get_full_spec kf ?stmt ?(behavior=[]) () =
match stmt with
| None ->
- (try funspec ~populate:false kf with Not_found -> Cil.empty_funspec())
+ (try funspec kf with Not_found -> Cil.empty_funspec())
| Some stmt ->
let filter a =
match a.annot_content with
@@ -1833,7 +1820,7 @@ let behavior_names_of_stmt_in_kf kf = match kf.fundec with
[]
let spec_function_behaviors kf =
- List.map (fun x -> x.b_name) (behaviors ~populate:false kf)
+ List.map (fun x -> x.b_name) (behaviors kf)
let all_function_behaviors kf =
behavior_names_of_stmt_in_kf kf @ spec_function_behaviors kf
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index f05e3dececf..d9cc123cbd1 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -62,7 +62,7 @@ val code_annot_emitter:
exception No_funspec of Emitter.t
val funspec:
- ?emitter:Emitter.t -> ?populate:bool -> kernel_function -> funspec
+ ?emitter:Emitter.t -> kernel_function -> funspec
(** Get the contract associated to the given function.
If [emitter] is specified, return only the annotations that
has been generated by this [emitter]. If [populate] is set to [true]
@@ -75,32 +75,31 @@ val has_funspec: kernel_function -> bool
@since 22.0-Titanium *)
val behaviors:
- ?emitter:Emitter.t -> ?populate:bool -> kernel_function -> funbehavior list
+ ?emitter:Emitter.t -> kernel_function -> funbehavior list
(** Get the behaviors clause of the contract associated to the given function.
Meaning of [emitter] and [populate] is similar to {!funspec}.
@raise No_funspec whenever the given function has no specification *)
val decreases:
- ?emitter:Emitter.t -> ?populate:bool -> kernel_function -> variant option
+ ?emitter:Emitter.t -> kernel_function -> variant option
(** If any, get the decrease clause of the contract associated to the given
function. Meaning of [emitter] and [populate] is similar to {!funspec}.
@raise No_funspec whenever the given function has no specification *)
val terminates:
- ?emitter:Emitter.t -> ?populate:bool -> kernel_function ->
- identified_predicate option
+ ?emitter:Emitter.t -> kernel_function -> identified_predicate option
(** If any, get the terminates clause of the contract associated to the given
function. Meaning of [emitter] and [populate] is similar to {!funspec}.
@raise No_funspec whenever the given function has no specification *)
val complete:
- ?emitter:Emitter.t -> ?populate:bool -> kernel_function -> string list list
+ ?emitter:Emitter.t -> kernel_function -> string list list
(** Get the complete behaviors clause of the contract associated to the given
function. Meaning of [emitter] and [populate] is similar to {!funspec}.
@raise No_funspec whenever the given function has no specification *)
val disjoint:
- ?emitter:Emitter.t -> ?populate:bool -> kernel_function -> string list list
+ ?emitter:Emitter.t -> kernel_function -> string list list
(** If any, get the disjoint behavior clause of the contract associated to the
given function. Meaning of [emitter] and [populate] is similar to
{!funspec}.
@@ -587,7 +586,6 @@ val global_state: State.t
(** {2 Internal stuff} *)
(**************************************************************************)
-val populate_spec_ref: (kernel_function -> funspec -> bool) ref
val unsafe_add_global: Emitter.t -> global_annotation -> unit
val register_funspec:
?emitter:Emitter.t -> ?force:bool -> kernel_function -> unit
diff --git a/src/kernel_services/ast_data/statuses_by_call.ml b/src/kernel_services/ast_data/statuses_by_call.ml
index 4d0628fa65c..5af0893cbc7 100644
--- a/src/kernel_services/ast_data/statuses_by_call.ml
+++ b/src/kernel_services/ast_data/statuses_by_call.ml
@@ -248,7 +248,7 @@ and add_call_precondition precondition call_precondition =
Property_status.logical_consequence preconditions_emitter precondition all
let fold_requires f kf acc =
- let bhvs = Annotations.behaviors ~populate:false kf in
+ let bhvs = Annotations.behaviors kf in
List.fold_right
(fun bhv acc -> List.fold_right (f bhv) bhv.b_requires acc) bhvs acc
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index 600da8008b6..5285e633a71 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -115,7 +115,7 @@ class printer_with_annot () = object (self)
super#may_be_skipped s && not (Annotations.has_code_annot s)
method private pretty_funspec fmt kf =
- let spec = Annotations.funspec ~populate:false kf in
+ let spec = Annotations.funspec kf in
self#opt_funspec fmt spec
method! private stmt_has_annot s = Annotations.has_code_annot s
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 36bb0e417a4..ebd8cc54651 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -1187,13 +1187,6 @@ let () =
constglobfold
syntactic_const_globals_substitution
-let populate_spec () =
- let add_spec kf =
- ignore @@ Populate_spec.populate_funspec ~force:false kf
- (Annotations.funspec ~populate:false kf)
- in
- Globals.Functions.iter add_spec
-
let prepare_cil_file ast =
Kernel.feedback ~level:2 "preparing the AST";
computeCFG ~clear_id:true ast;
@@ -1241,7 +1234,6 @@ let prepare_cil_file ast =
Filecheck.check_ast ~ast "AST after annotation registration"
end;
Transform_after_cleanup.apply ast;
- populate_spec () ;
(* reset tables depending on AST in case they have been computed during
the transformation. *)
Ast.set_file ast
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 893f231dc63..262a40268e8 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -269,7 +269,7 @@ module Base_checker = struct
"Body of %a is not shared between kernel function and AST"
Kernel_function.pretty kf;
return_stmt <- Some (Kernel_function.find_return kf);
- let spec = Annotations.funspec ~populate:false kf in
+ let spec = Annotations.funspec kf in
self#add_spec_behavior_names spec;
end else begin self#add_spec_behavior_names f.sspec; end;
labelled_stmt <- [];
diff --git a/src/kernel_services/ast_queries/logic_parse_string.ml b/src/kernel_services/ast_queries/logic_parse_string.ml
index a75626bd53c..c5ca8454232 100644
--- a/src/kernel_services/ast_queries/logic_parse_string.ml
+++ b/src/kernel_services/ast_queries/logic_parse_string.ml
@@ -146,6 +146,7 @@ let code_annot kf stmt s =
(function (_, Logic_ptree.Acode_annot (_,a)) -> Some a | _ -> None)
in
let parse pa =
+ Populate_spec.(populate_funspec kf [`Assigns]);
LT.code_annot
(Stmt.loc stmt)
(Logic_utils.get_behavior_names (Annotations.funspec kf))
diff --git a/src/kernel_services/ast_transformations/clone.ml b/src/kernel_services/ast_transformations/clone.ml
index 1c30cb22d59..1938854f0ad 100644
--- a/src/kernel_services/ast_transformations/clone.ml
+++ b/src/kernel_services/ast_transformations/clone.ml
@@ -36,7 +36,7 @@ let clone_function_definition old_kf =
let visitor = new Visitor.frama_c_refresh (Project.current()) in
let old_fundec = Kernel_function.get_definition old_kf in
let old_loc = Kernel_function.get_location old_kf in
- let old_funspec = Annotations.funspec ~populate:false old_kf in
+ let old_funspec = Annotations.funspec old_kf in
visitor#set_current_kf old_kf;
visitor#set_current_func old_fundec;
let new_fundec = Visitor.visitFramacFunction visitor old_fundec in
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index 7d01c6f8fb3..2542d8938c1 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -712,7 +712,7 @@ end = struct
Varinfo.Hashtbl.clear local_visible;
Varinfo.Hashtbl.add spec_table f.svar
(visitCilFunspec (self:>Cil.cilVisitor)
- (Annotations.funspec ~populate:false (Option.get self#current_kf)));
+ (Annotations.funspec (Option.get self#current_kf)));
SkipChildren
method private visit_pred p =
@@ -852,7 +852,7 @@ end = struct
self#get_filling_actions);
let res =
Cil.visitCilFunspec (self :> Cil.cilVisitor)
- (Annotations.funspec ~populate:false kf)
+ (Annotations.funspec kf)
in
let action () =
(* Replace the funspec copied by the default visitor, as
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 6a108374aac..773ad748a0c 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -118,7 +118,7 @@ let inline_call loc caller callee return args =
(Local_init (vi,AssignInit (SingleInit arg),loc))
in
let inits = List.map2 add_init fd.sformals args in
- let spec = Annotations.funspec ~populate:false callee in
+ let spec = Annotations.funspec callee in
if Cil.is_empty_funspec spec then begin
fd.sbody.blocals <- fd.sformals @ fd.sbody.blocals;
fd.sbody.bstmts <- inits @ fd.sbody.bstmts;
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index dd69b1d30bf..0cb56f3d6e2 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1455,22 +1455,8 @@ module DoCollapseCallCast =
and the lvalue it is assigned to."
end)
-
let () = Parameter_customize.set_group normalisation
let () = Parameter_customize.do_not_reset_on_copy ()
-module GenerateDefaultSpec =
- Bool
- (struct
- let module_name = "GenerateDefaultSpec"
- let option_name = "-generate-default-spec"
- let default = true
- let help = "Generates missing specifications according to options \
- -generated-spec-mode and -generated-spec-custom (activated \
- by default)."
- end)
-let () = Parameter_customize.set_group normalisation
-let () = Parameter_customize.do_not_reset_on_copy ()
-
module GeneratedSpecMode =
String
(struct
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 6b643f37c24..fec09bc71b5 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -556,9 +556,6 @@ module DoCollapseCallCast: Parameter_sig.Bool
This is false by default. Set to true to replicate the behavior
of CIL 1.3.5 and earlier. *)
-module GenerateDefaultSpec: Parameter_sig.Bool
-(** Behavior of option "-generate-default-spec". *)
-
module GeneratedSpecMode: Parameter_sig.String
(** Behavior of option "-generated-spec-mode". *)
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index 5bac5647dc5..0867c4460dc 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -185,7 +185,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
(* Ensures that we have a table associated to new_kf in Annotations. *)
add_queue
(fun () ->
- ignore (Annotations.behaviors ~populate:false new_kf));
+ ignore (Annotations.behaviors new_kf));
let module Fold =
struct
type 'a t =
@@ -331,7 +331,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
in
let register_annots b' f =
add_queue
- (fun () -> ignore (Annotations.behaviors ~populate:false new_kf));
+ (fun () -> ignore (Annotations.behaviors new_kf));
remove_and_add
(fun b -> b.b_requires)
Annotations.remove_requires
@@ -430,7 +430,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
in
Queue.add
(fun () ->
- ignore (Annotations.funspec ~populate:false new_kf))
+ ignore (Annotations.funspec new_kf))
self#get_filling_actions ;
let new_terminates =
Option.map
@@ -501,8 +501,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
in
let register_new_components new_spec =
let add_spec_components () =
- let populate = false in
- let new_behaviors = Annotations.behaviors ~populate new_kf in
+ let new_behaviors = Annotations.behaviors new_kf in
List.iter
(fun b ->
if
@@ -514,20 +513,20 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
Emitter.end_user new_kf [b]
end)
new_spec.spec_behavior;
- let new_complete = Annotations.complete ~populate new_kf in
+ let new_complete = Annotations.complete new_kf in
List.iter
(fun c ->
if not (List.memq c new_complete) then begin
Annotations.add_complete Emitter.end_user new_kf c
end)
new_spec.spec_complete_behaviors;
- let new_disjoint = Annotations.disjoint ~populate new_kf in
+ let new_disjoint = Annotations.disjoint new_kf in
List.iter
(fun d ->
if not (List.memq d new_disjoint) then
Annotations.add_disjoint Emitter.end_user new_kf d)
new_spec.spec_disjoint_behaviors;
- let new_terminates = Annotations.terminates ~populate new_kf in
+ let new_terminates = Annotations.terminates new_kf in
(match new_terminates, new_spec.spec_terminates with
| None, None -> ()
| Some _, None -> ()
@@ -542,7 +541,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
Kernel_function.pretty new_kf
Printer.pp_identified_predicate p1
Printer.pp_identified_predicate p2);
- let new_decreases = Annotations.decreases ~populate new_kf in
+ let new_decreases = Annotations.decreases new_kf in
(match new_decreases, new_spec.spec_variant with
| None, None -> ()
| Some _, None -> ()
@@ -673,7 +672,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
let get_spec () = match g with
| GFun _ | GFunDecl _ when Ast.is_def_or_last_decl g ->
let spec =
- Annotations.funspec ~populate:false (Option.get self#current_kf)
+ Annotations.funspec (Option.get self#current_kf)
in
Some (Cil.visitCilFunspec self#plain_copy_visitor spec)
| _ -> None
@@ -706,7 +705,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
(Kernel_function.get_vi new_kf)
then begin
let dft =
- Annotations.funspec ~populate:false new_kf
+ Annotations.funspec new_kf
in
let dft =
{ dft with spec_behavior = dft.spec_behavior }
@@ -715,7 +714,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
Globals.Functions.register new_kf;
Globals.Functions.replace_by_declaration spec v l;
(* Format.printf "registered spec:@\n%a@." Printer.pp_funspec
- (Annotations.funspec ~populate:false new_kf) *)
+ (Annotations.funspec new_kf) *)
end else begin
Globals.Functions.replace_by_declaration
(Cil.empty_funspec()) v l
@@ -767,7 +766,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
Globals.Functions.register new_kf;
let spec =
Option.value
- ~default:(Annotations.funspec ~populate:false new_kf)
+ ~default:(Annotations.funspec new_kf)
spec
in
Globals.Functions.replace_by_definition spec f l
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 0bea7e143fd..5c5b81dd863 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -883,6 +883,7 @@ class visit_adding_pre_post_from_buch treatloops =
method! vfunc f =
let my_kf = Option.get self#current_kf in
let vi = Kernel_function.get_vi my_kf in
+ Populate_spec.(populate_funspec my_kf [`Assigns]);
let spec = Annotations.funspec my_kf in
let loc = Kernel_function.get_location my_kf in
(match Aux_funcs.kind vi with
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 919b0cc253a..4d6d4a13a22 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -945,7 +945,7 @@ let type_cond needs_pebble metaenv env tr cond =
let b =
Option.map
(fun b ->
- let bhvs = Annotations.behaviors ~populate:false kf in
+ let bhvs = Annotations.behaviors kf in
try List.find (fun x -> x.b_name = b) bhvs
with Not_found ->
Aorai_option.abort "Function %a has no behavior named %s"
diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
index 2c91cecc4e2..206fb904e7a 100644
--- a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
+++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
@@ -438,6 +438,7 @@ class visitor cat
(* Analyze the funspec before visiting the first statement *)
if Annotations.has_funspec kf then begin
let old_kinstr_stmts = self#set_global_kinstr () in
+ Populate_spec.(populate_funspec kf [`Assigns]);
self#process_spec (Annotations.funspec kf);
self#reset_kinstr old_kinstr_stmts
end
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index c7c1ca187f0..960e1d79cb5 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -464,9 +464,11 @@ and inject_in_stmt env kf stmt =
let env = Translate_ats.for_stmt env kf stmt in
(* translate the precondition of the function *)
let env =
- if translate_pre_funspec then
+ if translate_pre_funspec then begin
+ Populate_spec.(populate_funspec kf [`Assigns]);
let funspec = Annotations.funspec kf in
Translate_annots.pre_funspec kf env funspec
+ end
else
env
in
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 50d2e39eadb..ba0d33bb564 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -621,7 +621,7 @@ let must_duplicate kf vi =
not (Functions.instrument kf)
||
(* or: *)
- ( let spec = Annotations.funspec ~populate:false kf in
+ ( let spec = Annotations.funspec kf in
(* it has a function contract *)
not (Cil.is_empty_funspec spec)
&& (* there are some annotations that might be treated *)
@@ -663,7 +663,7 @@ let prepare_global (globals, new_defs) = function
let new_def, new_decl =
dup_global
loc
- (Annotations.funspec ~populate:false kf)
+ (Annotations.funspec kf)
(Lazy.force sound_verdict_vi)
kf
vi
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index b865f4cace3..2f27d4cac9c 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -360,7 +360,7 @@ let get_formals_and_spec prj vi =
(fun vi ->
let kf = get_kf vi in
Kernel_function.get_formals kf,
- Annotations.funspec ~populate:false kf)
+ Annotations.funspec kf)
vi
(** Visitor to replace [varinfo] and [logic_info] leaves of an AST with
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index 48c2d53189c..3eec1afe396 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -118,6 +118,7 @@ let () =
(* Returns the specification of a builtin, used to evaluate preconditions
and to transfer the states of other domains. *)
let find_builtin_specification kf =
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
(* The specification can be empty if [kf] has a body but no specification,
in which case [Annotations.funspec] does not generate a specification.
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 59f8a8d9a4e..cee61d66501 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -45,7 +45,7 @@ let floats_ok () =
assert (0. < u && u < min_float)
let need_assigns kf =
- let spec = Annotations.funspec ~populate:false kf in
+ let spec = Annotations.funspec kf in
match Cil.find_default_behavior spec with
| None -> true
| Some bhv -> bhv.b_assigns = WritesAny
@@ -79,13 +79,13 @@ let plugins_ok () =
let generate_specs () =
let aux kf =
if need_assigns kf then begin
- let spec = Annotations.funspec ~populate:false kf in
+ let funspec = Annotations.funspec kf in
Self.warning "Generating potentially incorrect assigns \
for function '%a' for which option %s is set"
Kernel_function.pretty kf Parameters.UsePrototype.option_name;
(* The function populate_spec may emit a warning. Position a loc. *)
Cil.CurrentLoc.set (Kernel_function.get_location kf);
- ignore (!Annotations.populate_spec_ref kf spec)
+ Populate_spec.(populate_funspec ~funspec kf [`Assigns]);
end
in
Parameters.UsePrototype.iter aux
@@ -207,6 +207,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
apply_call_hooks call init_state `Reuse;
(* Evaluate the preconditions of kf, to update the statuses
at this call. *)
+ Populate_spec.(populate_funspec call.kf [`Assigns]);
let spec = Annotations.funspec call.kf in
if not (Eva_utils.skip_specifications call.kf) &&
Eval_annots.has_requires spec
diff --git a/src/plugins/eva/engine/function_calls.ml b/src/plugins/eva/engine/function_calls.ml
index bbc61c05b02..6a3dc5e207c 100644
--- a/src/plugins/eva/engine/function_calls.ml
+++ b/src/plugins/eva/engine/function_calls.ml
@@ -164,7 +164,10 @@ let analysis_target ~recursion_depth callsite kf =
| Declaration (_,_,_,_) -> `Spec (Annotations.funspec kf)
| Definition (def, _) ->
if Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
- then `Spec (Annotations.funspec kf)
+ then begin
+ Populate_spec.(populate_funspec kf [`Assigns]);
+ `Spec (Annotations.funspec kf)
+ end
else `Body (def, save_results def)
let define_analysis_target ?(recursion_depth = -1) callsite kf =
diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index b2fb66139b2..918905f490f 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/src/plugins/eva/engine/recursion.ml
@@ -50,7 +50,7 @@ let need_assigns funspec =
| Some bhv -> bhv.b_assigns = WritesAny
let get_spec kinstr kf =
- let funspec = Annotations.funspec ~populate:false kf in
+ let funspec = Annotations.funspec kf in
if List.for_all (fun b -> b.b_assigns = WritesAny) funspec.spec_behavior
then begin
Self.error ~current:true
@@ -66,7 +66,7 @@ let get_spec kinstr kf =
Kernel_function.pretty kf
Eva_utils.pp_callstack;
Cil.CurrentLoc.set (Kernel_function.get_location kf);
- ignore (!Annotations.populate_spec_ref kf funspec);
+ Populate_spec.(populate_funspec ~funspec kf [`Assigns]);
Annotations.funspec kf
end
else
@@ -84,8 +84,8 @@ let get_spec kinstr kf =
if need_assigns funspec
then
begin
- ignore (!Annotations.populate_spec_ref kf funspec);
- Annotations.funspec ~populate:false kf
+ Populate_spec.(populate_funspec ~funspec kf [`Assigns]);
+ Annotations.funspec kf
end
else funspec
in
@@ -96,7 +96,7 @@ let get_spec kinstr kf =
has no existing specification, generate (an incorrect) one, and warn
loudly. *)
let _spec_for_recursive_call kf =
- let initial_spec = Annotations.funspec ~populate:false kf in
+ let initial_spec = Annotations.funspec kf in
match Cil.find_default_behavior initial_spec with
| Some bhv when bhv.b_assigns <> WritesAny -> initial_spec
| _ ->
diff --git a/src/plugins/eva/engine/transfer_logic.ml b/src/plugins/eva/engine/transfer_logic.ml
index 319e14323b7..7de051e0183 100644
--- a/src/plugins/eva/engine/transfer_logic.ml
+++ b/src/plugins/eva/engine/transfer_logic.ml
@@ -285,6 +285,7 @@ module Make
Active_behaviors.create eval_predicate funspec
let create init_state kf =
+ Populate_spec.(populate_funspec kf [`Assigns]);
let funspec = Annotations.funspec kf in
create_from_spec init_state funspec
@@ -474,6 +475,7 @@ module Make
The postcondition of the global behavior is applied for each behavior,
to help reduce the final state. *)
let check_fct_postconditions kf ab kind ~pre_state ~post_states ~result =
+ Populate_spec.(populate_funspec kf [`Assigns]);
let behaviors = Annotations.behaviors kf in
let is_active = Active_behaviors.is_active ab in
let states =
@@ -520,6 +522,7 @@ module Make
into multiple states if the precondition contains disjunctions. *)
let check_fct_preconditions call_ki kf ab init_state =
let init_states = States.singleton init_state in
+ Populate_spec.(populate_funspec kf [`Assigns]);
let behaviors = Annotations.behaviors kf in
let is_active = Active_behaviors.is_active ab in
let states =
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index 6739454077a..8992d326150 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -46,6 +46,7 @@ let compute_term_deps stmt t =
let () = Logic_deps.compute_term_deps := compute_term_deps
let valid_behaviors kf state =
+ Populate_spec.(populate_funspec kf [`Assigns]);
let funspec = Annotations.funspec kf in
let eval_predicate pred =
match Eval_terms.(eval_predicate (env_pre_f ~pre:state ()) pred) with
@@ -210,6 +211,7 @@ let conv_status = function
let check_fct_assigns kf ab ~pre_state found_froms =
let open Locations in
let open Alarmset in
+ Populate_spec.(populate_funspec kf [`Assigns]);
let behaviors = Annotations.behaviors kf in
(* Under-approximation of the union. *)
let link zones = List.fold_left Zone.link Zone.bottom zones in
@@ -280,6 +282,7 @@ let check_fct_assigns kf ab ~pre_state found_froms =
in List.iter check_for_behavior behaviors
let verify_assigns kf ~pre froms =
+ Populate_spec.(populate_funspec kf [`Assigns]);
let funspec = Annotations.funspec kf in
let env = Eval_terms.env_pre_f ~pre () in
let eval_predicate pred =
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index 63d2550b21e..45c7b8d151d 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -113,7 +113,9 @@ let section_stubs env =
else
let intro = Markdown.text @@ Markdown.format
"`%s` has the following specification" s in
- let funspec = Markdown.codeblock ~lang:"acsl" "%a"
+ let funspec =
+ Populate_spec.(populate_funspec kf [`Assigns]);
+ Markdown.codeblock ~lang:"acsl" "%a"
Printer.pp_funspec (Annotations.funspec kf) in
Block ( intro @ funspec ) :: insert_remark env anchor
in
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 86674e7ae64..b41f94bd663 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -457,7 +457,7 @@ end
let get_filenames_in_funspec kf =
try
- let spec = Annotations.funspec ~populate:false kf in
+ let spec = Annotations.funspec kf in
Metrics_parameters.feedback ~dkey "looking for files in the spec of: %a"
Kernel_function.pretty kf;
List.fold_left (fun acc b ->
diff --git a/src/plugins/metrics/metrics_coverage.ml b/src/plugins/metrics/metrics_coverage.ml
index b1409748c28..da358e69770 100644
--- a/src/plugins/metrics/metrics_coverage.ml
+++ b/src/plugins/metrics/metrics_coverage.ml
@@ -35,7 +35,7 @@ class coverageAuxVisitor ~libc = object(self)
if Metrics_base.consider_function ~libc vi then begin
(* Visit the spec. There might be references to function pointers in
the assigns *)
- let spec = Annotations.funspec ~populate:false kf in
+ let spec = Annotations.funspec kf in
ignore (Visitor.visitFramacFunspec self spec);
end;
(try
diff --git a/src/plugins/report/tests/report/one_hyp.ml b/src/plugins/report/tests/report/one_hyp.ml
index e8c5b05c742..0f0fdb71769 100644
--- a/src/plugins/report/tests/report/one_hyp.ml
+++ b/src/plugins/report/tests/report/one_hyp.ml
@@ -44,6 +44,7 @@ let main () =
in
let ensures =
let kf = Globals.Functions.find_by_name "f" in
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
Property.ip_post_cond_of_spec kf Kglobal ~active:[] spec
in
diff --git a/src/plugins/report/tests/report/several_hyps.ml b/src/plugins/report/tests/report/several_hyps.ml
index 449f819dba7..840209facf6 100644
--- a/src/plugins/report/tests/report/several_hyps.ml
+++ b/src/plugins/report/tests/report/several_hyps.ml
@@ -45,11 +45,13 @@ let main () =
let hyps = [ g; h ] in
let ensures =
let kf = Globals.Functions.find_by_name "f" in
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
Property.ip_post_cond_of_spec kf Kglobal ~active:[] spec
in
let ensures2 =
let kf = Globals.Functions.find_by_name "f2" in
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
Property.ip_post_cond_of_spec kf Kglobal ~active:[] spec
in
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 958a36bfde7..7bfec3fc1b2 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -671,6 +671,7 @@ let cfun_spec env kf =
method !vterm t = update_spec_env (vterm env t)
end in
AssignsCompleteness.compute kf ;
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
ignore (Cil.visitCilFunspec (visitor:>Cil.cilVisitor) spec) ;
(* Partitioning the accesses of the spec for formals vs globals *)
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index 4d3d92aabe0..efd5084951a 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -35,6 +35,7 @@ let compute kf =
Wp.feedback ~ontty:`Transient "[region] Analyzing %a" Kf.pretty kf ;
let def = Kf.get_definition kf in
RegionAccess.cc_fundec map def ;
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
RegionAccess.cc_spec map spec ;
List.iter
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index 8511aa1adeb..218b169831d 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -341,6 +341,7 @@ struct
in
let cfg_contract env =
+ Populate_spec.(populate_funspec kf [`Assigns]);
spec env (Annotations.funspec kf)
in
@@ -764,6 +765,7 @@ struct
* close_out cout; *)
let binder = M.configure_ia autom in
let bind = binder.bind in
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
(* start and end nodes of pre(resp. post)-conditions. *)
let pres = { pre = Cfg.node (); post = Cfg.node () } in
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 5eb9442a2b6..1a50386edc6 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -159,6 +159,7 @@ let get_requires ~goal kf bhv =
let get_preconditions ~goal kf =
let module L = NormAtLabels in
let mk_pre = L.preproc_annot L.labels_fct_pre in
+ Populate_spec.(populate_funspec kf [`Assigns]);
List.map
(fun bhv ->
let p = Ast_info.behavior_precondition ~goal bhv in
@@ -167,6 +168,7 @@ let get_preconditions ~goal kf =
) (Annotations.behaviors kf)
let get_complete_behaviors kf =
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
let module L = NormAtLabels in
List.map
@@ -176,6 +178,7 @@ let get_complete_behaviors kf =
) spec.spec_complete_behaviors
let get_disjoint_behaviors kf =
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
let module L = NormAtLabels in
List.map
@@ -220,6 +223,7 @@ let get_terminates_clause kf =
in
let kf_vi = Kernel_function.get_vi kf in
let kf_name = Kernel_function.get_name kf in
+ Populate_spec.(populate_funspec kf [`Assigns]);
match Annotations.terminates kf with
| None
when Cil_builtins.is_builtin kf_vi
@@ -259,12 +263,12 @@ let check_variant_relation = function
let get_decreases_goal kf =
let defined t = WpPropId.mk_decrease_id kf Kglobal t, normalize_decreases t in
- match Annotations.decreases ~populate:false kf with
+ match Annotations.decreases kf with
| None -> None
| Some v -> check_variant_relation v ; Some (defined v)
let get_decreases_hyp kf =
- Annotations.decreases ~populate:false kf
+ Annotations.decreases kf
(* -------------------------------------------------------------------------- *)
(* --- Contracts --- *)
@@ -336,6 +340,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
let wpost : WpPropId.pred_info list ref = ref [] in
let wexit : WpPropId.pred_info list ref = ref [] in
let add w f x = match f x with Some y -> w := y :: !w | None -> () in
+ Populate_spec.(populate_funspec kf [`Assigns]);
let behaviors = Annotations.behaviors kf in
setup_preconditions kf ;
List.iter
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 929f23f336c..707e4d59273 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -51,6 +51,7 @@ type props = [ `All | `Names of string list | `PropId of Property.t ]
let default_requires mode kf =
if Cil.is_default_behavior mode.bhv then [] else
try
+ Populate_spec.(populate_funspec kf [`Assigns]);
let bhv = List.find Cil.is_default_behavior (Annotations.behaviors kf) in
CfgAnnot.get_requires ~goal:false kf bhv
with Not_found -> []
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index cdb7a436be0..9b30426bd5f 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -69,11 +69,13 @@ let empty_default_behavior : funbehavior = {
}
let default kf =
+ Populate_spec.(populate_funspec kf [`Assigns]);
match Annotations.behaviors kf with
| [] -> [empty_default_behavior]
| bhvs -> List.filter Cil.is_default_behavior bhvs
let select kf bnames =
+ Populate_spec.(populate_funspec kf [`Assigns]);
match Annotations.behaviors kf with
| [] -> if bnames = [] then [empty_default_behavior] else []
| bhvs -> if bnames = [] then bhvs else
@@ -97,6 +99,7 @@ let add_fun_task model pool ~kf ?infos ?bhvs ?target () =
let bhvs = match bhvs with
| Some bhvs -> bhvs
| None ->
+ Populate_spec.(populate_funspec kf [`Assigns]);
let bhvs = Annotations.behaviors kf in
if List.exists (Cil.is_default_behavior) bhvs then bhvs
else empty_default_behavior :: bhvs in
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 4a86f6250dd..e0418ab41ab 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -110,12 +110,14 @@ let selected_requires ~prop (b : Cil_types.funbehavior) =
List.exists (selected_precond ~prop) b.b_requires
let selected_call ~bhv ~prop kf =
+ Populate_spec.(populate_funspec kf [`Assigns]);
bhv = [] && List.exists (selected_requires ~prop) (Annotations.behaviors kf)
let selected_clause ~prop name getter kf =
getter kf <> [] && selected_name ~prop name
let selected_terminates ~prop kf =
+ Populate_spec.(populate_funspec kf [`Assigns]);
match Annotations.terminates kf with
| None ->
Wp_parameters.TerminatesDefinitions.get ()
@@ -125,6 +127,7 @@ let selected_terminates ~prop kf =
WpPropId.are_selected_names prop (tk_name :: tp_names)
let selected_decreases ~prop kf =
+ Populate_spec.(populate_funspec kf [`Assigns]);
match Annotations.decreases kf with
| None -> false
| Some (it, _) ->
@@ -133,6 +136,7 @@ let selected_decreases ~prop kf =
WpPropId.are_selected_names prop (tk_name :: tp_names)
let selected_disjoint_complete kf ~bhv ~prop =
+ Populate_spec.(populate_funspec kf [`Assigns]);
selected_default ~bhv &&
( selected_clause ~prop "@complete_behaviors" Annotations.complete kf ||
selected_clause ~prop "@disjoint_behaviors" Annotations.disjoint kf )
@@ -163,7 +167,10 @@ let collect_calls ~bhv ?(on_missing_calls=fun _ -> ()) kf stmt =
| None ->
let bhvs =
if bhv = []
- then List.map (fun b -> b.b_name) (Annotations.behaviors kf)
+ then begin
+ Populate_spec.(populate_funspec kf [`Assigns]);
+ List.map (fun b -> b.b_name) (Annotations.behaviors kf)
+ end
else bhv in
let calls =
List.fold_left
@@ -435,6 +442,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
no_variant_loops = Sset.empty ;
terminates_deps = Pset.empty ;
} in
+ Populate_spec.(populate_funspec kf [`Assigns]);
let behaviors = Annotations.behaviors kf in
(* Inits *)
if is_entry_point kf then
diff --git a/src/plugins/wp/wpTarget.ml b/src/plugins/wp/wpTarget.ml
index 06406e4834c..adfbefafdb3 100644
--- a/src/plugins/wp/wpTarget.ml
+++ b/src/plugins/wp/wpTarget.ml
@@ -102,6 +102,7 @@ let check_properties behaviors props kf =
in
let check_complete_disjoint kf kinstr =
try
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
let comp = ip_complete_of_spec kf kinstr ~active:[] spec in
let disj = ip_disjoint_of_spec kf kinstr ~active:[] spec in
@@ -125,6 +126,7 @@ let check_properties behaviors props kf =
in
let check_call stmt =
let check_callee kf =
+ Populate_spec.(populate_funspec kf [`Assigns]);
let kf_behaviors = Annotations.behaviors kf in
List.iter (check_bhv_requires kf Kglobal) kf_behaviors
in
diff --git a/tests/libc/check_const.ml b/tests/libc/check_const.ml
index 807c878a660..9be7b2b2cf3 100644
--- a/tests/libc/check_const.ml
+++ b/tests/libc/check_const.ml
@@ -62,7 +62,7 @@ let check_annot kf _ (a: identified_predicate) =
let check () =
let check_kf kf =
- let bhvs = Annotations.behaviors ~populate:false kf in
+ let bhvs = Annotations.behaviors kf in
List.iter (fun bhv ->
Annotations.iter_requires (check_annot kf) kf bhv.b_name) bhvs
in
diff --git a/tests/misc/add_assigns.ml b/tests/misc/add_assigns.ml
index 04d7bec1b14..f3d3ad760a8 100644
--- a/tests/misc/add_assigns.ml
+++ b/tests/misc/add_assigns.ml
@@ -22,6 +22,7 @@ let main () =
let bhv = Cil.mk_behavior ~assigns () in
Annotations.add_behaviors emitter kf [bhv];
let bhv =
+ Populate_spec.(populate_funspec kf [`Assigns]);
List.find
(fun b -> b.b_name = Cil.default_behavior_name)
(Annotations.behaviors kf)
diff --git a/tests/misc/ensures.ml b/tests/misc/ensures.ml
index 56cb3e03cc2..93eaaed8c25 100644
--- a/tests/misc/ensures.ml
+++ b/tests/misc/ensures.ml
@@ -6,6 +6,7 @@ let run () =
Globals.Functions.iter
(fun kf ->
let kf_name = Kernel_function.get_name kf in
+ Populate_spec.(populate_funspec kf [`Assigns]);
let spec = Annotations.funspec kf in
let ip = Property.ip_of_spec kf Kglobal ~active:[] spec in
List.iter
diff --git a/tests/misc/vis_spec.ml b/tests/misc/vis_spec.ml
index 19a8ae65685..fa9afd7df9d 100644
--- a/tests/misc/vis_spec.ml
+++ b/tests/misc/vis_spec.ml
@@ -10,9 +10,11 @@ class pathcrawlerVisitor prj =
Format.printf "@[Funspec of %s is@ @['%a'@]@ through visitor@]@."
fundec.svar.vname
Printer.pp_funspec fundec.sspec;
+ let kf = Globals.Functions.get fundec.svar in
+ Populate_spec.(populate_funspec kf [`Assigns]);
Format.printf "@[It is@ @['%a'@]@ through get_spec@]@."
Printer.pp_funspec
- (Annotations.funspec (Globals.Functions.get fundec.svar));
+ (Annotations.funspec kf);
DoChildren
method! vspec sp =
@@ -23,9 +25,11 @@ class pathcrawlerVisitor prj =
Format.printf "@[Funspec of %s is@ @['%a'@]@ through visitor@]@."
fundec.svar.vname
Printer.pp_funspec sp;
+ let kf = Globals.Functions.get fundec.svar in
+ Populate_spec.(populate_funspec kf [`Assigns]);
Format.printf "@[It is@ @['%a'@]@ through get_spec@]@."
Printer.pp_funspec
- (Annotations.funspec (Globals.Functions.get fundec.svar));
+ (Annotations.funspec kf);
| None ->
Format.printf "@[Function prototype;@ Funspec is@ @['%a'@]@]@."
Printer.pp_funspec sp;
diff --git a/tests/spec/assigns_from_kf.ml b/tests/spec/assigns_from_kf.ml
index d0c1e3965c8..5c18173bfc8 100644
--- a/tests/spec/assigns_from_kf.ml
+++ b/tests/spec/assigns_from_kf.ml
@@ -1,4 +1,7 @@
let run () =
- Globals.Functions.iter (fun kf -> ignore (Annotations.funspec kf))
+ Globals.Functions.iter (fun kf ->
+ Populate_spec.(populate_funspec kf [`Assigns]);
+ ignore (Annotations.funspec kf)
+ )
let () = Db.Main.extend run
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index c767a53b710..6a6df0f28f9 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -50,6 +50,7 @@ let treat_fct check fct =
| _ -> false)
stmts
in
+ Populate_spec.(populate_funspec fct [`Assigns]);
let ensures = (List.hd (Annotations.funspec fct).spec_behavior).b_post_cond in
let ensures = List.filter (fun (kind,_) -> kind = Normal) ensures in
(* A bit fragile, but should do the trick as long as the test itself does
@@ -69,6 +70,7 @@ let treat_fct_pred fct =
(fun x -> match x.skind with Instr(Call _) -> true | _ -> false)
stmts
in
+ Populate_spec.(populate_funspec fct [`Assigns]);
let ensures = (List.hd (Annotations.funspec fct).spec_behavior).b_post_cond in
let ensures = List.filter (fun (kind,_) -> kind = Normal) ensures in
if List.length stmts <> List.length ensures then
diff --git a/tests/spec/non_ast_spec_copy.ml b/tests/spec/non_ast_spec_copy.ml
index 03faef2019e..6c97f210601 100644
--- a/tests/spec/non_ast_spec_copy.ml
+++ b/tests/spec/non_ast_spec_copy.ml
@@ -3,7 +3,7 @@ let add_terminates_true _ =
Logic_const.(new_predicate { ptrue with pred_loc })
in
let add_terminates kf =
- if Annotations.terminates ~populate:false kf = None then
+ if Annotations.terminates kf = None then
Annotations.add_terminates
Emitter.kernel kf (terminates @@ Kernel_function.get_location kf)
in
diff --git a/tests/spec/pp_empty_spec.ml b/tests/spec/pp_empty_spec.ml
index 44d43d49c60..220c1774a2c 100644
--- a/tests/spec/pp_empty_spec.ml
+++ b/tests/spec/pp_empty_spec.ml
@@ -1,6 +1,5 @@
let e = Emitter.create "foo" [ Emitter.Funspec ] ~correctness:[] ~tuning:[]
let emitter = e
-let populate = false
let run () =
let () = Ast.compute () in
@@ -11,7 +10,7 @@ let run () =
e main [ Logic_const.new_predicate Logic_const.ptrue];
File.pretty_ast();
Annotations.remove_behavior
- e main (List.hd (Annotations.behaviors ~populate ~emitter main));
+ e main (List.hd (Annotations.behaviors ~emitter main));
File.pretty_ast();
Annotations.add_ensures e main [];
File.pretty_ast();
@@ -30,7 +29,7 @@ let run () =
Annotations.add_complete e main [behavior];
Annotations.add_disjoint e main [behavior];
Annotations.remove_behavior_components e main
- (List.hd (Annotations.behaviors ~populate ~emitter main));
+ (List.hd (Annotations.behaviors ~emitter main));
File.pretty_ast()
let () = Db.Main.extend run
--
GitLab