diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
index 7025db38a3d861520ef5a8fca21fb4f43a6a3d25..eee32358838c1a1a25af908def2d3d1a904b2c72 100755
--- a/share/analysis-scripts/make_wrapper.py
+++ b/share/analysis-scripts/make_wrapper.py
@@ -87,7 +87,7 @@ with subprocess.Popen(cmd_list, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
else:
break
-re_missing_spec = re.compile("Neither code nor specification for function ([^,]+),")
+re_missing_spec = re.compile("Neither code nor (specification|[^ ]+ assigns clause) for function ([^,]+),")
re_recursive_call_start = re.compile("detected recursive call")
re_recursive_call_stack_start = re.compile(r"^\s+stack:")
re_recursive_call_stack_end = re.compile(r"^\[")
@@ -134,7 +134,8 @@ for line in lines:
assert False
match = re_missing_spec.search(line)
if match:
- fname = match.group(1)
+ spec_kind = match.group(1)
+ fname = match.group(2)
def _action(fname):
out = subprocess.Popen(
@@ -174,7 +175,9 @@ for line in lines:
print("Find the sources defining it and add them, " + "or provide a stub.")
tip = {
- "message": "Found function with missing spec: "
+ "message": "Found function with missing "
+ + spec_kind
+ + ": "
+ fname
+ "\n"
+ " Looking for files defining it...",
diff --git a/share/libc/assert.h b/share/libc/assert.h
index 26ee575269c86e3c11193f565b7f4376feaab5a4..0c4f0639509be1c43594a2ee2673bc7cab594430 100644
--- a/share/libc/assert.h
+++ b/share/libc/assert.h
@@ -29,7 +29,6 @@ __BEGIN_DECLS
/*@
requires nonnull_c: c != 0;
- terminates c != 0;
assigns \nothing;
*/
extern void __FC_assert(int c, const char* file, int line, const char*expr);
@@ -42,7 +41,7 @@ __POP_FC_STDLIB
#endif
#undef assert
-#ifdef NDEBUG
+#ifdef NDEBUG
#define assert(ignore) ((void)0)
#else
#ifndef __FRAMAC__
diff --git a/src/kernel_internals/typing/infer_annotations.ml b/src/kernel_internals/typing/infer_annotations.ml
index b6f2e39f836b07024ebfa3d7c0ebc93b4c31c370..568b2da42b83d1a254d92f98ee554bbb67209e82 100644
--- a/src/kernel_internals/typing/infer_annotations.ml
+++ b/src/kernel_internals/typing/infer_annotations.ml
@@ -226,7 +226,8 @@ let populate_funspec_aux kf spec =
let warn_if_not_builtin explicit_name name orig_name =
if not (is_frama_c_builtin name) then
Kernel.warning ~once:true ~current:true
- "No code nor %s assigns clause for function %a, \
+ ~wkey:Kernel.wkey_missing_spec
+ "Neither code nor %s assigns clause for function %a, \
generating default assigns from the %s"
explicit_name Kernel_function.pretty kf orig_name
in
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index edbda3e42290c18d8bf0028c3abc51d7d847b384..5bcae638d57136b9d5ad259836ec865c7cae6e11 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -256,14 +256,15 @@ let merge_behaviors fresh old =
let merge_variant fresh old = match fresh.spec_variant, old.spec_variant with
| _, None -> ()
- | Some _, Some _ -> assert false
- | None, (Some _ as v) -> fresh.spec_variant <- v
+ | Some f, Some o when not @@ Logic_utils.is_same_variant f o -> assert false
+ | _, (Some _ as v) -> fresh.spec_variant <- v
let merge_terminates fresh old =
match fresh.spec_terminates, old.spec_terminates with
| _, None -> ()
- | Some _, Some _ -> assert false
- | None, (Some _ as v) -> fresh.spec_terminates <- v
+ | Some f, Some o when not @@ Logic_utils.is_same_identified_predicate f o ->
+ assert false
+ | _, (Some _ as v) -> fresh.spec_terminates <- v
let merge_complete fresh old =
fresh.spec_complete_behaviors <-
@@ -290,6 +291,8 @@ module Behavior_set_map = Stdlib.Map.Make(Datatype.String.Set)
let is_same_behavior_set l1 l2 =
Datatype.String.Set.(equal (of_list l1) (of_list l2))
+let is_same_behavior b1 b2 = b1.b_name = b2.b_name
+
let merge_annots_emitters extract merge make annots =
let merge_same_bhvs bhvs (ca,a,e) acc =
let elt =
@@ -758,6 +761,215 @@ let remove_code_annot_internal e ?(remove_statuses=true) ?kf stmt ca =
(* annotation not registered *)
()
+
+(**************************************************************************)
+(** {2 Removing annotations} *)
+(**************************************************************************)
+
+(* If this function gets exported, please turn e into an Emitter.t *)
+let remove_model_field (e:Usable_emitter.t) m =
+ try
+ let ty = m.mi_base_type in
+ let h = Model_fields.find ty in
+ let l = Usable_emitter.Hashtbl.find h e in
+ let l' =
+ List.filter (fun x -> not (Cil_datatype.Model_info.equal x m)) l
+ in
+ Usable_emitter.Hashtbl.replace h e l';
+ Model_fields.apply_hooks_on_remove e ty l'
+ with Not_found ->
+ ()
+
+let remove_global e a =
+ try
+ let e = Emitter.get e in
+ let h = Globals.find a in
+ Usable_emitter.Hashtbl.iter
+ (fun e' () ->
+ if Emitter.Usable_emitter.equal e e' then begin
+ Globals.remove a;
+ (match a with
+ | Dmodel_annot (m,_) -> remove_model_field e m
+ | _ -> ());
+ let file = Ast.get () in
+ file.globals <-
+ List.filter
+ (fun a' ->
+ not (Global.equal (GAnnot(a, Global_annotation.loc a)) a'))
+ file.globals;
+ Globals.apply_hooks_on_remove e a ()
+ end)
+ h;
+ with Not_found ->
+ ()
+
+let remove_in_funspec e kf set_spec =
+ try
+ let tbl = Funspecs.find kf in
+ let e = Emitter.get e in
+ try
+ let spec = Emitter.Usable_emitter.Hashtbl.find tbl e in
+ (* Format.printf "Known specs for %a@." Kf.pretty kf;*)
+ (* Emitter.Usable_emitter.Hashtbl.iter
+ (fun e spec ->
+ Format.printf "For emitter %a: %a@."
+ Emitter.Usable_emitter.pretty e
+ Cil_printer.pp_funspec spec) tbl; *)
+ set_spec spec tbl
+ with Not_found -> ()
+ with Not_found ->
+ assert false
+
+let remove_behavior ?(force=false) e kf bhv =
+ let set_spec spec tbl =
+ (* Kernel.feedback "Current spec is %a@." Cil_printer.pp_funspec spec; *)
+ (* do not use physical equality since the behaviors are almost always copied
+ at some points *)
+ spec.spec_behavior <- filterq ~eq:is_same_behavior bhv spec.spec_behavior;
+ let name = bhv.b_name in
+ let check get =
+ if not force &&
+ exists_in_funspec
+ (fun s -> List.exists (List.exists ((=) name)) (get s))
+ tbl
+ then
+ Kernel.fatal
+ "trying to remove a behavior used in a complete or disjoint clause"
+ in
+ check (fun s -> s.spec_complete_behaviors);
+ check (fun s -> s.spec_disjoint_behaviors);
+ (* Kernel.feedback "Removing behavior %s@." bhv.b_name; *)
+ (* Kernel.feedback "New spec is %a@." Cil_printer.pp_funspec spec; *)
+ List.iter Property_status.remove
+ (Property.ip_all_of_behavior kf Kglobal ~active:[] bhv)
+ in
+ remove_in_funspec e kf set_spec
+
+let remove_decreases e kf =
+ let set_spec spec _tbl =
+ match spec.spec_variant with
+ | None -> ()
+ | Some d ->
+ Property_status.remove (Property.ip_of_decreases kf Kglobal d);
+ spec.spec_variant <- None
+ in
+ remove_in_funspec e kf set_spec
+
+let remove_terminates e kf =
+ let set_spec spec _tbl =
+ match spec.spec_terminates with
+ | None -> ()
+ | Some t ->
+ Property_status.remove (Property.ip_of_terminates kf Kglobal t);
+ spec.spec_terminates <- None
+ in
+ remove_in_funspec e kf set_spec
+
+let remove_complete e kf l =
+ let set_spec spec _tbl =
+ spec.spec_complete_behaviors <- filterq l spec.spec_complete_behaviors
+ in
+ remove_in_funspec e kf set_spec;
+ Property_status.remove (Property.ip_of_complete kf Kglobal ~active:[] l)
+
+let remove_disjoint e kf l =
+ let set_spec spec _tbl =
+ spec.spec_disjoint_behaviors <- filterq l spec.spec_disjoint_behaviors
+ in
+ remove_in_funspec e kf set_spec;
+ Property_status.remove (Property.ip_of_disjoint kf Kglobal ~active:[] l)
+
+let remove_requires e kf p =
+ let set_spec spec _tbl =
+ List.iter
+ (fun b ->
+ if List.memq p b.b_requires then begin
+ b.b_requires <- filterq p b.b_requires;
+ Property_status.remove (Property.ip_of_requires kf Kglobal b p)
+ end)
+ spec.spec_behavior
+ in
+ remove_in_funspec e kf set_spec
+
+let remove_assumes e kf p =
+ let set_spec spec _tbl =
+ List.iter
+ (fun b ->
+ if List.memq p b.b_assumes then begin
+ b.b_assumes <- filterq p b.b_assumes;
+ Property_status.remove (Property.ip_of_assumes kf Kglobal b p)
+ end)
+ spec.spec_behavior
+ in
+ remove_in_funspec e kf set_spec
+
+let remove_ensures e kf p =
+ let set_spec spec _tbl =
+ List.iter
+ (fun b ->
+ if List.memq p b.b_post_cond then begin
+ b.b_post_cond <- filterq p b.b_post_cond;
+ Property_status.remove (Property.ip_of_ensures kf Kglobal b p)
+ end)
+ spec.spec_behavior
+ in
+ remove_in_funspec e kf set_spec
+
+let remove_allocates e kf p =
+ let set_spec spec _tbl =
+ List.iter
+ (fun b ->
+ if b.b_allocation == p then begin
+ b.b_allocation <- FreeAllocAny;
+ let info = Id_contract (Datatype.String.Set.empty,b) in
+ Option.iter Property_status.remove
+ (Property.ip_of_allocation kf Kglobal info p)
+ end)
+ spec.spec_behavior
+ in
+ remove_in_funspec e kf set_spec
+
+let remove_extended e kf ext =
+ let set_spec spec _tbl =
+ List.iter
+ (fun b ->
+ b.b_extended <- List.filter ((!=) ext) b.b_extended;
+ Property_status.remove
+ (Property.(ip_of_extended (ELContract kf) ext)))
+ spec.spec_behavior
+ in
+ remove_in_funspec e kf set_spec
+
+
+let remove_assigns e kf p =
+ let set_spec spec _tbl =
+ List.iter
+ (fun b ->
+ if b.b_assigns == p then begin
+ b.b_assigns <- WritesAny;
+ let info = Id_contract(Datatype.String.Set.empty, b) in
+ Option.iter Property_status.remove
+ (Property.ip_of_assigns kf Kglobal info p);
+ (match p with
+ | WritesAny -> ()
+ | Writes l ->
+ List.iter
+ (fun f ->
+ Option.iter
+ Property_status.remove
+ (Property.ip_of_from kf Kglobal info f)) l)
+ end)
+ spec.spec_behavior
+ in
+ remove_in_funspec e kf set_spec
+
+let remove_behavior_components e kf b =
+ List.iter (remove_requires e kf) b.b_requires;
+ List.iter (remove_assumes e kf) b.b_assumes;
+ List.iter (remove_ensures e kf) b.b_post_cond;
+ remove_assigns e kf b.b_assigns;
+ remove_allocates e kf b.b_allocation
+
(**************************************************************************)
(** {2 Adding annotations} *)
(**************************************************************************)
@@ -860,7 +1072,6 @@ let kinstr stmt =
| None -> Kglobal
| Some s -> Kstmt s
-let is_same_behavior b1 b2 = b1.b_name = b2.b_name
let mk_spec bhv variant terminates complete disjoint =
{ spec_behavior = bhv;
@@ -936,21 +1147,26 @@ let add_behaviors ?(register_children=true) e kf ?stmt ?active bhvs =
bhvs
end
-let add_decreases e kf v =
+exception AlreadySpecified of string list
+
+let add_decreases ?(force=false) e kf v =
+ if force then remove_decreases e kf ;
let full_spec = get_spec_all kf () in
let emit_spec = get_spec_e e kf () in
(match full_spec.spec_variant with
- | Some _ -> Kernel.fatal "already a variant for function %a" Kf.pretty kf
- | None -> emit_spec.spec_variant <- Some v);
+ | Some old when not @@ Logic_utils.is_same_variant old v ->
+ raise (AlreadySpecified ["decreases"])
+ | _ -> emit_spec.spec_variant <- Some v);
Property_status.register (Property.ip_of_decreases kf Kglobal v)
-let add_terminates e kf ?stmt ?active t =
+let add_terminates ?(force=false) e kf ?stmt ?active t =
+ if force then remove_terminates e kf ;
let full_spec = get_spec_all kf ?stmt ?active () in
let emit_spec = get_spec_e e kf ?stmt ?active () in
(match full_spec.spec_terminates with
- | Some _ ->
- Kernel.fatal "already a terminates clause for function %a" Kf.pretty kf
- | None -> emit_spec.spec_terminates <- Some t);
+ | Some old when not @@ Logic_utils.is_same_identified_predicate old t ->
+ raise (AlreadySpecified ["terminates"])
+ | _ -> emit_spec.spec_terminates <- Some t);
Property_status.register (Property.ip_of_terminates kf (kinstr stmt) t)
let check_bhv_name spec name =
@@ -997,11 +1213,27 @@ let add_disjoint e kf ?stmt ?active l =
Property_status.register (Property.ip_of_disjoint kf (kinstr stmt) ~active l)
end
-let add_spec ?register_children e kf ?stmt ?active spec =
+let add_spec ?register_children ?(force=false) e kf ?stmt ?active spec =
+ let full_spec = get_spec_all kf ?stmt ?active () in
+ let conflicts =
+ (match full_spec.spec_terminates, spec.spec_terminates with
+ | Some old_t, Some new_t
+ when not @@ Logic_utils.is_same_identified_predicate old_t new_t ->
+ ["terminates"]
+ | _ -> []) @
+ (match full_spec.spec_variant, spec.spec_variant with
+ | Some old_t, Some new_t
+ when not @@ Logic_utils.is_same_variant old_t new_t ->
+ ["decreases"]
+ | _ -> [])
+ in
+ if not force && conflicts <> [] then raise (AlreadySpecified conflicts) ;
add_behaviors ?register_children e kf ?stmt ?active spec.spec_behavior;
- Option.iter (fun variant -> add_decreases e kf variant) spec.spec_variant;
Option.iter
- (fun terminates -> add_terminates e kf ?stmt ?active terminates)
+ (fun variant -> add_decreases ~force e kf variant)
+ spec.spec_variant;
+ Option.iter
+ (fun terminates -> add_terminates ~force e kf ?stmt ?active terminates)
spec.spec_terminates;
List.iter
(fun complete -> add_complete e kf ?stmt ?active complete)
@@ -1439,214 +1671,6 @@ let add_global e a =
unsafe_add_global e a;
if Ast.is_computed() then insert_global_in_ast a
-(**************************************************************************)
-(** {2 Removing annotations} *)
-(**************************************************************************)
-
-(* If this function gets exported, please turn e into an Emitter.t *)
-let remove_model_field (e:Usable_emitter.t) m =
- try
- let ty = m.mi_base_type in
- let h = Model_fields.find ty in
- let l = Usable_emitter.Hashtbl.find h e in
- let l' =
- List.filter (fun x -> not (Cil_datatype.Model_info.equal x m)) l
- in
- Usable_emitter.Hashtbl.replace h e l';
- Model_fields.apply_hooks_on_remove e ty l'
- with Not_found ->
- ()
-
-let remove_global e a =
- try
- let e = Emitter.get e in
- let h = Globals.find a in
- Usable_emitter.Hashtbl.iter
- (fun e' () ->
- if Emitter.Usable_emitter.equal e e' then begin
- Globals.remove a;
- (match a with
- | Dmodel_annot (m,_) -> remove_model_field e m
- | _ -> ());
- let file = Ast.get () in
- file.globals <-
- List.filter
- (fun a' ->
- not (Global.equal (GAnnot(a, Global_annotation.loc a)) a'))
- file.globals;
- Globals.apply_hooks_on_remove e a ()
- end)
- h;
- with Not_found ->
- ()
-
-let remove_in_funspec e kf set_spec =
- try
- let tbl = Funspecs.find kf in
- let e = Emitter.get e in
- try
- let spec = Emitter.Usable_emitter.Hashtbl.find tbl e in
- (* Format.printf "Known specs for %a@." Kf.pretty kf;*)
- (* Emitter.Usable_emitter.Hashtbl.iter
- (fun e spec ->
- Format.printf "For emitter %a: %a@."
- Emitter.Usable_emitter.pretty e
- Cil_printer.pp_funspec spec) tbl; *)
- set_spec spec tbl
- with Not_found -> ()
- with Not_found ->
- assert false
-
-let remove_behavior ?(force=false) e kf bhv =
- let set_spec spec tbl =
- (* Kernel.feedback "Current spec is %a@." Cil_printer.pp_funspec spec; *)
- (* do not use physical equality since the behaviors are almost always copied
- at some points *)
- spec.spec_behavior <- filterq ~eq:is_same_behavior bhv spec.spec_behavior;
- let name = bhv.b_name in
- let check get =
- if not force &&
- exists_in_funspec
- (fun s -> List.exists (List.exists ((=) name)) (get s))
- tbl
- then
- Kernel.fatal
- "trying to remove a behavior used in a complete or disjoint clause"
- in
- check (fun s -> s.spec_complete_behaviors);
- check (fun s -> s.spec_disjoint_behaviors);
- (* Kernel.feedback "Removing behavior %s@." bhv.b_name; *)
- (* Kernel.feedback "New spec is %a@." Cil_printer.pp_funspec spec; *)
- List.iter Property_status.remove
- (Property.ip_all_of_behavior kf Kglobal ~active:[] bhv)
- in
- remove_in_funspec e kf set_spec
-
-let remove_decreases e kf =
- let set_spec spec _tbl =
- match spec.spec_variant with
- | None -> ()
- | Some d ->
- Property_status.remove (Property.ip_of_decreases kf Kglobal d);
- spec.spec_variant <- None
- in
- remove_in_funspec e kf set_spec
-
-let remove_terminates e kf =
- let set_spec spec _tbl =
- match spec.spec_terminates with
- | None -> ()
- | Some t ->
- Property_status.remove (Property.ip_of_terminates kf Kglobal t);
- spec.spec_terminates <- None
- in
- remove_in_funspec e kf set_spec
-
-let remove_complete e kf l =
- let set_spec spec _tbl =
- spec.spec_complete_behaviors <- filterq l spec.spec_complete_behaviors
- in
- remove_in_funspec e kf set_spec;
- Property_status.remove (Property.ip_of_complete kf Kglobal ~active:[] l)
-
-let remove_disjoint e kf l =
- let set_spec spec _tbl =
- spec.spec_disjoint_behaviors <- filterq l spec.spec_disjoint_behaviors
- in
- remove_in_funspec e kf set_spec;
- Property_status.remove (Property.ip_of_disjoint kf Kglobal ~active:[] l)
-
-let remove_requires e kf p =
- let set_spec spec _tbl =
- List.iter
- (fun b ->
- if List.memq p b.b_requires then begin
- b.b_requires <- filterq p b.b_requires;
- Property_status.remove (Property.ip_of_requires kf Kglobal b p)
- end)
- spec.spec_behavior
- in
- remove_in_funspec e kf set_spec
-
-let remove_assumes e kf p =
- let set_spec spec _tbl =
- List.iter
- (fun b ->
- if List.memq p b.b_assumes then begin
- b.b_assumes <- filterq p b.b_assumes;
- Property_status.remove (Property.ip_of_assumes kf Kglobal b p)
- end)
- spec.spec_behavior
- in
- remove_in_funspec e kf set_spec
-
-let remove_ensures e kf p =
- let set_spec spec _tbl =
- List.iter
- (fun b ->
- if List.memq p b.b_post_cond then begin
- b.b_post_cond <- filterq p b.b_post_cond;
- Property_status.remove (Property.ip_of_ensures kf Kglobal b p)
- end)
- spec.spec_behavior
- in
- remove_in_funspec e kf set_spec
-
-let remove_allocates e kf p =
- let set_spec spec _tbl =
- List.iter
- (fun b ->
- if b.b_allocation == p then begin
- b.b_allocation <- FreeAllocAny;
- let info = Id_contract (Datatype.String.Set.empty,b) in
- Option.iter Property_status.remove
- (Property.ip_of_allocation kf Kglobal info p)
- end)
- spec.spec_behavior
- in
- remove_in_funspec e kf set_spec
-
-let remove_extended e kf ext =
- let set_spec spec _tbl =
- List.iter
- (fun b ->
- b.b_extended <- List.filter ((!=) ext) b.b_extended;
- Property_status.remove
- (Property.(ip_of_extended (ELContract kf) ext)))
- spec.spec_behavior
- in
- remove_in_funspec e kf set_spec
-
-
-let remove_assigns e kf p =
- let set_spec spec _tbl =
- List.iter
- (fun b ->
- if b.b_assigns == p then begin
- b.b_assigns <- WritesAny;
- let info = Id_contract(Datatype.String.Set.empty, b) in
- Option.iter Property_status.remove
- (Property.ip_of_assigns kf Kglobal info p);
- (match p with
- | WritesAny -> ()
- | Writes l ->
- List.iter
- (fun f ->
- Option.iter
- Property_status.remove
- (Property.ip_of_from kf Kglobal info f)) l)
- end)
- spec.spec_behavior
- in
- remove_in_funspec e kf set_spec
-
-let remove_behavior_components e kf b =
- List.iter (remove_requires e kf) b.b_requires;
- List.iter (remove_assumes e kf) b.b_assumes;
- List.iter (remove_ensures e kf) b.b_post_cond;
- remove_assigns e kf b.b_assigns;
- remove_allocates e kf b.b_allocation
-
(**************************************************************************)
(** {2 Other useful functions} *)
(**************************************************************************)
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index 81e0911b96c4836b5e5a63e538e95cac0aebda85..4f6c1e6baa0813f46d12bfb8502f5d1a01b45d69 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -331,12 +331,31 @@ type 'a behavior_component_addition =
@since Aluminium-20160501
*)
-val add_spec: ?register_children:bool -> spec contract_component_addition
-(** Add new spec into the given contract.
+exception AlreadySpecified of string list
+(** raised when a specification can't be added since there is already one, the
+ list contains the clause kind that can't be addeed (e.g: "decreases"). *)
+
+val add_spec:
+ ?register_children:bool -> ?force:bool -> spec contract_component_addition
+(** Add new spec into the given contract. The [force] (which defaults to
+ [false]) parameter is used to determine whether [decreases] and [terminates]
+ clauses mùst be relaced if they already exists and a new one is provided.
+
+ More precisely, if [force] is [true] *and* the new contract has
+ [Some terminates], the old one is removed and the new clause is used
+ (the same applies for [decreases]). *But* if the new clause is [None], the
+ old one is kept. If you really want to remove some of these clauses, use
+ {!remove_decreases} and {!remove_terminates}.
+
+ If [force] is [false] and the contract has [Some terminates] (or decreases)
+ and the old contract already has such specification, an exception
+ [AlreadySpecified] is raised. Note that in this case, the function does not
+ perform any modification to the spec.
[register_children] is directly given to the function [add_behaviors].
@since 23.0-Vanadium
+ @before Frama-C+dev: the [force] parameter does not exist
*)
val add_behaviors:
@@ -346,14 +365,26 @@ val add_behaviors:
behavior will also be registered by the function.
*)
-val add_decreases: Emitter.t -> kernel_function -> variant -> unit
+val add_decreases:
+ ?force:bool -> Emitter.t -> kernel_function -> variant -> unit
(** Add a decrease clause into the contract of the given function.
- No decrease clause must previously be attached to this function.
+
+ If [force] is [false] (default), if a clause is already attached to the
+ function, an exception [AlreadySpecified] is raised. If [force] is [true]
+ the old specification is dropped and the new one replaces it.
+
+ @before Frama-C+dev: the [force] parameter does not exist
*)
-val add_terminates: identified_predicate contract_component_addition
-(** Add a terminates clause into a contract.
- No terminates clause must previously be attached to this contract.
+val add_terminates:
+ ?force:bool -> identified_predicate contract_component_addition
+(** Add a terminates clause into the contract of the given function.
+
+ If [force] is [false] (default), if a clause is already attached to the
+ function, an exception [AlreadySpecified] is raised. If [force] is [true]
+ the old specification is dropped and the new one replaces it.
+
+ @before Frama-C+dev: the [force] parameter does not exist
*)
val add_complete: string list contract_component_addition
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index b11c7031c00d20b76b8c5af9271e17c833e3df0a..6853fe7e402dd29321e3a4ae919be7790ce0dec4 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3054,7 +3054,7 @@ class cil_printer () = object (self)
let nl_assigns = nl || b.b_allocation != FreeAllocAny in
let nl_extended = nl_assigns || b.b_assigns != WritesAny in
let nl_ensures = nl_extended || b.b_extended != [] in
- let nl_decreases = nl_extended || b.b_post_cond != [] in
+ let nl_decreases = nl_ensures || b.b_post_cond != [] in
let nl_requires = nl_decreases || variant != None || terminates != None in
let nl_assumes = nl_requires || b.b_requires != [] in
let pp_list nl fmt =
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index 220f595078371d39769ca279359877beb0db5dde..cdb006d3a1eac09c041814a24b0eb0824699c34f 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -408,10 +408,8 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
{ spec_behavior = snd (List.split old_behaviors);
spec_complete_behaviors = snd (List.split old_complete);
spec_disjoint_behaviors = snd (List.split old_disjoint);
- spec_terminates =
- (Option.map snd) old_terminates;
- spec_variant =
- (Option.map snd) old_decreases
+ spec_terminates = Option.map snd old_terminates;
+ spec_variant = Option.map snd old_decreases
}
in
let res = self#vspec spec in
@@ -430,6 +428,10 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
b')
old_behaviors
in
+ Queue.add
+ (fun () ->
+ ignore (Annotations.funspec ~populate:false new_kf))
+ self#get_filling_actions ;
let new_terminates =
Option.map
(fun (e,t) ->
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 d3b9353faf697321bb3adfffba751e16d49373a2..7d9589cab9a6f01ded358361ce109682da56423e 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -598,6 +598,13 @@ let unduplicable_functions =
Datatype.String.Set.empty
white_list
+(* Note: it might not have terminates at all, the point is just to ignore it. *)
+let spec_has_only_terminates spec =
+ spec.spec_variant = None &&
+ List.for_all Cil.is_empty_behavior spec.spec_behavior &&
+ spec.spec_disjoint_behaviors = [] &&
+ spec.spec_complete_behaviors = []
+
let must_duplicate kf vi =
(* it is not already duplicated *)
not (Dup_functions.mem vi)
@@ -614,8 +621,11 @@ let must_duplicate kf vi =
not (Functions.instrument kf)
||
(* or: *)
- ((* it has a function contract *)
- not (Cil.is_empty_funspec (Annotations.funspec ~populate:false kf))
+ ( let spec = Annotations.funspec ~populate:false kf in
+ (* it has a function contract *)
+ not (Cil.is_empty_funspec spec)
+ && (* there are some annotations that might be treated *)
+ not (spec_has_only_terminates spec)
&& (* its annotations must be monitored *)
Functions.check kf))
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index 9cda687a2e314b91a843d26863a4e36a6938cea6..3dc9d2147008e22628a1ce68cedbbe471ea2c5fb 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -468,7 +468,13 @@ let merge_rtl_spec rtl_prj rtl_global =
let vis_replace_formals = new vis_replace_leaves ~formals:formals_assoc () in
let spec = Visitor.visitFramacFunspec vis_replace_formals spec in
(* Add the updated spec to the user's kf *)
- Annotations.add_spec Options.emitter user_kf spec
+ try Annotations.add_spec Options.emitter user_kf spec
+ with Annotations.AlreadySpecified(clauses) ->
+ Options.error ~source:(fst @@ Kernel_function.get_location user_kf)
+ "Found inconsistent specification for function %a (clause%s: %a)"
+ Cil_printer.pp_varinfo vi
+ (if 1 < List.length clauses then "s" else "")
+ (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) clauses
end
| GVarDecl _ | GVar _ | GType _ | GCompTag _ | GCompTagDecl _ | GEnumTag _
| GEnumTagDecl _ | GAnnot _ | GAsm _ | GPragma _ | GText _ ->
diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index 5c3d8c60694a70c9af58d802235e9121759334e8..4668713a3706888b7b18bffd0ceb25d6e0d83df6 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/src/plugins/eva/engine/recursion.ml
@@ -46,9 +46,10 @@ let mark_unknown_requires kinstr kf funspec =
let get_spec kinstr kf =
let funspec = Annotations.funspec ~populate:false kf in
- if Cil.is_empty_funspec funspec then begin
+ if List.for_all (fun b -> b.b_assigns = WritesAny) funspec.spec_behavior
+ then begin
Self.error ~current:true
- "@[Recursive call to %a@ without a specification.@ \
+ "@[Recursive call to %a@ without assigns clause.@ \
Generating probably incomplete assigns to interpret the call.@ \
Try to increase@ the %s parameter@ \
or write a correct specification@ for function %a.@\n%t@]"
diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
index c46055dd4a58a205e31956206de4d70292a59bbd..af855741f0e4372683b22084a5d97ef9f1d235a2 100644
--- a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
+++ b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
@@ -4,16 +4,16 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
-[kernel] n5.i:21: Warning:
- No code nor implicit assigns clause for function may_not_terminate, generating default assigns from the prototype
+[kernel:annot:missing-spec] n5.i:21: Warning:
+ Neither code nor implicit assigns clause for function may_not_terminate, generating default assigns from the prototype
[eva] computing for function may_not_terminate <- main.
Called from n5.i:21.
[eva] using specification for function may_not_terminate
[eva] Done for function may_not_terminate
[eva] computing for function f <- main.
Called from n5.i:22.
-[kernel] n5.i:12: Warning:
- No code nor implicit assigns clause for function never_terminates, generating default assigns from the prototype
+[kernel:annot:missing-spec] n5.i:12: Warning:
+ Neither code nor implicit assigns clause for function never_terminates, generating default assigns from the prototype
[eva] computing for function never_terminates <- f <- main.
Called from n5.i:12.
[eva] using specification for function never_terminates
diff --git a/src/plugins/report/tests/report/oracle/csv.res.oracle b/src/plugins/report/tests/report/oracle/csv.res.oracle
index 5647ffdfd1d4c01f4910a6efcdfc05e2ae610bd3..5564080578e09d1a0a62c6da94d75155a92291a1 100644
--- a/src/plugins/report/tests/report/oracle/csv.res.oracle
+++ b/src/plugins/report/tests/report/oracle/csv.res.oracle
@@ -10,8 +10,8 @@
[eva] Done for function main1
[eva] computing for function main2 <- main.
Called from csv.c:55.
-[kernel] csv.c:21: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] csv.c:21: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[eva] computing for function f <- main2 <- main.
Called from csv.c:21.
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
index cc2a87bfd3f19af366cd3d82f9a3300303ce8ada..adeba624aa19e9d4e3301bb167609775c6a53cd6 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
@@ -4,8 +4,8 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel] empty-vpar-with-ghost.i:8: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] empty-vpar-with-ghost.i:8: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
index 14ecb70143047d655580d9432317065252f90d91..2992d941ca229fefe1171389c2c30f4183eff055 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
@@ -3,8 +3,8 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel] empty-vpar.i:8: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] empty-vpar.i:8: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
index 1acd1bb8c69359eeb7e416f4c75368bf98049533..d32b93303b868c261244c1274999b04b146ca76a 100644
--- a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
@@ -5,11 +5,11 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel] multi.i:18: Warning:
- No code nor implicit assigns clause for function g, generating default assigns from the prototype
+[kernel:annot:missing-spec] multi.i:18: Warning:
+ Neither code nor implicit assigns clause for function g, generating default assigns from the prototype
[eva] using specification for function g
-[kernel] multi.i:9: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] multi.i:9: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
index 1b378cc5fd2c0d860e9582ddded60997df0e3f99..e00685b83a54ebe8dec8cf3585694e8faace471e 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
@@ -4,8 +4,8 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel] simple-with-ghost.i:9: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] simple-with-ghost.i:9: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
index d9e9fd70b24481021169e6112dc7409bb54440aa..f7b68f735644c4999f763be64a4892a4e3e48079 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
@@ -3,8 +3,8 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel] simple.i:9: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] simple.i:9: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle b/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
index 8f286711f517a65f915fd3baf916a38959b8936d..4e98311386b6b1d4cf9598dfd6d5a760d75fa8ec 100644
--- a/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing bad_cast_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] bad_cast_call.i:6: Warning:
- No code nor implicit assigns clause for function m, generating default assigns from the prototype
+[kernel:annot:missing-spec] bad_cast_call.i:6: Warning:
+ Neither code nor implicit assigns clause for function m, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] bad_cast_call.i:8: Warning:
Cast with incompatible pointers types (source: sint8*) (target: char**)
diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
index 7ce4b54a31acd53f9242f3c0f9de84b7017236b7..91cb6e824e2d2e85e3113105e49430c14078350e 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
@@ -3,8 +3,8 @@
[kernel:CERT:MSC:37] stmtcompiler_test.i:136: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
-[kernel] stmtcompiler_test.i:145: Warning:
- No code nor implicit assigns clause for function behavior1, generating default assigns from the prototype
+[kernel:annot:missing-spec] stmtcompiler_test.i:145: Warning:
+ Neither code nor implicit assigns clause for function behavior1, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] stmtcompiler_test.i:81: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
index a81e1ddf5392dc20fcedc4458a2058d068877454..d8af6c81ecd389758eaea647a5491d116fe719b7 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
@@ -1,10 +1,10 @@
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
-[kernel] wp_call_pre.c:44: Warning:
- No code nor implicit assigns clause for function g, generating default assigns from the prototype
-[kernel] wp_call_pre.c:44: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] wp_call_pre.c:44: Warning:
+ Neither code nor implicit assigns clause for function g, generating default assigns from the prototype
+[kernel:annot:missing-spec] wp_call_pre.c:44: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call_main
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle
index edc16654c84577e1f333f79f4b6ce8c70ea29212..6553a1b4b238da7fbf46706d15a43ca2e6571e9f 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle
@@ -2,8 +2,8 @@
[kernel] Parsing wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[kernel] wp_call_pre.c:32: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] wp_call_pre.c:32: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
Goal Pre-condition 'qed_ok,Rmain' in 'main':
Prove: true.
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
index 8ee9e5fdf9b33fe732705bb05a771463647de355..6a0cbda51fab7be9b574c60f562de1a9f58d18ee 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
@@ -1,10 +1,10 @@
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
-[kernel] wp_call_pre.c:44: Warning:
- No code nor implicit assigns clause for function g, generating default assigns from the prototype
-[kernel] wp_call_pre.c:44: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] wp_call_pre.c:44: Warning:
+ Neither code nor implicit assigns clause for function g, generating default assigns from the prototype
+[kernel:annot:missing-spec] wp_call_pre.c:44: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function double_call
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
index 63c5f1576f9bcce5d71cad71eb0588f4a083bb04..930902b0f4de6e37f9ba703959ea80da9ef994b7 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
-[kernel] wp_call_pre.c:44: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] wp_call_pre.c:44: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
Goal Instance of 'Pre-condition 'qed_ok,Rf' in 'f'' in 'double_call' at initialization of 'x1' (file wp_call_pre.c, line 25)
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
index 03960c9b9cd0bceb2d8faa3a9f531c9a77b7eb3b..ddc6608f5c6b758a57889d287428dced4bc1fe03 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing bad_cast_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] bad_cast_call.i:6: Warning:
- No code nor implicit assigns clause for function m, generating default assigns from the prototype
+[kernel:annot:missing-spec] bad_cast_call.i:6: Warning:
+ Neither code nor implicit assigns clause for function m, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] bad_cast_call.i:8: Warning:
Cast with incompatible pointers types (source: sint8*) (target: char**)
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
index 299000ad3043b080254a426feaac1a9f0b4cb842..ff79bc4165659abce7ec46136d370524b9195672 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
@@ -3,8 +3,8 @@
[kernel:CERT:MSC:37] stmtcompiler_test.i:136: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
-[kernel] stmtcompiler_test.i:145: Warning:
- No code nor implicit assigns clause for function behavior1, generating default assigns from the prototype
+[kernel:annot:missing-spec] stmtcompiler_test.i:145: Warning:
+ Neither code nor implicit assigns clause for function behavior1, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] stmtcompiler_test.i:81: Warning:
Missing assigns clause (assigns 'everything' instead)
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index 3e878841ff7e6c807cf3c6d85897bebe6376c215..99ca48093e3ff6a1b6eed0bb089cfeb7a1b091a9 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -1,10 +1,10 @@
# frama-c -wp [...]
[kernel] Parsing wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
-[kernel] wp_call_pre.c:44: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
-[kernel] wp_call_pre.c:44: Warning:
- No code nor implicit assigns clause for function g, generating default assigns from the prototype
+[kernel:annot:missing-spec] wp_call_pre.c:44: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] wp_call_pre.c:44: Warning:
+ Neither code nor implicit assigns clause for function g, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Valid] typed_double_call_call_f_requires_qed_ok_Rf (Qed)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
index 574ed8394568446bf7b1bb5c3318e633f34a4029..71210268875ed88f4ff98c01a477bf150bed75d8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing init_label.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] init_label.i:27: Warning:
- No code nor implicit assigns clause for function main, generating default assigns from the prototype
+[kernel:annot:missing-spec] init_label.i:27: Warning:
+ Neither code nor implicit assigns clause for function main, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function extra
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
index 7cff9c2db7da4e9622ee9f46f726a8a67e5cadef..596aaa702dea36c2937dc85414c63d6b811bbce5 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing initialized_shift_array.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] initialized_shift_array.i:52: Warning:
- No code nor implicit assigns clause for function test, generating default assigns from the prototype
+[kernel:annot:missing-spec] initialized_shift_array.i:52: Warning:
+ Neither code nor implicit assigns clause for function test, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function fail_cell_after_end
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
index e446f4a55dc881882723d992c586d452026fc22f..d3ce666bfa06e912a34d4a07792a18a7fda7696d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing unsupported_builtin.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] unsupported_builtin.i:11: Warning:
- No code nor implicit assigns clause for function foo, generating default assigns from the prototype
+[kernel:annot:missing-spec] unsupported_builtin.i:11: Warning:
+ Neither code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] unsupported_builtin.i:8: Warning: Builtin unimplemented_builtin not defined
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
index 09e822a3133e8e05930d5363cb0d3c26dbd5b1c1..592aac32a718cdc7f936f067f9faa71d01983ffd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing init_label.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] init_label.i:27: Warning:
- No code nor implicit assigns clause for function main, generating default assigns from the prototype
+[kernel:annot:missing-spec] init_label.i:27: Warning:
+ Neither code nor implicit assigns clause for function main, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Valid] typed_main_requires_OK (Qed)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
index c329417b047a4faa3f8080e1f69011c83b0f5cad..61f043e7e7a9f5bea912f1ec4dd4316c781b1930 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing initialized_shift_array.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] initialized_shift_array.i:52: Warning:
- No code nor implicit assigns clause for function test, generating default assigns from the prototype
+[kernel:annot:missing-spec] initialized_shift_array.i:52: Warning:
+ Neither code nor implicit assigns clause for function test, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 11 goals scheduled
[wp] [Valid] typed_succ_full_first_cell_call_test_requires (Qed)
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
index 1bed6f65bc40584922571536d04f0d44016f29e8..af657760b216fab5b746a3e8cb162c525bdbcd5c 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing issue_715_a.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] issue_715_a.i:6: Warning:
- No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[kernel:annot:missing-spec] issue_715_a.i:6: Warning:
+ Neither code nor implicit assigns clause for function dummy, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function foo
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
index 1809a095bf9e67412647d8d64b402cfa516eb437..2280f9912d354e134ae5f998e6167eeded951517 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing issue_715_b.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] issue_715_b.i:9: Warning:
- No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[kernel:annot:missing-spec] issue_715_b.i:9: Warning:
+ Neither code nor implicit assigns clause for function dummy, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function foo
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
index 295a361966cdad5b4a5d1789f40117c3dfad025d..2e03bd7cafc3cb62df57e32df2deec421f05b722 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing issue_715_a.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] issue_715_a.i:6: Warning:
- No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[kernel:annot:missing-spec] issue_715_a.i:6: Warning:
+ Neither code nor implicit assigns clause for function dummy, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Valid] typed_foo_call_dummy_requires (Qed)
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
index 4618d75a688bd8a091d785fedca59be46a0c5096..4903ca6afa2d82d44cb8bd237c7b13a699c50639 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing issue_715_b.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] issue_715_b.i:9: Warning:
- No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
+[kernel:annot:missing-spec] issue_715_b.i:9: Warning:
+ Neither code nor implicit assigns clause for function dummy, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_foo_call_dummy_requires (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle
index 90301835e4554489d0da0eafe5894c07cfc85b01..120b181c638c3d333f8531ca4d5f970afe86d899 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing invertible.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] invertible.i:17: Warning:
- No code nor implicit assigns clause for function main, generating default assigns from the prototype
+[kernel:annot:missing-spec] invertible.i:17: Warning:
+ Neither code nor implicit assigns clause for function main, generating default assigns from the prototype
------------------------------------------------------------
Function main
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/annot/a.i b/src/plugins/wp/tests/wp_region/annot/a.i
index 88fa61563c1be65c5d7db0846e8cb9298e45d8b1..8289866c443bb5159d61152f513aeffe280e7aa7 100644
--- a/src/plugins/wp/tests/wp_region/annot/a.i
+++ b/src/plugins/wp/tests/wp_region/annot/a.i
@@ -23,7 +23,8 @@ struct Block {
SN sum ;
};
typedef struct Block FB;
-/*@ region *fb; */
+/*@ terminates \true;
+ region *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
@@ -31,7 +32,8 @@ void fb_ADD(FB *fb)
return;
}
-/*@ region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
+/*@ terminates \true;
+ region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
*/
diff --git a/src/plugins/wp/tests/wp_region/annot/b.i b/src/plugins/wp/tests/wp_region/annot/b.i
index 88fa61563c1be65c5d7db0846e8cb9298e45d8b1..8289866c443bb5159d61152f513aeffe280e7aa7 100644
--- a/src/plugins/wp/tests/wp_region/annot/b.i
+++ b/src/plugins/wp/tests/wp_region/annot/b.i
@@ -23,7 +23,8 @@ struct Block {
SN sum ;
};
typedef struct Block FB;
-/*@ region *fb; */
+/*@ terminates \true;
+ region *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
@@ -31,7 +32,8 @@ void fb_ADD(FB *fb)
return;
}
-/*@ region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
+/*@ terminates \true;
+ region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
*/
diff --git a/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle
index aa86080b5b384cca827b4b5e8fb4b453ae67317e..1968a14bef0d5d7f4093b96cb88df9820da1821e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing avar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] avar.i:4: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] avar.i:4: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function g
diff --git a/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle
index 0d402e887cd313a28e3a94ee362d33b07bf0a508..901822d2d6132eac4fd6f2c2783a17c84c14a2ca 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing avar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] avar.i:4: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] avar.i:4: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function g
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
index 599eded1e56bdfc979ac6fa672e753f34ad17ffe..85c716b9d81f9a59e48101904beef91b34b206ca 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing mvar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] mvar.i:14: Warning:
- No code nor implicit assigns clause for function Write, generating default assigns from the prototype
+[kernel:annot:missing-spec] mvar.i:14: Warning:
+ Neither code nor implicit assigns clause for function Write, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function Job
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
index 756b2207096d3d57d59d960596ac96795257c9d3..5d84ef595fc3cf717f180ad8f479a786cab71386 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing mvar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] mvar.i:14: Warning:
- No code nor implicit assigns clause for function Write, generating default assigns from the prototype
+[kernel:annot:missing-spec] mvar.i:14: Warning:
+ Neither code nor implicit assigns clause for function Write, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function Job
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
index 81b6a3c63eaa995bcb9d50e5a03e1cff6e779fd4..aab090d5f3b3658b6eb4d3f175698a0d1fb08772 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing unit_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] unit_call.i:7: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] unit_call.i:7: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
index 70022706b9fbae3ba71f400040391c85dd2f61ae..054a832b2c49989e0980255f037e7e9192e9bb74 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing unit_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] unit_call.i:7: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] unit_call.i:7: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
index 3600dcbe6cf4ed84e6901b84e0149422a9f2af32..a11babf7d19218e7014305dcca4a0c0577c027a4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing avar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] avar.i:4: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] avar.i:4: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Valid] typed_g_call_f_requires (Qed)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
index b6eb918828a57fb45a7477a6971c10fdabfce34a..5429a71d38cdb4697fe2552f025ee52c4cea959b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing mvar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] mvar.i:14: Warning:
- No code nor implicit assigns clause for function Write, generating default assigns from the prototype
+[kernel:annot:missing-spec] mvar.i:14: Warning:
+ Neither code nor implicit assigns clause for function Write, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Valid] typed_Job_ensures (Alt-Ergo) (Trivial)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
index 8511246e3d97c259f14ec0b5d0a1d7fd83426395..764e60eba2daf7ca129c6a350d93a838a8323b11 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing unit_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] unit_call.i:7: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] unit_call.i:7: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Valid] typed_job_assert (Qed)
diff --git a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
index 922d25821646c3bd412698e9126fd015e99b2873..fef0939f6ab86b83a9e14a065b09d79054179375 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
@@ -1,10 +1,10 @@
# frama-c -wp [...]
[kernel] Parsing code_spec.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] code_spec.i:126: Warning:
- No code nor implicit assigns clause for function by_addr_in_spec, generating default assigns from the prototype
-[kernel] code_spec.i:126: Warning:
- No code nor implicit assigns clause for function by_array_in_spec, generating default assigns from the prototype
+[kernel:annot:missing-spec] code_spec.i:126: Warning:
+ Neither code nor implicit assigns clause for function by_addr_in_spec, generating default assigns from the prototype
+[kernel:annot:missing-spec] code_spec.i:126: Warning:
+ Neither code nor implicit assigns clause for function by_array_in_spec, generating default assigns from the prototype
.................................................
... Ref Usage
.................................................
diff --git a/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle
index 475f67de1ea00f70a931776916623c0469364988..e2c0d2e712e4ffee401296486c7c2a8557563186 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing reads.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] reads.i:86: Warning:
- No code nor implicit assigns clause for function recursive_usage, generating default assigns from the prototype
+[kernel:annot:missing-spec] reads.i:86: Warning:
+ Neither code nor implicit assigns clause for function recursive_usage, generating default assigns from the prototype
.................................................
... Ref Usage
.................................................
diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res
index a291cdc31ab4cd51a4176787f3cbe67776a4972d..4d7db660ccc23d7fdb72db0fd967b104b62da771 100644
--- a/tests/fc_script/oracle/make-wrapper.res
+++ b/tests/fc_script/oracle/make-wrapper.res
@@ -11,7 +11,7 @@
Consider patching, stubbing or adding an ACSL specification to the recursive call, then re-run the analysis.
*** recommendation #2 ***
-2. Found function with missing spec: large_name_to_force_line_break_in_stack_msg
+2. Found function with missing specification: large_name_to_force_line_break_in_stack_msg
Looking for files defining it...
Add the following file to the list of sources to be parsed:
make-wrapper.c
diff --git a/tests/float/oracle/contract_special_float.1.res.oracle b/tests/float/oracle/contract_special_float.1.res.oracle
index 86c08416bbdaff949193ab85ef743721a2d09340..5bcec0fa32eb91f0b232274a4b1f849691e756f8 100644
--- a/tests/float/oracle/contract_special_float.1.res.oracle
+++ b/tests/float/oracle/contract_special_float.1.res.oracle
@@ -16,8 +16,8 @@
[eva] Done for function fun
[eva:alarm] contract_special_float.c:93: Warning:
NaN double value. assert ¬\is_NaN(v);
-[kernel] contract_special_float.c:94: Warning:
- No code nor explicit assigns clause for function fun_no_default, generating default assigns from the specification
+[kernel:annot:missing-spec] contract_special_float.c:94: Warning:
+ Neither code nor explicit assigns clause for function fun_no_default, generating default assigns from the specification
[eva] computing for function fun_no_default <- main.
Called from contract_special_float.c:94.
[eva] using specification for function fun_no_default
diff --git a/tests/float/oracle/contract_special_float.2.res.oracle b/tests/float/oracle/contract_special_float.2.res.oracle
index daefc3e0500b277b95d58763b0a48636faf4978f..38b3c035a39917aede90fb3b693882883152b185 100644
--- a/tests/float/oracle/contract_special_float.2.res.oracle
+++ b/tests/float/oracle/contract_special_float.2.res.oracle
@@ -8,8 +8,8 @@
Called from contract_special_float.c:92.
[eva] using specification for function fun
[eva] Done for function fun
-[kernel] contract_special_float.c:94: Warning:
- No code nor explicit assigns clause for function fun_no_default, generating default assigns from the specification
+[kernel:annot:missing-spec] contract_special_float.c:94: Warning:
+ Neither code nor explicit assigns clause for function fun_no_default, generating default assigns from the specification
[eva] computing for function fun_no_default <- main.
Called from contract_special_float.c:94.
[eva] using specification for function fun_no_default
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8ce7b3829c60d4afb7a416be103cf3f7f2894c5f..5a35c61690f2dd9a0489f8d22cddd5839c938637 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2505,7 +2505,6 @@ void __FC_assert(int c, char const *file, int line, char const *expr);
extern void Frama_C_show_each_warning();
/*@ requires nonnull_c: c ≢ 0;
- terminates c ≢ 0;
assigns \nothing; */
void __FC_assert(int c, char const *file, int line, char const *expr)
{
diff --git a/tests/slicing/oracle/bts1768.res.oracle b/tests/slicing/oracle/bts1768.res.oracle
index b9ebf7ff3bdbeb98fb1c7e6b59e1ba898e36792f..03c5a75c4c2687ea17a89cc000421f94c0657b7c 100644
--- a/tests/slicing/oracle/bts1768.res.oracle
+++ b/tests/slicing/oracle/bts1768.res.oracle
@@ -10,8 +10,8 @@
step ∈ {0}
[eva] computing for function lecture <- main.
Called from bts1768.i:45.
-[kernel] bts1768.i:18: Warning:
- No code nor implicit assigns clause for function choisir, generating default assigns from the prototype
+[kernel:annot:missing-spec] bts1768.i:18: Warning:
+ Neither code nor implicit assigns clause for function choisir, generating default assigns from the prototype
[eva] computing for function choisir <- lecture <- main.
Called from bts1768.i:18.
[eva] using specification for function choisir
diff --git a/tests/sparecode/oracle/bts334.0.res.oracle b/tests/sparecode/oracle/bts334.0.res.oracle
index b5d83bb8ac73533c87e09bfe5e6f2580b7ddec63..7b6ed9eaf508b7a7590bceef65b54f7228a145d1 100644
--- a/tests/sparecode/oracle/bts334.0.res.oracle
+++ b/tests/sparecode/oracle/bts334.0.res.oracle
@@ -12,8 +12,8 @@
s1 ∈ {0}
si[0..1] ∈ {0}
so[0..1] ∈ {0}
-[kernel] bts334.i:66: Warning:
- No code nor explicit assigns clause for function init, generating default assigns from the specification
+[kernel:annot:missing-spec] bts334.i:66: Warning:
+ Neither code nor explicit assigns clause for function init, generating default assigns from the specification
[eva] computing for function init <- main_init.
Called from bts334.i:66.
[eva] using specification for function init
diff --git a/tests/sparecode/oracle/bts334.1.res.oracle b/tests/sparecode/oracle/bts334.1.res.oracle
index 77e6867d86f7469c165f58830a95983a72c8330b..fe6d55a43661081ae54eb9ea68a72579f726ce8b 100644
--- a/tests/sparecode/oracle/bts334.1.res.oracle
+++ b/tests/sparecode/oracle/bts334.1.res.oracle
@@ -12,8 +12,8 @@
s1 ∈ {0}
si[0..1] ∈ {0}
so[0..1] ∈ {0}
-[kernel] bts334.i:66: Warning:
- No code nor explicit assigns clause for function init, generating default assigns from the specification
+[kernel:annot:missing-spec] bts334.i:66: Warning:
+ Neither code nor explicit assigns clause for function init, generating default assigns from the specification
[eva] computing for function init <- main_init.
Called from bts334.i:66.
[eva] using specification for function init
diff --git a/tests/sparecode/oracle/bts334.2.res.oracle b/tests/sparecode/oracle/bts334.2.res.oracle
index 2f276f5ff609c6532b77d47ce878fe364e49a637..358637091dd44e3341a0c9431b9fed0ac6fbb0f5 100644
--- a/tests/sparecode/oracle/bts334.2.res.oracle
+++ b/tests/sparecode/oracle/bts334.2.res.oracle
@@ -11,8 +11,8 @@
s1 ∈ {0}
si[0..1] ∈ {0}
so[0..1] ∈ {0}
-[kernel] bts334.i:66: Warning:
- No code nor explicit assigns clause for function init, generating default assigns from the specification
+[kernel:annot:missing-spec] bts334.i:66: Warning:
+ Neither code nor explicit assigns clause for function init, generating default assigns from the specification
[eva] computing for function init <- main_init.
Called from bts334.i:66.
[eva] using specification for function init
diff --git a/tests/spec/non_ast_spec_copy.i b/tests/spec/non_ast_spec_copy.i
new file mode 100644
index 0000000000000000000000000000000000000000..6b0ef4c550a412730efd94394f932dc39a5ae550
--- /dev/null
+++ b/tests/spec/non_ast_spec_copy.i
@@ -0,0 +1,9 @@
+/* run.config
+ MODULE: @PTEST_NAME@
+ OPT: -copy
+*/
+
+// to be populated by non_ast_spec_copy.ml
+void function(void){
+
+}
diff --git a/tests/spec/non_ast_spec_copy.ml b/tests/spec/non_ast_spec_copy.ml
new file mode 100644
index 0000000000000000000000000000000000000000..03faef2019ec0970de6c518e0e11b08d5f5a7782
--- /dev/null
+++ b/tests/spec/non_ast_spec_copy.ml
@@ -0,0 +1,14 @@
+let add_terminates_true _ =
+ let terminates pred_loc =
+ Logic_const.(new_predicate { ptrue with pred_loc })
+ in
+ let add_terminates kf =
+ if Annotations.terminates ~populate:false kf = None then
+ Annotations.add_terminates
+ Emitter.kernel kf (terminates @@ Kernel_function.get_location kf)
+ in
+ Globals.Functions.iter add_terminates
+
+let () =
+ let category = File.register_code_transformation_category "my_category" in
+ File.add_code_transformation_after_cleanup category add_terminates_true
diff --git a/tests/spec/oracle/default_assigns_bts0966.res.oracle b/tests/spec/oracle/default_assigns_bts0966.res.oracle
index 27379756910d1974772d59270cdb1cb678dcc3d5..6ec612c64f3c4a78d93df4acaa4b36080a848932 100644
--- a/tests/spec/oracle/default_assigns_bts0966.res.oracle
+++ b/tests/spec/oracle/default_assigns_bts0966.res.oracle
@@ -4,8 +4,8 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
auto_states[0..3] ∈ {0}
-[kernel] default_assigns_bts0966.i:34: Warning:
- No code nor implicit assigns clause for function copy, generating default assigns from the specification
+[kernel:annot:missing-spec] default_assigns_bts0966.i:34: Warning:
+ Neither code nor implicit assigns clause for function copy, generating default assigns from the specification
[eva] using specification for function copy
[eva] default_assigns_bts0966.i:20: Warning:
no \from part for clause 'assigns auto_states[Init], auto_states[Copy];'
diff --git a/tests/spec/oracle/non_ast_spec_copy.res.oracle b/tests/spec/oracle/non_ast_spec_copy.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5cb2216aab1e14b1b72427a342a1914d46fcf805
--- /dev/null
+++ b/tests/spec/oracle/non_ast_spec_copy.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing non_ast_spec_copy.i (no preprocessing)
diff --git a/tests/value/oracle/behaviors1.res.oracle b/tests/value/oracle/behaviors1.res.oracle
index 504e982e8951bf6f1ea5d40e294f447aa340583d..17c437e69b3df93242c679dc77d22bf7e2703f9c 100644
--- a/tests/value/oracle/behaviors1.res.oracle
+++ b/tests/value/oracle/behaviors1.res.oracle
@@ -337,8 +337,8 @@
[eva] Done for function test_assigns2
[eva] computing for function test_small1 <- main.
Called from behaviors1.i:649.
-[kernel] behaviors1.i:506: Warning:
- No code nor implicit assigns clause for function f3, generating default assigns from the prototype
+[kernel:annot:missing-spec] behaviors1.i:506: Warning:
+ Neither code nor implicit assigns clause for function f3, generating default assigns from the prototype
[eva] computing for function f3 <- test_small1 <- main.
Called from behaviors1.i:506.
[eva] using specification for function f3
@@ -351,8 +351,8 @@
[eva] Done for function test_small1
[eva] computing for function test_small2 <- main.
Called from behaviors1.i:650.
-[kernel] behaviors1.i:521: Warning:
- No code nor implicit assigns clause for function f4, generating default assigns from the prototype
+[kernel:annot:missing-spec] behaviors1.i:521: Warning:
+ Neither code nor implicit assigns clause for function f4, generating default assigns from the prototype
[eva] computing for function f4 <- test_small2 <- main.
Called from behaviors1.i:521.
[eva] using specification for function f4
@@ -369,8 +369,8 @@
[eva] Done for function test_small2
[eva] computing for function test_small3 <- main.
Called from behaviors1.i:651.
-[kernel] behaviors1.i:534: Warning:
- No code nor implicit assigns clause for function f5, generating default assigns from the prototype
+[kernel:annot:missing-spec] behaviors1.i:534: Warning:
+ Neither code nor implicit assigns clause for function f5, generating default assigns from the prototype
[eva] computing for function f5 <- test_small3 <- main.
Called from behaviors1.i:534.
[eva] using specification for function f5
@@ -379,8 +379,8 @@
[eva] Done for function test_small3
[eva] computing for function test_small4 <- main.
Called from behaviors1.i:652.
-[kernel] behaviors1.i:548: Warning:
- No code nor implicit assigns clause for function f6, generating default assigns from the prototype
+[kernel:annot:missing-spec] behaviors1.i:548: Warning:
+ Neither code nor implicit assigns clause for function f6, generating default assigns from the prototype
[eva] computing for function f6 <- test_small4 <- main.
Called from behaviors1.i:548.
[eva] using specification for function f6
@@ -389,8 +389,8 @@
[eva] Done for function test_small4
[eva] computing for function test_small5 <- main.
Called from behaviors1.i:653.
-[kernel] behaviors1.i:561: Warning:
- No code nor implicit assigns clause for function f7, generating default assigns from the prototype
+[kernel:annot:missing-spec] behaviors1.i:561: Warning:
+ Neither code nor implicit assigns clause for function f7, generating default assigns from the prototype
[eva] computing for function f7 <- test_small5 <- main.
Called from behaviors1.i:561.
[eva] using specification for function f7
diff --git a/tests/value/oracle/false.res.oracle b/tests/value/oracle/false.res.oracle
index 25154cc12ce0807639e59e140f7c7c6ea75ede34..49c04be7ee32a741ccbc826a0c7f1334ca9290ae 100644
--- a/tests/value/oracle/false.res.oracle
+++ b/tests/value/oracle/false.res.oracle
@@ -4,8 +4,8 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel] false.i:18: Warning:
- No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel:annot:missing-spec] false.i:18: Warning:
+ Neither code nor implicit assigns clause for function f, generating default assigns from the prototype
[eva] computing for function f <- main.
Called from false.i:18.
[eva] using specification for function f
diff --git a/tests/value/oracle/postcond_leaf.res.oracle b/tests/value/oracle/postcond_leaf.res.oracle
index c1b3280dc1fa594d2aa5c84a5c614c21717f71d9..27afc68ad1f68081dcc8b4294e70076d3e2cb650 100644
--- a/tests/value/oracle/postcond_leaf.res.oracle
+++ b/tests/value/oracle/postcond_leaf.res.oracle
@@ -5,8 +5,8 @@
[eva:initial-state] Values of globals at initialization
i ∈ [--..--]
j ∈ [--..--]
-[kernel] postcond_leaf.c:109: Warning:
- No code nor implicit assigns clause for function f1, generating default assigns from the prototype
+[kernel:annot:missing-spec] postcond_leaf.c:109: Warning:
+ Neither code nor implicit assigns clause for function f1, generating default assigns from the prototype
[eva] using specification for function f1
[eva:ensures-false] postcond_leaf.c:21: Warning:
function f1: this postcondition evaluates to false in this context.
diff --git a/tests/value/oracle/postcondition.res.oracle b/tests/value/oracle/postcondition.res.oracle
index e714c6b9e81a3e1687803b51ffca85555e2d1ef8..932355e0b64dfc42b1722b1046677783593b3ade 100644
--- a/tests/value/oracle/postcondition.res.oracle
+++ b/tests/value/oracle/postcondition.res.oracle
@@ -17,8 +17,8 @@
Called from postcondition.i:84.
[eva] postcondition.i:84: function get_index: precondition got status valid.
[eva] postcondition.i:17: Frama_C_show_each_cmd: {1}
-[kernel] postcondition.i:20: Warning:
- No code nor implicit assigns clause for function u, generating default assigns from the prototype
+[kernel:annot:missing-spec] postcondition.i:20: Warning:
+ Neither code nor implicit assigns clause for function u, generating default assigns from the prototype
[eva] computing for function u <- get_index <- main.
Called from postcondition.i:20.
[eva] using specification for function u
@@ -74,8 +74,8 @@
[eva] computing for function u <- main.
Called from postcondition.i:88.
[eva] Done for function u
-[kernel] postcondition.i:89: Warning:
- No code nor implicit assigns clause for function cap, generating default assigns from the prototype
+[kernel:annot:missing-spec] postcondition.i:89: Warning:
+ Neither code nor implicit assigns clause for function cap, generating default assigns from the prototype
[eva] computing for function cap <- main.
Called from postcondition.i:89.
[eva] using specification for function cap
diff --git a/tests/value/oracle/precond.res.oracle b/tests/value/oracle/precond.res.oracle
index 01008cd04905b7032567375d16efff639f56a92a..7ed636f7ac45307f821e9bd7b8417e319d15eca3 100644
--- a/tests/value/oracle/precond.res.oracle
+++ b/tests/value/oracle/precond.res.oracle
@@ -17,8 +17,8 @@
[eva] precond.c:32: function f: precondition 'i' got status valid.
[eva] Recording results for f
[eva] Done for function f
-[kernel] precond.c:34: Warning:
- No code nor implicit assigns clause for function g, generating default assigns from the prototype
+[kernel:annot:missing-spec] precond.c:34: Warning:
+ Neither code nor implicit assigns clause for function g, generating default assigns from the prototype
[eva] computing for function g <- main.
Called from precond.c:34.
[eva] using specification for function g
@@ -26,8 +26,8 @@
[eva] Done for function g
[eva] computing for function aux <- main.
Called from precond.c:36.
-[kernel] precond.c:21: Warning:
- No code nor implicit assigns clause for function f2, generating default assigns from the prototype
+[kernel:annot:missing-spec] precond.c:21: Warning:
+ Neither code nor implicit assigns clause for function f2, generating default assigns from the prototype
[eva] computing for function f2 <- aux <- main.
Called from precond.c:21.
[eva] using specification for function f2
diff --git a/tests/value/oracle/precond2.0.res.oracle b/tests/value/oracle/precond2.0.res.oracle
index bdee5be00a85220edd6ceda78281a48e0c6970d1..7be4fbc3520fa7232ac5c8f628f8db941b913301 100644
--- a/tests/value/oracle/precond2.0.res.oracle
+++ b/tests/value/oracle/precond2.0.res.oracle
@@ -19,8 +19,8 @@
function f: precondition 'i' got status invalid.
[eva] Recording results for f
[eva] Done for function f
-[kernel] precond2.c:24: Warning:
- No code nor implicit assigns clause for function g, generating default assigns from the prototype
+[kernel:annot:missing-spec] precond2.c:24: Warning:
+ Neither code nor implicit assigns clause for function g, generating default assigns from the prototype
[eva] computing for function g <- main.
Called from precond2.c:24.
[eva] using specification for function g
diff --git a/tests/value/oracle/precond2.1.res.oracle b/tests/value/oracle/precond2.1.res.oracle
index 39929885285698e3c2746bd5c6e002c64c3dbfb1..7373eea9f6da5713b4b151ccdc7f3bc2f3bcca90 100644
--- a/tests/value/oracle/precond2.1.res.oracle
+++ b/tests/value/oracle/precond2.1.res.oracle
@@ -17,8 +17,8 @@
function f: precondition 'i' got status invalid.
[eva] Recording results for f
[eva] Done for function f
-[kernel] precond2.c:24: Warning:
- No code nor implicit assigns clause for function g, generating default assigns from the prototype
+[kernel:annot:missing-spec] precond2.c:24: Warning:
+ Neither code nor implicit assigns clause for function g, generating default assigns from the prototype
[eva] computing for function g <- main.
Called from precond2.c:24.
[eva] using specification for function g
diff --git a/tests/value/oracle/recursion.2.res.oracle b/tests/value/oracle/recursion.2.res.oracle
index 3b2344e98e1d4ff963ffd974fd3641cff0f3dff8..84f55cfe2e5abfe7f85dd8bc16592c62502637d0 100644
--- a/tests/value/oracle/recursion.2.res.oracle
+++ b/tests/value/oracle/recursion.2.res.oracle
@@ -10,7 +10,7 @@
[eva] recursion.c:438: Frama_C_show_each_36: {36}
[eva] using specification for function Frama_C_interval
[eva] recursion.c:426: User Error:
- Recursive call to sum_nospec without a specification.
+ Recursive call to sum_nospec without assigns clause.
Generating probably incomplete assigns to interpret the call. Try to increase
the -eva-unroll-recursive-calls parameter or write a correct specification
for function sum_nospec.