diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index 57fa079e8c3e3ce473a329cdd0372cc2412d0847..aba019286b2148db0fc9d9689ff377d4bc3298dc 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 74bada5d9c51718660a4e10b77dc003c80b35ae1..cf51410e75cee097a9abdadfeabf95ac08279319 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 25366eb037c867d84c112c4515a8329e36a29909..7d6fadf10a93d7f086db4f8a290e8fdc364f098c 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 dd0e4788566acfa3f01b63666411ace2de1381a4..d71a3451ea0bc44473285ec1e78e8341ca70b225 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 f05e3dececf4db420c5163b7595a344c15779a65..d9cc123cbd1d200614ae82f711f28f87015c450e 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 4d0628fa65ca5d099f85b41e83a47980ebcb31e9..5af0893cbc75ac15af59b33abd24af7ced016b96 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 600da8008b64babc825792d2a6027720c97e0f41..5285e633a715d7e2ae47ef870b178601bbe4da6f 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 36bb0e417a434e938b8c589cf42f5ddbe3d2241d..ebd8cc54651568285dd359589530d2f8236f8b3a 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 893f231dc637b9f83fc6fba37df70c36d5ab9eb4..262a40268e873206e5d593f5b673c4280092ad51 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 a75626bd53c6f3927ca95be6d93e1c7e40faa12e..c5ca8454232fb1aaa0e7514ea39f65ac728ae0c4 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 1c30cb22d59682f018d79ad5141e3c1a8781887f..1938854f0ad671a9587ccce575c36e19326c4181 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 7d01c6f8fb3cf6ecff55301b564080b793e4e1ec..2542d8938c1255addaca43f7014357a57a8ebe8a 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 6a108374aac24ab325dcfdfe8127b59886ec5777..773ad748a0c8c9b56107bf18c0084644a9ac284a 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 dd69b1d30bfe6cbdbb555505340294b19e8fa558..0cb56f3d6e2c7442de5c8c37c2ddcbdc3262c99c 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 6b643f37c248656b00275935312a1f8375941e60..fec09bc71b5a023d9db139d8250e1519c2d1e772 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 5bac5647dc570fc72cfdd9c632fe0fcbeae877ae..0867c4460dc40a09f8bc36da4bb02a3613279a59 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 0bea7e143fd55b4ed176b4e176013be0832326a8..5c5b81dd8637462a5e8488948f410b55d63d4409 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 919b0cc253acadb481fc44a9495fe281ec351663..4d6d4a13a2290a5a03cdef736827687c43a4eab6 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 2c91cecc4e2310f38de7669f03e825da9fc33f0f..206fb904e7a8866847551e0b5536b4b7fe7332ee 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 c7c1ca187f02906639685c13bf64c468d6cbb9d9..960e1d79cb5658576b7c7477da82e33c4a3457e7 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 50d2e39eadb9675027c459c8d3cb73d41f5dc295..ba0d33bb5641c02b1f7d7b44d8b626528274a73e 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 b865f4cace3616d24cf2848f67f3788240e5b25c..2f27d4cac9ca8eb8b2fe02c005443631d965b7f7 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 48c2d53189c0e07471eee40242001f04947522c8..3eec1afe396bb51794f6b0083937f6f67159f154 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 59f8a8d9a4e6c3e74a00fbc6427d09371995da74..cee61d665015fadda66fb50ead463274f39c2985 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 bbc61c05b0217eed796622029e61d10e6f2f6b1b..6a3dc5e207cd45f545eb91534d4165bc5135d22d 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 b2fb66139b2ce3db51094c6f76ebd585d7d11ac3..918905f490f8b6b4f39fe349e80a2f7ae1e727fe 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 319e14323b77fbbfcce9e987daf8febd6c7d10b6..7de051e01837b3cd8dcb7245c18fcf89a2c2c705 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 6739454077a4edb23a034a14bd1ab6582be8bea6..8992d326150e9cbc51e53a1a066ba7dd889fa881 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 63d2550b21e875969100aa46c756848d57b3c121..45c7b8d151d54b38d06c136b85c0ca250df673ef 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 86674e7ae64dd6b2254605da867bba40f5ec2450..b41f94bd66328586891891cc561ee6fac25a6ab8 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 b1409748c28d4ee57772253c5e49615a1c83756e..da358e697703fddfc6fd79c918593dfc433726a8 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 e8c5b05c742e6e397fb98694cafe65358a78b6e8..0f0fdb717691f5e5eb7e27bf69ed6dd7d8dbab9a 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 449f819dba78753b829f2139ba624e7554dcb2fb..840209facf650919fc61c4f7c2b7b7bd2af1e08c 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 958a36bfde7edcb1c54dda27b20b8cd1118248b0..7bfec3fc1b2a2dc8819b765fd73bf7208bf4a17e 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 4d3d92aabe00b1e3360eaa070efc675199527eaf..efd5084951a6eb277f79b82be240e0c1aaa6b9dd 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 8511aa1adebc7e091e867dd4df54d7c54b472d9f..218b169831d1a68b9df68c657c7cd6090660f773 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 5eb9442a2b603221781c6716b14af5620a0c5355..1a50386edc66f98cdc205bd07f27276f9daa7a01 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 929f23f336cabf6f3b09b12e680adb5f47b56f09..707e4d59273ccaf41c3d078a6b9c7c3f32081c1e 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 cdb7a436be01dad5c49a6d97c8583dd3ae8f4ec8..9b30426bd5f264c2eaedf6fd4fa38d77b8a4d11f 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 4a86f6250ddc2b0dd7e07b62d1a28d694217bd52..e0418ab41abb598de5a6b51528da50e6f255eba3 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 06406e4834c864bdfec40b4b1611e2a3b606fea5..adfbefafdb3d5024f9dda48ef7ba1407fc407744 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 807c878a6602a9517375fea1b008ffec61cff2d7..9be7b2b2cf3ab2debf77a764ef0d4fe04f02eecc 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 04d7bec1b147135f8b102a33365da9196a1c918f..f3d3ad760a8fe4eef691aba1cc0b86b626918a46 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 56cb3e03cc2e0c4d4288d24001b22ecc6540c96a..93eaaed8c252ee778a3783cd3791cfd7f7a277f4 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 19a8ae656851850588a386cfd5640ebaf34f5bdc..fa9afd7df9d662272abca93b3bf823aaeeda6bb2 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 d0c1e3965c83412df495adc03bcd88a623f2a509..5c18173bfc8a1429ceba93d949447abca0f99ad9 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 c767a53b7108b0af8cb19eb460eb40c16729da14..6a6df0f28f965c94d49477b7b8f48c6390f98870 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 03faef2019ec0970de6c518e0e11b08d5f5a7782..6c97f210601285a7e06ac810fb1790421333d399 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 44d43d49c608c905cabfd37e5b05f25ceb60bf7d..220c1774a2c1ca3265ff87578f56edb13604456f 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