diff --git a/Changelog b/Changelog
index c1519d1bef4d7a87323733f950c114b4edb92dec..a784c580236a5866708ca967e1221460e6fce72e 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,11 @@
Open Source Release <next-release>
###############################################################################
+- Eva [2025-01-23] Rename warning key `invalid-assigns` to
+ `assigns:invalid-location`
+- Eva [2025-01-23] All warnings about missing assigns or \from clauses
+ are now emitted as errors by default, with the new warning key
+ `assigns:missing`.
- Kernel [2025-01-17] New option -memory-footprint to configure the memory
usage of analyses.
o! Kernel [2024-12-20] Remove Cabs.SEQUENCE statement
diff --git a/src/libraries/utils/pretty_utils.ml b/src/libraries/utils/pretty_utils.ml
index bac42ea030c7f3038e164f9c0acd9d38512bbb30..df97d37c80c5d5380d58f9219fe448d4b127acc9 100644
--- a/src/libraries/utils/pretty_utils.ml
+++ b/src/libraries/utils/pretty_utils.ml
@@ -37,15 +37,6 @@ let to_string ?margin pp x =
Format.pp_print_flush f () ;
Buffer.contents b
-let rec pp_print_string_fill out s =
- if String.contains s ' ' then begin
- let i = String.index s ' ' in
- let l = String.length s in
- let s1 = String.sub s 0 i in
- let s2 = String.sub s (i+1) (l - i - 1) in
- Format.fprintf out "%s@ %a" s1 pp_print_string_fill s2
- end else Format.pp_print_string out s
-
type sformat = (unit,Format.formatter,unit) format
type 'a formatter = Format.formatter -> 'a -> unit
type ('a,'b) formatter2 = Format.formatter -> 'a -> 'b -> unit
diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index 9082720f017197f68bd737b3e7d4c9786299c2ff..c169cbe4fd9b75ce7866e219d4f9885c59df0ecf 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -57,9 +57,6 @@ val to_string: ?margin:int -> (Format.formatter -> 'a -> unit) -> 'a -> string
(** {2 separators} *)
-val pp_print_string_fill : Format.formatter -> string -> unit
-(** transforms every space in a string in breakable spaces.*)
-
val escape_underscores : string -> string
(* ********************************************************************** *)
diff --git a/src/plugins/aorai/tests/ya/floats.i b/src/plugins/aorai/tests/ya/floats.i
index 84879fa708d3368a90685b68d1fb5bbcba28dfd1..d8d8d2b898b0cf25557faa7c614856281a0f0059 100644
--- a/src/plugins/aorai/tests/ya/floats.i
+++ b/src/plugins/aorai/tests/ya/floats.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -then-last -eva
+ STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -then-last -eva -eva-warn-key assigns:missing=active
*/
//@ assigns \result \from x, n;
diff --git a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
index 11062e0fd83fdbe5c227b400a6eaa1209e8af14f..960635f47e9055f7ffce2a06d2fa45b9324868fe 100644
--- a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
@@ -14,9 +14,10 @@
Analysis of function square_root_aux is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function square_root_aux
-[eva] floats.i:6: Warning:
- no \from part
- for clause 'assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;'
+[eva:assigns:missing] floats.i:6: Warning:
+ no \from part for clause
+ 'assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;'.
+ Assuming \from \nothing so that the analysis can continue, but be aware this is probably incorrect.
[eva:alarm] <unknown location> Warning:
function square_root_aux, behavior Buchi_property_behavior: postcondition got status unknown.
[eva:alarm] floats.i:11: Warning:
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
index 8688011acc97bb434e94372d224c53e917b51b99..eda04cca2f426021910934e62da87f3285e2738f 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
@@ -14,9 +14,10 @@
Analysis of function square_root_aux is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function square_root_aux
-[eva] floats.i:6: Warning:
- no \from part
- for clause 'assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;'
+[eva:assigns:missing] floats.i:6: Warning:
+ no \from part for clause
+ 'assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;'.
+ Assuming \from \nothing so that the analysis can continue, but be aware this is probably incorrect.
[eva:alarm] <unknown location> Warning:
function square_root_aux, behavior Buchi_property_behavior: postcondition got status unknown.
[eva:alarm] floats.i:11: Warning:
diff --git a/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle
index 3e4f2b0295e1fc586820cf1a277c1de17c7449a5..f7c2880850e61b252336c1f86dfd0d8a4de5139d 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle
@@ -14,7 +14,7 @@
[eva] memsize.c:25: Warning: ignoring unsupported allocates clause
[eva:alarm] memsize.c:26: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva] FRAMAC_SHARE/libc/stdlib.h:485: Warning:
+[eva:assigns:missing-result] FRAMAC_SHARE/libc/stdlib.h:485: Warning:
no 'assigns \result \from ...' clause specified for function realloc
[eva] memsize.c:29: Warning: ignoring unsupported allocates clause
[eva:alarm] memsize.c:29: Warning:
@@ -42,7 +42,7 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] memsize.c:52: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva] FRAMAC_SHARE/libc/stdlib.h:418: Warning:
+[eva:assigns:missing-result] FRAMAC_SHARE/libc/stdlib.h:418: Warning:
no 'assigns \result \from ...' clause specified for function calloc
[eva] memsize.c:55: Warning: ignoring unsupported allocates clause
[eva:alarm] memsize.c:56: Warning:
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 30b6bc6e5f96a502df6bebb3f39496128673caf6..49efc48b0bad9cd5941596d6b077f6b3e8e9f73d 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -59,12 +59,14 @@ let options_ok () =
check Parameters.EqualityCallFunction.get;
let check_assigns kf =
if need_assigns kf then
- Self.error "@[no assigns@ specified@ for function '%a',@ for \
- which@ a builtin@ or the specification@ will be used.@ \
- Potential unsoundness.@]" Kernel_function.pretty kf
+ Self.warning ~wkey:Self.wkey_missing_assigns
+ "@[No assigns specified for function '%a', for which a builtin will be \
+ used. Potential unsoundness.@]"
+ Kernel_function.pretty kf
in
- Parameters.BuiltinsOverrides.iter (fun (kf, _) -> check_assigns kf);
- Parameters.UsePrototype.iter (fun kf -> check_assigns kf)
+ Parameters.BuiltinsOverrides.iter (fun (kf, _) -> check_assigns kf)
+
+(* Parameters.UsePrototype.iter (fun kf -> check_assigns kf) *)
let plugins_ok () =
if not (Plugin.is_present "inout") then
@@ -77,8 +79,9 @@ let plugins_ok () =
let generate_specs () =
let aux kf =
if need_assigns kf then begin
- Self.warning "Generating potentially incorrect assigns \
- for function '%a' for which option %s is set"
+ Self.warning ~wkey:Self.wkey_missing_assigns
+ "@[No assigns specified for function '%a' for which option %s is set. \
+ Generating potentially incorrect assigns.@]"
Kernel_function.pretty kf Parameters.UsePrototype.option_name;
Populate_spec.populate_funspec ~do_body:true kf [`Assigns];
end
diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index 4852aa7590e40d00a7c3e812a6fe31fb0e423da7..c984b0bc8b6cbdd38d76050da43da38e6b36ab6b 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/src/plugins/eva/engine/recursion.ml
@@ -48,11 +48,11 @@ let check_spec kinstr kf =
let funspec = Annotations.funspec kf in
if List.for_all (fun b -> b.b_assigns = WritesAny) funspec.spec_behavior
then
- Self.error ~current:true
- "@[Recursive call to %a@ without assigns clause.@ \
+ Self.warning ~current:true ~wkey:Self.wkey_missing_assigns
+ "@[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@]"
+ Try to increase the %s parameter \
+ or write a correct specification for function %a.@\n%t@]"
(* note: the "\n" before the pretty print of the stack is required by:
FRAMAC_LIB/analysis-scripts/make_wrapper.py
*)
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index 27c8c62b98e4c22dc3cafcfffba856dd7a573147..4697b7f2671b060c9aa199b2d6af8b657aa6d84b 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/src/plugins/eva/engine/transfer_specification.ml
@@ -40,19 +40,31 @@ let find_default_behavior spec =
List.find (fun b' -> b'.b_name = Cil.default_behavior_name) spec.spec_behavior
let warn_empty_assigns () =
- Self.warning ~current:true ~once:true
- "Cannot handle empty assigns clause. Assuming assigns \\nothing: \
- be aware this is probably incorrect."
+ Self.warning ~current:true ~once:true ~wkey:Self.wkey_missing_assigns
+ "Cannot handle empty assigns clause. Assuming assigns \\nothing so that \
+ the analysis can continue, but be aware this is probably incorrect."
(* Warn for assigns clauses without \from. *)
let warn_empty_from list =
- let no_from = List.filter (fun (_, from) -> from = FromAny) list in
+ let is_empty_set it =
+ match it with
+ | { it_content = { term_node = Tempty_set }} -> true
+ | _ -> false
+ in
+ let no_from =
+ List.filter
+ (fun (it, from) ->
+ (* Ignore assigns \empty with no \from. *)
+ not (is_empty_set it) && from = FromAny)
+ list
+ in
match no_from with
| [] -> ()
| (out, _) :: _ ->
let source = fst out.it_content.term_loc in
- Self.warning ~source ~once:true
- "@[no \\from part@ for clause '%a'@]"
+ Self.warning ~source ~once:true ~wkey:Self.wkey_missing_assigns
+ "@[no \\from part for clause@ '%a'.@ Assuming \\from \\nothing so that \
+ the analysis can continue, but be aware this is probably incorrect.@]"
Printer.pp_assigns (Writes no_from)
let get_assigns = function
@@ -124,8 +136,8 @@ let warn_on_missing_result_assigns kinstr kf spec =
if return_used && not (List.for_all assigns_result spec.spec_behavior)
then
let source = fst (Kernel_function.get_location kf) in
- Self.warning ~once:true ~source
- "@[no 'assigns \\result@ \\from ...'@ clause@ specified for@ function %a@]"
+ Self.warning ~wkey:Self.wkey_missing_assigns_result ~once:true ~source
+ "@[no 'assigns \\result \\from ...' clause specified for function %a@]"
Kernel_function.pretty kf
let reduce_to_valid_location kind term loc =
diff --git a/src/plugins/eva/self.ml b/src/plugins/eva/self.ml
index e270b09a08f63e30934c8ffd762ad6c6f9226f57..5fb3cb9223b4f218576e43a3e0d1796fd8e1bed9 100644
--- a/src/plugins/eva/self.ml
+++ b/src/plugins/eva/self.ml
@@ -138,8 +138,11 @@ let () = set_warn_status wkey_missing_loop_unroll Log.Winactive
let wkey_missing_loop_unroll_for = register_warn_category "loop-unroll:missing:for"
let () = set_warn_status wkey_missing_loop_unroll_for Log.Winactive
let wkey_signed_overflow = register_warn_category "signed-overflow"
-let wkey_invalid_assigns = register_warn_category "invalid-assigns"
+let wkey_invalid_assigns = register_warn_category "assigns:invalid-location"
let () = set_warn_status wkey_invalid_assigns Log.Wfeedback
+let wkey_missing_assigns = register_warn_category "assigns:missing"
+let () = set_warn_status wkey_missing_assigns Log.Werror
+let wkey_missing_assigns_result = register_warn_category "assigns:missing-result"
let wkey_experimental = register_warn_category "experimental"
let wkey_unknown_size = register_warn_category "unknown-size"
let wkey_ensures_false = register_warn_category "ensures-false"
diff --git a/src/plugins/eva/self.mli b/src/plugins/eva/self.mli
index 14c2020a03347a60098d0ae49bd02195e8031ce9..0e05e69bb710893b044ddad5061212023c3a36e2 100644
--- a/src/plugins/eva/self.mli
+++ b/src/plugins/eva/self.mli
@@ -69,6 +69,8 @@ val wkey_missing_loop_unroll : warn_category
val wkey_missing_loop_unroll_for : warn_category
val wkey_signed_overflow : warn_category
val wkey_invalid_assigns : warn_category
+val wkey_missing_assigns : warn_category
+val wkey_missing_assigns_result : warn_category
val wkey_experimental : warn_category
val wkey_unknown_size : warn_category
val wkey_ensures_false : warn_category
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index 1da3a3b77a3c13cd853560b8888d5e9d7842e666..22c098c54d1ad5f2e224a66dfc6f584f03da72f8 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -43,7 +43,7 @@
Neither code nor specification for function execlp_fallback_1,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function execlp
-[eva:invalid-assigns] exec.c:15:
+[eva:assigns:invalid-location] exec.c:15:
Completely invalid destination for assigns clause *(param1 + (0 ..)).
Ignoring.
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle b/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
index b81c4a205054408e1e93413c92a73dbf0a56745e..7a10dd4b7f203e009b806548b4d124e6c17d429d 100644
--- a/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
@@ -11,7 +11,7 @@
[eva] Analyzing a complete application starting at main
[eva] using specification for function __va_ioctl_void
[eva] using specification for function __va_ioctl_ptr
-[eva:invalid-assigns] ioctl.c:17:
+[eva:assigns:invalid-location] ioctl.c:17:
Completely invalid destination for assigns clause *((char *)argp + (0 ..)).
Ignoring.
[eva] using specification for function __va_ioctl_int
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index a4bc497d2519e7a7a1689ca4ddb35ae17826dbcc..0340f6ca2e98c45d9136b5748c41959e630fda5d 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -105,7 +105,7 @@
[kernel:annot:missing-spec] printf.c:71: Warning:
Neither code nor specification for function printf_fallback_1,
generating default assigns. See -generated-spec-* options for more info
-[eva:invalid-assigns] printf.c:71:
+[eva:assigns:invalid-location] printf.c:71:
Completely invalid destination for assigns clause *(param1 + (0 ..)).
Ignoring.
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/builtins/oracle/from_result.res.oracle b/tests/builtins/oracle/from_result.res.oracle
index 947ea0bed392daa6a55090a0d52fff7c3b265995..e1d0931d67dd12df046de54d7fe7de3d051fd1ee 100644
--- a/tests/builtins/oracle/from_result.res.oracle
+++ b/tests/builtins/oracle/from_result.res.oracle
@@ -31,7 +31,7 @@
[eva] computing for function foo <- main.
Called from from_result.c:37.
[eva] using specification for function foo
-[eva] from_result.c:29: Warning:
+[eva:assigns:missing-result] from_result.c:29: Warning:
no 'assigns \result \from ...' clause specified for function foo
[eva] Done for function foo
[eva] Recording results for main
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index d1109bb30e959c3ab228bc4c6ab6338e51d856e0..a3f654bb1e21208a52565ba90f0c5c354b160e9d 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -39,7 +39,7 @@
[eva] computing for function f <- invalid_assigns_imprecise <- main.
Called from imprecise.c:11.
[eva] using specification for function f
-[eva:invalid-assigns] imprecise.c:11:
+[eva:assigns:invalid-location] imprecise.c:11:
Completely invalid destination for assigns clause *p. Ignoring.
[eva] Done for function f
[eva] Recording results for invalid_assigns_imprecise
diff --git a/tests/fc_script/make-wrapper.t/run.t b/tests/fc_script/make-wrapper.t/run.t
index e70aaa31a57f87209702a00fbbae0814ef2f7258..936b5c2b4d211b3752646aae45cb0632350e66be 100644
--- a/tests/fc_script/make-wrapper.t/run.t
+++ b/tests/fc_script/make-wrapper.t/run.t
@@ -17,12 +17,10 @@ verbose output for Make.
[eva:recursion] make-wrapper.c:17:
detected recursive call
of function large_name_to_force_line_break_in_stack_msg.
- [eva] make-wrapper.c:17: User Error:
- Recursive call to large_name_to_force_line_break_in_stack_msg
- 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 large_name_to_force_line_break_in_stack_msg.
+ [eva:assigns:missing] make-wrapper.c:17: Warning:
+ Recursive call to large_name_to_force_line_break_in_stack_msg 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 large_name_to_force_line_break_in_stack_msg.
stack: large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:17 <-
large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:21 <-
rec :: make-wrapper.c:26 <-
diff --git a/tests/float/oracle/logic.0.res.oracle b/tests/float/oracle/logic.0.res.oracle
index 160f80b0c1ec85a4e31961bddad4dfcec0a7fb9d..8487b6d802ac2b199da7844d05639412d2474c02 100644
--- a/tests/float/oracle/logic.0.res.oracle
+++ b/tests/float/oracle/logic.0.res.oracle
@@ -334,7 +334,7 @@
[eva] computing for function my_ratio <- test_is_finite <- main.
Called from logic.i:181.
[eva] using specification for function my_ratio
-[eva] logic.i:153: Warning:
+[eva:assigns:missing-result] logic.i:153: Warning:
no 'assigns \result \from ...' clause specified for function my_ratio
[eva] Done for function my_ratio
[eva] computing for function my_ratio_body <- test_is_finite <- main.
diff --git a/tests/float/oracle/logic.1.res.oracle b/tests/float/oracle/logic.1.res.oracle
index 10df71b62bdfd6efa259cf507b19d69dc1868057..7ae4cb5160b7afb9acc6e18dc05f3aca34a18ce6 100644
--- a/tests/float/oracle/logic.1.res.oracle
+++ b/tests/float/oracle/logic.1.res.oracle
@@ -336,7 +336,7 @@
[eva] computing for function my_ratio <- test_is_finite <- main.
Called from logic.i:181.
[eva] using specification for function my_ratio
-[eva] logic.i:153: Warning:
+[eva:assigns:missing-result] logic.i:153: Warning:
no 'assigns \result \from ...' clause specified for function my_ratio
[eva] Done for function my_ratio
[eva] computing for function my_ratio_body <- test_is_finite <- main.
diff --git a/tests/impact/call.i b/tests/impact/call.i
index 65a046489c1fedd09ad8f9488da1f8a52c2622ae..470cb61c0b654fa0147362c70e98a2cb1ce07472 100644
--- a/tests/impact/call.i
+++ b/tests/impact/call.i
@@ -38,7 +38,7 @@ void main2(int x) {
/* ************************************************************************* */
-/*@ assigns G; */
+/*@ assigns G \from \nothing; */
void p3 (int);
void test3 (void) {
diff --git a/tests/impact/oracle/call.2.res.oracle b/tests/impact/oracle/call.2.res.oracle
index 2d7016cb262fe25ca6633576337ee357d677d885..083752beda8c27c51bff76462387af17eec97c59 100644
--- a/tests/impact/oracle/call.2.res.oracle
+++ b/tests/impact/oracle/call.2.res.oracle
@@ -13,7 +13,6 @@
[eva] computing for function p3 <- test3 <- call_test3 <- main3.
Called from call.i:45.
[eva] using specification for function p3
-[eva] call.i:41: Warning: no \from part for clause 'assigns G;'
[eva] Done for function p3
[kernel:annot:missing-spec] call.i:45: Warning:
Neither code nor specification for function p2,
@@ -44,7 +43,10 @@
[pdg] done for function test3
[pdg] computing for function p3
[pdg] done for function p3
+[pdg] computing for function p2
+[pdg] done for function p2
[impact] impacted statements of stmt(s) 30 are:
- call.i:45 (sid 22): p3(1);call.i:49 (sid 26): test3();
+ call.i:45 (sid 21): if(X) <..>call.i:45 (sid 22): p3(1);
+ call.i:45 (sid 23): p2(0);call.i:49 (sid 26): test3();
call.i:55 (sid 31): call_test3();
[impact] analysis done
diff --git a/tests/libc/oracle/libgen_h.res.oracle b/tests/libc/oracle/libgen_h.res.oracle
index 9e5405c1b5985d48f0095eaa36feacc6be89081d..d7df73fb9973ed6f8f9b3e81949ae7a8664a105c 100644
--- a/tests/libc/oracle/libgen_h.res.oracle
+++ b/tests/libc/oracle/libgen_h.res.oracle
@@ -15,7 +15,7 @@
Called from libgen_h.c:11.
[eva] libgen_h.c:11:
function basename: precondition 'null_or_valid_string_path' got status valid.
-[eva:invalid-assigns] libgen_h.c:11:
+[eva:assigns:invalid-location] libgen_h.c:11:
Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
[eva] Done for function basename
[eva:alarm] libgen_h.c:12: Warning: assertion got status unknown.
@@ -30,7 +30,7 @@
Called from libgen_h.c:16.
[eva] libgen_h.c:16:
function dirname: precondition 'null_or_valid_string_path' got status valid.
-[eva:invalid-assigns] libgen_h.c:16:
+[eva:assigns:invalid-location] libgen_h.c:16:
Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
[eva] Done for function dirname
[eva:alarm] libgen_h.c:17: Warning: assertion got status unknown.
diff --git a/tests/libc/oracle/search_h.res.oracle b/tests/libc/oracle/search_h.res.oracle
index f3a24652dc25a198f18e79333b456cd0b9cff435..9367d7f9d122dbdff1e2b8e2473296626b6fc96c 100644
--- a/tests/libc/oracle/search_h.res.oracle
+++ b/tests/libc/oracle/search_h.res.oracle
@@ -41,7 +41,7 @@
[eva] computing for function tsearch <- main.
Called from search_h.c:34.
[eva] using specification for function tsearch
-[eva:invalid-assigns] search_h.c:34:
+[eva:assigns:invalid-location] search_h.c:34:
Completely invalid destination for assigns clause *compar. Ignoring.
[eva] Done for function tsearch
[eva:alarm] search_h.c:40: Warning:
@@ -61,7 +61,7 @@
[eva] computing for function twalk <- main.
Called from search_h.c:46.
[eva] using specification for function twalk
-[eva:invalid-assigns] search_h.c:46:
+[eva:assigns:invalid-location] search_h.c:46:
Completely invalid destination for assigns clause *action. Ignoring.
[eva] Done for function twalk
[eva] Recording results for main
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 1219ddf39fa0fd1ac3e62a1ef6bba43ab1dfb7b9..af6af2df61181de0c2eaff470c8ea9cd005698ad 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -83,7 +83,7 @@
function sigprocmask: precondition 'valid_oldset_or_null' got status valid.
[eva] signal_h.c:35:
function sigprocmask: precondition 'separation' got status valid.
-[eva:invalid-assigns] signal_h.c:35:
+[eva:assigns:invalid-location] signal_h.c:35:
Completely invalid destination for assigns clause *oldset. Ignoring.
[eva] Done for function sigprocmask
[eva] computing for function sigprocmask <- main.
@@ -145,7 +145,7 @@
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] signal_h.c:51:
function sigaction: precondition 'separation,separated_acts' got status valid.
-[eva:invalid-assigns] signal_h.c:51:
+[eva:assigns:invalid-location] signal_h.c:51:
Completely invalid destination for assigns clause *oldact. Ignoring.
[eva] Done for function sigaction
[eva] signal_h.c:55: assertion 'valid_nsig' got status valid.
diff --git a/tests/libc/oracle/socket_h.res.oracle b/tests/libc/oracle/socket_h.res.oracle
index d19a86d1f49df0b6281ef306b0e3f9ace0bc4edf..665bc6a7f7d34628cfcad314be829e731a507074 100644
--- a/tests/libc/oracle/socket_h.res.oracle
+++ b/tests/libc/oracle/socket_h.res.oracle
@@ -93,9 +93,9 @@
function recvfrom: precondition 'valid_buffer_length' got status valid.
[eva] socket_h.c:37:
function recvfrom: precondition 'valid_addrbuf_or_null,initialization' got status valid.
-[eva:invalid-assigns] socket_h.c:37:
+[eva:assigns:invalid-location] socket_h.c:37:
Completely invalid destination for assigns clause *addrbuf_len. Ignoring.
-[eva:invalid-assigns] socket_h.c:37:
+[eva:assigns:invalid-location] socket_h.c:37:
Completely invalid destination
for assigns clause *((char *)addrbuf + (0 .. \old(*addrbuf_len) - 1)).
Ignoring.
diff --git a/tests/libc/oracle/stdio_h.res.oracle b/tests/libc/oracle/stdio_h.res.oracle
index 501e3cbf6721700b16630e39626ebf133fa82927..5c49c9788af76c5b30f529a4432476ed64a9498c 100644
--- a/tests/libc/oracle/stdio_h.res.oracle
+++ b/tests/libc/oracle/stdio_h.res.oracle
@@ -204,7 +204,7 @@
[eva:libc:unsupported-spec] stdio_h.c:99: Warning:
The specification of function 'vscanf' is currently not supported by Eva.
Consider adding 'FRAMAC_SHARE/libc/stdio.c' to the analyzed source files.
-[eva] FRAMAC_SHARE/libc/stdio.h:276: Warning:
+[eva:assigns:missing-result] FRAMAC_SHARE/libc/stdio.h:276: Warning:
no 'assigns \result \from ...' clause specified for function vscanf
[eva] Done for function vscanf
[eva] Recording results for caller_stub_for_vscanf
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 6990b87fa3ba5e9731ee7c3dc7d88f2d7553a46f..ba0970af431e10d22ffccfd53459b858c7a719c2 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -174,7 +174,7 @@
function strtok: precondition 'separation' got status valid.
[eva] string_h.c:82:
function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status valid.
-[eva:invalid-assigns] string_h.c:82:
+[eva:assigns:invalid-location] string_h.c:82:
Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
[eva] Done for function strtok
[eva:alarm] string_h.c:83: Warning: check got status unknown.
@@ -273,7 +273,7 @@
function strtok_r: precondition 'valid_saveptr' got status valid.
[eva] string_h.c:112:
function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status valid.
-[eva:invalid-assigns] string_h.c:112:
+[eva:assigns:invalid-location] string_h.c:112:
Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
[eva] Done for function strtok_r
[eva:alarm] string_h.c:113: Warning: check got status unknown.
@@ -500,7 +500,7 @@
Called from string_h.c:204.
[eva] string_h.c:204:
function strsep: precondition 'valid_stringp' got status valid.
-[eva:invalid-assigns] string_h.c:204:
+[eva:assigns:invalid-location] string_h.c:204:
Completely invalid destination for assigns clause *(*(stringp + (0 ..))).
Ignoring.
[eva] Done for function strsep
diff --git a/tests/libc/oracle/sys_select.res.oracle b/tests/libc/oracle/sys_select.res.oracle
index 1de303ea58ff3397cf97d94a8be16dbea3cc469a..730b009517292caee22f46aa4289fa76e21fb5eb 100644
--- a/tests/libc/oracle/sys_select.res.oracle
+++ b/tests/libc/oracle/sys_select.res.oracle
@@ -68,9 +68,9 @@
[eva] sys_select.c:31:
function select: precondition 'errorfds' got status valid.
[eva] sys_select.c:31: function select: precondition 'timeout' got status valid.
-[eva:invalid-assigns] sys_select.c:31:
+[eva:assigns:invalid-location] sys_select.c:31:
Completely invalid destination for assigns clause *writefds. Ignoring.
-[eva:invalid-assigns] sys_select.c:31:
+[eva:assigns:invalid-location] sys_select.c:31:
Completely invalid destination for assigns clause *errorfds. Ignoring.
[eva] Done for function select
[eva] computing for function FD_ISSET <- main.
diff --git a/tests/libc/oracle/sys_sendfile_h.res.oracle b/tests/libc/oracle/sys_sendfile_h.res.oracle
index 68cffb5124d14d5e0cc2feec3db4179d16f4bdab..0a2dd0c2fa31de40dda51a9b4ccc42dc41771514 100644
--- a/tests/libc/oracle/sys_sendfile_h.res.oracle
+++ b/tests/libc/oracle/sys_sendfile_h.res.oracle
@@ -52,7 +52,7 @@
function sendfile: precondition 'valid_offset_or_null' got status valid.
[eva] sys_sendfile_h.c:19:
function sendfile: precondition 'initialization,offset' got status valid.
-[eva:invalid-assigns] sys_sendfile_h.c:19:
+[eva:assigns:invalid-location] sys_sendfile_h.c:19:
Completely invalid destination for assigns clause *offset. Ignoring.
[eva] Done for function sendfile
[eva] computing for function close <- main.
diff --git a/tests/libc/oracle/sys_time_h.res.oracle b/tests/libc/oracle/sys_time_h.res.oracle
index 5cf6085db2850f98415b2ee55f0537ae30c03ec6..ec2bc7917c503a1476ffbe6bde69c91e378ba89c 100644
--- a/tests/libc/oracle/sys_time_h.res.oracle
+++ b/tests/libc/oracle/sys_time_h.res.oracle
@@ -11,7 +11,7 @@
function setitimer: precondition 'valid_new_value' got status valid.
[eva] sys_time_h.c:6:
function setitimer: precondition 'old_value_null_or_valid' got status valid.
-[eva:invalid-assigns] sys_time_h.c:6:
+[eva:assigns:invalid-location] sys_time_h.c:6:
Completely invalid destination for assigns clause *old_value. Ignoring.
[eva] Done for function setitimer
[eva] sys_time_h.c:7: assertion got status valid.
diff --git a/tests/libc/oracle/time_h.res.oracle b/tests/libc/oracle/time_h.res.oracle
index f8f4edbaefc073e47b71e067120b8e9ad3d4adf0..e0e2f3af74f1a814cd31b761eaf0eb097692d32b 100644
--- a/tests/libc/oracle/time_h.res.oracle
+++ b/tests/libc/oracle/time_h.res.oracle
@@ -37,7 +37,7 @@
function nanosleep: precondition 'valid_nanosecs' got status valid.
[eva] time_h.c:22:
function nanosleep: precondition 'valid_remaining_or_null' got status valid.
-[eva:invalid-assigns] time_h.c:22:
+[eva:assigns:invalid-location] time_h.c:22:
Completely invalid destination for assigns clause *rmtp. Ignoring.
[eva] Done for function nanosleep
[eva] computing for function nanosleep <- main.
diff --git a/tests/libc/oracle/uchar_h.res.oracle b/tests/libc/oracle/uchar_h.res.oracle
index 82a0ae391735acd03045073e97a1f0bf7b214cc4..dbf44b8c1c81a06790c29759b8a1f01976d6d7a5 100644
--- a/tests/libc/oracle/uchar_h.res.oracle
+++ b/tests/libc/oracle/uchar_h.res.oracle
@@ -7,7 +7,7 @@
[eva] computing for function mbrtoc8 <- main.
Called from uchar_h.c:10.
[eva] using specification for function mbrtoc8
-[eva:invalid-assigns] uchar_h.c:10:
+[eva:assigns:invalid-location] uchar_h.c:10:
Completely invalid destination for assigns clause *ps. Ignoring.
[eva] Done for function mbrtoc8
[eva] computing for function mbrtoc8 <- main.
@@ -15,14 +15,14 @@
[eva] Done for function mbrtoc8
[eva] computing for function mbrtoc8 <- main.
Called from uchar_h.c:12.
-[eva:invalid-assigns] uchar_h.c:12:
+[eva:assigns:invalid-location] uchar_h.c:12:
Completely invalid destination for assigns clause *(pc8 + 0). Ignoring.
[eva] Done for function mbrtoc8
[eva] computing for function mbrtoc8 <- main.
Called from uchar_h.c:13.
-[eva:invalid-assigns] uchar_h.c:13:
+[eva:assigns:invalid-location] uchar_h.c:13:
Completely invalid destination for assigns clause *(pc8 + 0). Ignoring.
-[eva:invalid-assigns] uchar_h.c:13:
+[eva:assigns:invalid-location] uchar_h.c:13:
Completely invalid destination for assigns clause *ps. Ignoring.
[eva] Done for function mbrtoc8
[eva] computing for function c8rtomb <- main.
@@ -31,22 +31,22 @@
[eva] Done for function c8rtomb
[eva] computing for function c8rtomb <- main.
Called from uchar_h.c:15.
-[eva:invalid-assigns] uchar_h.c:15:
+[eva:assigns:invalid-location] uchar_h.c:15:
Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
Ignoring.
[eva] Done for function c8rtomb
[eva] computing for function c8rtomb <- main.
Called from uchar_h.c:16.
-[eva:invalid-assigns] uchar_h.c:16:
+[eva:assigns:invalid-location] uchar_h.c:16:
Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
Ignoring.
-[eva:invalid-assigns] uchar_h.c:16:
+[eva:assigns:invalid-location] uchar_h.c:16:
Completely invalid destination for assigns clause *ps. Ignoring.
[eva] Done for function c8rtomb
[eva] computing for function mbrtoc16 <- main.
Called from uchar_h.c:20.
[eva] using specification for function mbrtoc16
-[eva:invalid-assigns] uchar_h.c:20:
+[eva:assigns:invalid-location] uchar_h.c:20:
Completely invalid destination for assigns clause *ps. Ignoring.
[eva] Done for function mbrtoc16
[eva] computing for function mbrtoc16 <- main.
@@ -54,14 +54,14 @@
[eva] Done for function mbrtoc16
[eva] computing for function mbrtoc16 <- main.
Called from uchar_h.c:22.
-[eva:invalid-assigns] uchar_h.c:22:
+[eva:assigns:invalid-location] uchar_h.c:22:
Completely invalid destination for assigns clause *(pc16 + 0). Ignoring.
[eva] Done for function mbrtoc16
[eva] computing for function mbrtoc16 <- main.
Called from uchar_h.c:23.
-[eva:invalid-assigns] uchar_h.c:23:
+[eva:assigns:invalid-location] uchar_h.c:23:
Completely invalid destination for assigns clause *(pc16 + 0). Ignoring.
-[eva:invalid-assigns] uchar_h.c:23:
+[eva:assigns:invalid-location] uchar_h.c:23:
Completely invalid destination for assigns clause *ps. Ignoring.
[eva] Done for function mbrtoc16
[eva] computing for function c16rtomb <- main.
@@ -70,22 +70,22 @@
[eva] Done for function c16rtomb
[eva] computing for function c16rtomb <- main.
Called from uchar_h.c:25.
-[eva:invalid-assigns] uchar_h.c:25:
+[eva:assigns:invalid-location] uchar_h.c:25:
Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
Ignoring.
[eva] Done for function c16rtomb
[eva] computing for function c16rtomb <- main.
Called from uchar_h.c:26.
-[eva:invalid-assigns] uchar_h.c:26:
+[eva:assigns:invalid-location] uchar_h.c:26:
Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
Ignoring.
-[eva:invalid-assigns] uchar_h.c:26:
+[eva:assigns:invalid-location] uchar_h.c:26:
Completely invalid destination for assigns clause *ps. Ignoring.
[eva] Done for function c16rtomb
[eva] computing for function mbrtoc32 <- main.
Called from uchar_h.c:30.
[eva] using specification for function mbrtoc32
-[eva:invalid-assigns] uchar_h.c:30:
+[eva:assigns:invalid-location] uchar_h.c:30:
Completely invalid destination for assigns clause *ps. Ignoring.
[eva] Done for function mbrtoc32
[eva] computing for function mbrtoc32 <- main.
@@ -93,14 +93,14 @@
[eva] Done for function mbrtoc32
[eva] computing for function mbrtoc32 <- main.
Called from uchar_h.c:32.
-[eva:invalid-assigns] uchar_h.c:32:
+[eva:assigns:invalid-location] uchar_h.c:32:
Completely invalid destination for assigns clause *(pc32 + 0). Ignoring.
[eva] Done for function mbrtoc32
[eva] computing for function mbrtoc32 <- main.
Called from uchar_h.c:33.
-[eva:invalid-assigns] uchar_h.c:33:
+[eva:assigns:invalid-location] uchar_h.c:33:
Completely invalid destination for assigns clause *(pc32 + 0). Ignoring.
-[eva:invalid-assigns] uchar_h.c:33:
+[eva:assigns:invalid-location] uchar_h.c:33:
Completely invalid destination for assigns clause *ps. Ignoring.
[eva] Done for function mbrtoc32
[eva] computing for function c32rtomb <- main.
@@ -109,16 +109,16 @@
[eva] Done for function c32rtomb
[eva] computing for function c32rtomb <- main.
Called from uchar_h.c:35.
-[eva:invalid-assigns] uchar_h.c:35:
+[eva:assigns:invalid-location] uchar_h.c:35:
Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
Ignoring.
[eva] Done for function c32rtomb
[eva] computing for function c32rtomb <- main.
Called from uchar_h.c:36.
-[eva:invalid-assigns] uchar_h.c:36:
+[eva:assigns:invalid-location] uchar_h.c:36:
Completely invalid destination for assigns clause *(s + (0 .. 16 - 1)).
Ignoring.
-[eva:invalid-assigns] uchar_h.c:36:
+[eva:assigns:invalid-location] uchar_h.c:36:
Completely invalid destination for assigns clause *ps. Ignoring.
[eva] Done for function c32rtomb
[eva] Recording results for main
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index 87a6533a18367d35d29ca8e57677ab9d3089565a..5a6d4556056dd40051fd1efbfbd7b23fd4407ee5 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -37,17 +37,17 @@
},
"warning-categories": {
"enabled": [
- "*", "alarm", "builtins", "builtins:missing-spec",
- "builtins:override", "ensures-false", "experimental", "garbled-mix",
- "libc", "libc:unsupported-spec", "locals-escaping", "loop-unroll",
- "malloc", "malloc:imprecise", "signed-overflow", "taint",
- "unknown-size"
+ "*", "alarm", "assigns", "assigns:missing", "assigns:missing-result",
+ "builtins", "builtins:missing-spec", "builtins:override",
+ "ensures-false", "experimental", "garbled-mix", "libc",
+ "libc:unsupported-spec", "locals-escaping", "loop-unroll", "malloc",
+ "malloc:imprecise", "signed-overflow", "taint", "unknown-size"
],
"disabled": [
- "garbled-mix:assigns", "garbled-mix:summary", "garbled-mix:write",
- "invalid-assigns", "loop-unroll:auto", "loop-unroll:missing",
- "loop-unroll:missing:for", "loop-unroll:partial", "malloc:weak",
- "recursion", "watchpoint"
+ "assigns:invalid-location", "garbled-mix:assigns",
+ "garbled-mix:summary", "garbled-mix:write", "loop-unroll:auto",
+ "loop-unroll:missing", "loop-unroll:missing:for",
+ "loop-unroll:partial", "malloc:weak", "recursion", "watchpoint"
]
}
},
diff --git a/tests/sparecode/bts324.i b/tests/sparecode/bts324.i
index b41f4dc2c193f58846ef9acfcd0632223f73e6c4..e201f7edc8f489d5d19d96d6d152c47601ec0a78 100644
--- a/tests/sparecode/bts324.i
+++ b/tests/sparecode/bts324.i
@@ -8,10 +8,10 @@
int i0, o0;
-/*@ assigns i0, o0 ; */
+/*@ assigns i0, o0 \from \nothing; */
void loop_body (void) ;
-/*@ assigns *p_res; */
+/*@ assigns *p_res \from indirect:p_res; */
void init (int * p_res) ;
int is_ko = -1;
diff --git a/tests/sparecode/oracle/bts324.0.res.oracle b/tests/sparecode/oracle/bts324.0.res.oracle
index 980e5daafeeac0f2132bd1deb8786c2cc34d3421..42219df344b6d7cdedcd7f19bf15cf33f59280b1 100644
--- a/tests/sparecode/oracle/bts324.0.res.oracle
+++ b/tests/sparecode/oracle/bts324.0.res.oracle
@@ -11,12 +11,10 @@
[eva] computing for function init <- main.
Called from bts324.i:19.
[eva] using specification for function init
-[eva] bts324.i:14: Warning: no \from part for clause 'assigns *p_res;'
[eva] Done for function init
[eva] computing for function loop_body <- main.
Called from bts324.i:22.
[eva] using specification for function loop_body
-[eva] bts324.i:11: Warning: no \from part for clause 'assigns i0, o0;'
[eva] Done for function loop_body
[eva:partition] bts324.i:21: starting to merge loop iterations
[eva] computing for function loop_body <- main.
@@ -55,7 +53,8 @@
[sparecode] remove unused global declarations...
[sparecode] result in new project 'default without sparecode'.
/* Generated by Frama-C */
-/*@ assigns *p_res; */
+/*@ assigns *p_res;
+ assigns *p_res \from (indirect: p_res); */
void init(int *p_res);
int is_ko = -1;
diff --git a/tests/sparecode/oracle/bts324.1.res.oracle b/tests/sparecode/oracle/bts324.1.res.oracle
index 08edb8bad3a52849427a4ecea8c2607c05216908..5eb1a9aa0a781997680ce29d76deb79351b5764f 100644
--- a/tests/sparecode/oracle/bts324.1.res.oracle
+++ b/tests/sparecode/oracle/bts324.1.res.oracle
@@ -11,12 +11,10 @@
[eva] computing for function init <- main_bis.
Called from bts324.i:26.
[eva] using specification for function init
-[eva] bts324.i:14: Warning: no \from part for clause 'assigns *p_res;'
[eva] Done for function init
[eva] computing for function loop_body <- main_bis.
Called from bts324.i:29.
[eva] using specification for function loop_body
-[eva] bts324.i:11: Warning: no \from part for clause 'assigns i0, o0;'
[eva] Done for function loop_body
[eva:partition] bts324.i:28: starting to merge loop iterations
[eva] computing for function loop_body <- main_bis.
@@ -59,10 +57,13 @@
/* Generated by Frama-C */
int i0;
int o0;
-/*@ assigns i0, o0; */
+/*@ assigns i0, o0;
+ assigns i0 \from \nothing;
+ assigns o0 \from \nothing; */
void loop_body(void);
-/*@ assigns *p_res; */
+/*@ assigns *p_res;
+ assigns *p_res \from (indirect: p_res); */
void init(int *p_res);
int is_ko = -1;
diff --git a/tests/sparecode/oracle/bts324.2.res.oracle b/tests/sparecode/oracle/bts324.2.res.oracle
index f9473d7383052c8eb9f8a8f3888d58e195b53d47..40be8d5e3742259109f069ce3fdee2ed49dbec84 100644
--- a/tests/sparecode/oracle/bts324.2.res.oracle
+++ b/tests/sparecode/oracle/bts324.2.res.oracle
@@ -11,12 +11,10 @@
[eva] computing for function init <- main_ter.
Called from bts324.i:35.
[eva] using specification for function init
-[eva] bts324.i:14: Warning: no \from part for clause 'assigns *p_res;'
[eva] Done for function init
[eva] computing for function loop_body <- main_ter.
Called from bts324.i:39.
[eva] using specification for function loop_body
-[eva] bts324.i:11: Warning: no \from part for clause 'assigns i0, o0;'
[eva] Done for function loop_body
[eva:partition] bts324.i:37: starting to merge loop iterations
[eva] computing for function loop_body <- main_ter.
@@ -59,10 +57,13 @@
/* Generated by Frama-C */
int i0;
int o0;
-/*@ assigns i0, o0; */
+/*@ assigns i0, o0;
+ assigns i0 \from \nothing;
+ assigns o0 \from \nothing; */
void loop_body(void);
-/*@ assigns *p_res; */
+/*@ assigns *p_res;
+ assigns *p_res \from (indirect: p_res); */
void init(int *p_res);
int is_ko = -1;
diff --git a/tests/sparecode/oracle/bts334.0.res.oracle b/tests/sparecode/oracle/bts334.0.res.oracle
index 62c9ca46f75a407ecb37953cc4f6901735272f23..4a326965681d9c718d66b3187482dc323c4673a4 100644
--- a/tests/sparecode/oracle/bts334.0.res.oracle
+++ b/tests/sparecode/oracle/bts334.0.res.oracle
@@ -18,7 +18,7 @@
[eva] computing for function init <- main_init.
Called from bts334.i:66.
[eva] using specification for function init
-[eva] bts334.i:61: Warning:
+[eva:assigns:missing-result] bts334.i:61: Warning:
no 'assigns \result \from ...' clause specified for function init
[kernel] bts334.i:66: Warning: keeping only assigns from behaviors: default
[eva] Done for function init
diff --git a/tests/sparecode/oracle/bts334.1.res.oracle b/tests/sparecode/oracle/bts334.1.res.oracle
index 06bc529abee892df2a4156cdecd0988a4b0ff9b4..76a21c8a6cc5196f49b3011c32c447c54329ea05 100644
--- a/tests/sparecode/oracle/bts334.1.res.oracle
+++ b/tests/sparecode/oracle/bts334.1.res.oracle
@@ -18,7 +18,7 @@
[eva] computing for function init <- main_init.
Called from bts334.i:66.
[eva] using specification for function init
-[eva] bts334.i:61: Warning:
+[eva:assigns:missing-result] bts334.i:61: Warning:
no 'assigns \result \from ...' clause specified for function init
[kernel] bts334.i:66: Warning: keeping only assigns from behaviors: default
[eva] Done for function init
diff --git a/tests/sparecode/oracle/bts334.2.res.oracle b/tests/sparecode/oracle/bts334.2.res.oracle
index a03e12ab714af782ecd637c6b1a0c54cb27658d8..5ca5138f126b75e665ee87ad34519052c7ec4e26 100644
--- a/tests/sparecode/oracle/bts334.2.res.oracle
+++ b/tests/sparecode/oracle/bts334.2.res.oracle
@@ -17,7 +17,7 @@
[eva] computing for function init <- main_init.
Called from bts334.i:66.
[eva] using specification for function init
-[eva] bts334.i:61: Warning:
+[eva:assigns:missing-result] bts334.i:61: Warning:
no 'assigns \result \from ...' clause specified for function init
[kernel] bts334.i:66: Warning: keeping only assigns from behaviors: default
[eva] Done for function init
diff --git a/tests/spec/default_assigns_bts0966.i b/tests/spec/default_assigns_bts0966.i
index 3aceabc5aabc09f475734f7e3f3e996d6c809a72..42806105a7681a827569d8d6311177d014fc4b54 100644
--- a/tests/spec/default_assigns_bts0966.i
+++ b/tests/spec/default_assigns_bts0966.i
@@ -12,17 +12,17 @@ enum states {
};
// contract with missing "complete behaviors"
-/*@
+/*@
ensures \true;
behavior from_init:
assumes auto_states[Init] == 1;
ensures (auto_states[Copy] == 1) && (auto_states[Init] == 0);
- assigns auto_states[Init], auto_states[Copy];
+ assigns auto_states[Init], auto_states[Copy] \from \nothing;
behavior from_other:
assumes (auto_states[Init] == 0);
assigns \nothing;
-
+
*/
void copy(int x);
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 67f8b8d40922d3f1bc425e9010b77c45b54c2b12..b83679d2c9bf9c06f9cc2b1d60fe5a8fc2a20c17 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -6,7 +6,7 @@ PLUGIN:
*/
/*@ check lemma easy_proof: \false; */ // should not be put in any environment
/*@ check requires f_valid_x: \valid(x);
- assigns *x;
+ assigns *x \from indirect:x;
check ensures f_init_x: *x == 0;
*/
void f(int* x) {
diff --git a/tests/spec/oracle/array_typedef.res.oracle b/tests/spec/oracle/array_typedef.res.oracle
index 37ea592e18d1c8d208547bd76b7f772ed3c43195..067a46f618bb8c26318818c1ee5c513613b099f5 100644
--- a/tests/spec/oracle/array_typedef.res.oracle
+++ b/tests/spec/oracle/array_typedef.res.oracle
@@ -24,7 +24,6 @@
[eva] computing for function send_addr <- send_msg <- main.
Called from array_typedef.c:15.
[eva] using specification for function send_addr
-[eva] array_typedef.c:12: Warning: no \from part for clause 'assigns \empty;'
[eva] Done for function send_addr
[eva] Recording results for send_msg
[eva] Done for function send_msg
diff --git a/tests/spec/oracle/default_assigns_bts0966.res.oracle b/tests/spec/oracle/default_assigns_bts0966.res.oracle
index 728ce51af93543be68e905a91274e29a393ded31..69fa1490ad0a57f860c6a117cc4f4d2134e0cc02 100644
--- a/tests/spec/oracle/default_assigns_bts0966.res.oracle
+++ b/tests/spec/oracle/default_assigns_bts0966.res.oracle
@@ -6,8 +6,6 @@
Neither code nor explicit assigns for function copy,
generating default clauses from the specification. See -generated-spec-* options for more info
[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];'
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
auto_states[0] ∈ {0}
@@ -20,7 +18,7 @@
In this function, 7 statements reached (out of 7): 100% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 1 warning
+ by the Eva analyzer: 0 errors 0 warnings
by the Frama-C kernel: 0 errors 1 warning
----------------------------------------------------------------------------
0 alarms generated by the analysis.
@@ -37,11 +35,15 @@ enum states {
int auto_states[4];
/*@ ensures \true;
assigns auto_states[Copy], auto_states[Init];
+ assigns auto_states[Copy] \from \nothing;
+ assigns auto_states[Init] \from \nothing;
behavior from_init:
assumes auto_states[Init] ≡ 1;
ensures auto_states[Copy] ≡ 1 ∧ auto_states[Init] ≡ 0;
assigns auto_states[Init], auto_states[Copy];
+ assigns auto_states[Init] \from \nothing;
+ assigns auto_states[Copy] \from \nothing;
behavior from_other:
assumes auto_states[Init] ≡ 0;
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
index 0fb9927aa934253ed3519b9fda6f0dbfd3d2adfe..b56fab66c807791a015c86d59d318af3a852b82f 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -7,7 +7,6 @@
[eva] using specification for function f
[eva:alarm] generalized_check.i:24: Warning:
function f: precondition 'f_valid_x' got status unknown.
-[eva] generalized_check.i:9: Warning: no \from part for clause 'assigns *x;'
[eva:alarm] generalized_check.i:25: Warning:
check 'main_valid_ko' got status unknown.
[eva:alarm] generalized_check.i:26: Warning:
@@ -29,9 +28,7 @@
2 functions analyzed (out of 3): 66% coverage.
In these functions, 25 statements reached (out of 25): 100% coverage.
----------------------------------------------------------------------------
- Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 1 warning
- by the Frama-C kernel: 0 errors 0 warnings
+ No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
1 alarm generated by the analysis:
1 access to uninitialized left-values
diff --git a/tests/spec/oracle/generalized_check.1.res.oracle b/tests/spec/oracle/generalized_check.1.res.oracle
index 7e0503ac2ae81e3733b87703e497dee35f843332..258bcbb81d66189d0c98d11b01fb5a92c80d2df4 100644
--- a/tests/spec/oracle/generalized_check.1.res.oracle
+++ b/tests/spec/oracle/generalized_check.1.res.oracle
@@ -5,6 +5,7 @@
/*@ check requires f_valid_x: \valid(x);
check ensures f_init_x: *\old(x) ≡ 0;
assigns *x;
+ assigns *x \from (indirect: x);
*/
void f(int *x)
{
diff --git a/tests/spec/oracle/statement_behavior.res.oracle b/tests/spec/oracle/statement_behavior.res.oracle
index f3594a563c4b2f46589fb8d4e9997c34ba7ce8ff..40a469ca62195bd3f37f6c333343033644096ee5 100644
--- a/tests/spec/oracle/statement_behavior.res.oracle
+++ b/tests/spec/oracle/statement_behavior.res.oracle
@@ -6,8 +6,6 @@
[eva] computing for function pfsqopfc <- main.
Called from statement_behavior.c:23.
-[eva] statement_behavior.c:10: Warning:
- no \from part for clause 'assigns five_times;'
[eva:alarm] statement_behavior.c:17: Warning: assertion got status unknown.
[eva:alarm] statement_behavior.c:5: Warning:
function pfsqopfc: postcondition got status unknown.
diff --git a/tests/spec/statement_behavior.c b/tests/spec/statement_behavior.c
index c8834f72c8ea2102631e6060ac6dc0c3acc9cc3c..3a3c8ae51da0558a06d0c8f340c37136051d695a 100644
--- a/tests/spec/statement_behavior.c
+++ b/tests/spec/statement_behavior.c
@@ -7,7 +7,7 @@ PLUGIN: eva,inout,scope
int pfsqopfc(int x) {
int five_times;
/*@
- assigns five_times;
+ assigns five_times \from x;
ensures five_times == (int)(5 * x);
*/
asm ("leal (%1,%1,4), %0"
diff --git a/tests/value/assigns.i b/tests/value/assigns.i
index a36a92073e6020daa3bbddc084c3d5b80a5ab376..459bb27daa165d8ace3dc1c45651781cb4baeeed 100644
--- a/tests/value/assigns.i
+++ b/tests/value/assigns.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-print -inout"
+ STDOPT: +"-print -inout -eva-warn-key assigns:missing=active"
*/
volatile int v;
int G;
@@ -50,7 +50,7 @@ void main1(void)
g(2 * (int)(&T) );
h((int*)(2 * (int)(&t3)));
-
+
j((int*)(T+9));
assigns_post(18);
diff --git a/tests/value/lock.i b/tests/value/lock.i
index a73d927e72c3ade360db55650f887241d40fa739..e928c1203b168c3d93f79ffa520d666fe40e491f 100644
--- a/tests/value/lock.i
+++ b/tests/value/lock.i
@@ -18,7 +18,7 @@
/*@
requires !(locked(m));
ensures locked(m);
- assigns ghost_loctable[0..99];
+ assigns ghost_loctable[0..99] \from indirect:*m;
*/
void acquire_lock(struct mutex *m);
@@ -26,14 +26,14 @@ void acquire_lock(struct mutex *m);
/*@
requires locked(m);
ensures !(locked(m));
- assigns ghost_loctable[..];
+ assigns ghost_loctable[..] \from indirect:*m;
*/
void release_lock(struct mutex *m);
/*@
requires !(locked(m));
- assigns ghost_loctable[..];
+ assigns ghost_loctable[..] \from indirect:*m;
behavior success:
ensures (\result != 0) ==> locked(m);
@@ -43,11 +43,12 @@ void release_lock(struct mutex *m);
*/
int try_acquire_lock(struct mutex *m);
-struct mutex *pmutex;
+struct mutex { int __id; };
+extern struct mutex mutex;
-/*@ requires !(locked(pmutex)); */
+/*@ requires !(locked(&mutex)); */
void locks0_good(int flag)
{
- acquire_lock(pmutex);
- release_lock(pmutex);
+ acquire_lock(&mutex);
+ release_lock(&mutex);
}
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index a0290280a5fc1643491abf4785f33b59f681ddb9..5de66d92722b49b5da0103914fd328e5cdf8b940 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -79,9 +79,10 @@
[eva] computing for function assigns_post <- main1 <- main.
Called from assigns.i:56.
[eva] using specification for function assigns_post
-[eva] assigns.i:39: Warning:
- no \from part
- for clause 'assigns Tpost[\at(\old(i),Post)], Tpost[\at(k,Post)];'
+[eva:assigns:missing] assigns.i:39: Warning:
+ no \from part for clause
+ 'assigns Tpost[\at(\old(i),Post)], Tpost[\at(k,Post)];'.
+ Assuming \from \nothing so that the analysis can continue, but be aware this is probably incorrect.
[eva] assigns.i:56: Warning:
cannot interpret \from clause \at(x,Post)
(no environment to evaluate \at(_,Post)); effects will be ignored
@@ -99,13 +100,15 @@
[eva] computing for function ff1 <- main2 <- main.
Called from assigns.i:76.
[eva] using specification for function ff1
-[eva] assigns.i:60: Warning:
+[eva:assigns:missing-result] assigns.i:60: Warning:
no 'assigns \result \from ...' clause specified for function ff1
[eva] Done for function ff1
[eva] computing for function ff3 <- main2 <- main.
Called from assigns.i:78.
[eva] using specification for function ff3
-[eva] assigns.i:68: Warning: no \from part for clause 'assigns y1, y3;'
+[eva:assigns:missing] assigns.i:68: Warning:
+ no \from part for clause 'assigns y1, y3;'.
+ Assuming \from \nothing so that the analysis can continue, but be aware this is probably incorrect.
[eva] Done for function ff3
[kernel:annot:missing-spec] assigns.i:79: Warning:
Neither code nor specification for function ff4,
@@ -131,7 +134,7 @@
[eva] computing for function ff2_bis <- main2 <- main.
Called from assigns.i:83.
[eva] using specification for function ff2_bis
-[eva] assigns.i:64: Warning:
+[eva:assigns:missing-result] assigns.i:64: Warning:
no 'assigns \result \from ...' clause specified for function ff2_bis
[eva] Done for function ff2_bis
[eva:alarm] assigns.i:84: Warning:
diff --git a/tests/value/oracle/cast_fun.res.oracle b/tests/value/oracle/cast_fun.res.oracle
index c9083de743142ba756293ace6ed9478267b3ca3d..a0f86efd2c32fa461579b0ffbb0377df3a5a4d92 100644
--- a/tests/value/oracle/cast_fun.res.oracle
+++ b/tests/value/oracle/cast_fun.res.oracle
@@ -41,7 +41,7 @@
[eva] computing for function f1 <- main.
Called from cast_fun.i:60.
[eva] using specification for function f1
-[eva] cast_fun.i:6: Warning:
+[eva:assigns:missing-result] cast_fun.i:6: Warning:
no 'assigns \result \from ...' clause specified for function f1
[eva] Done for function f1
[eva:alarm] cast_fun.i:65: Warning:
@@ -49,13 +49,13 @@
[eva] computing for function f2 <- main.
Called from cast_fun.i:65.
[eva] using specification for function f2
-[eva] cast_fun.i:8: Warning:
+[eva:assigns:missing-result] cast_fun.i:8: Warning:
no 'assigns \result \from ...' clause specified for function f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
Called from cast_fun.i:70.
[eva] using specification for function f3
-[eva] cast_fun.i:10: Warning:
+[eva:assigns:missing-result] cast_fun.i:10: Warning:
no 'assigns \result \from ...' clause specified for function f3
[eva] Done for function f3
[eva] computing for function f3 <- main.
diff --git a/tests/value/oracle/leaf_spec.0.res.oracle b/tests/value/oracle/leaf_spec.0.res.oracle
index 9d1932aa482eece15fb1af19cb6a2e1c98beb281..fb936dc43f79dc32a4176877aa639cc7e00d0030 100644
--- a/tests/value/oracle/leaf_spec.0.res.oracle
+++ b/tests/value/oracle/leaf_spec.0.res.oracle
@@ -31,7 +31,7 @@
[eva] computing for function k <- main.
Called from leaf_spec.i:22.
[eva] using specification for function k
-[eva:invalid-assigns] leaf_spec.i:22:
+[eva:assigns:invalid-location] leaf_spec.i:22:
Completely invalid destination for assigns clause *l. Ignoring.
[eva] Done for function k
[kernel:annot:missing-spec] leaf_spec.i:22: Warning:
diff --git a/tests/value/oracle/leaf_spec.1.res.oracle b/tests/value/oracle/leaf_spec.1.res.oracle
index f47d633f23ac1ee42e1fc1f98b1918dfbd95d7a4..dd179ff3717724142d56e235564c04902c95e4f7 100644
--- a/tests/value/oracle/leaf_spec.1.res.oracle
+++ b/tests/value/oracle/leaf_spec.1.res.oracle
@@ -10,9 +10,9 @@
[eva] computing for function f <- main1.
Called from leaf_spec.i:27.
[eva] using specification for function f
-[eva:invalid-assigns] leaf_spec.i:27:
+[eva:assigns:invalid-location] leaf_spec.i:27:
Completely invalid destination for assigns clause *x. Ignoring.
-[eva:invalid-assigns] leaf_spec.i:27:
+[eva:assigns:invalid-location] leaf_spec.i:27:
Completely invalid destination for assigns clause *y. Ignoring.
[eva] Done for function f
[eva] Recording results for main1
diff --git a/tests/value/oracle/library_precond.res.oracle b/tests/value/oracle/library_precond.res.oracle
index c9a910c9cee742592dcdf5467549c12a765f13d8..0824f2e6161a54549f46aafa9374d95f638fa552 100644
--- a/tests/value/oracle/library_precond.res.oracle
+++ b/tests/value/oracle/library_precond.res.oracle
@@ -7,7 +7,7 @@
[eva] computing for function mxml <- main.
Called from library_precond.i:9.
[eva] using specification for function mxml
-[eva] library_precond.i:5: Warning:
+[eva:assigns:missing-result] library_precond.i:5: Warning:
no 'assigns \result \from ...' clause specified for function mxml
[eva:alarm] library_precond.i:9: Warning:
function mxml: precondition got status invalid.
diff --git a/tests/value/oracle/lock.res.oracle b/tests/value/oracle/lock.res.oracle
index 6bcf2c8b534d7de58ffeb476a98ce9ea537a95c5..ceba5a0de8cfe17dbe3ebb5dc87ca2be9a3de63f 100644
--- a/tests/value/oracle/lock.res.oracle
+++ b/tests/value/oracle/lock.res.oracle
@@ -4,23 +4,20 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
ghost_loctable[0..99] ∈ {0}
- pmutex ∈ {0}
-[eva:alarm] lock.i:48: Warning:
+ mutex ∈ [--..--]
+[eva:alarm] lock.i:49: Warning:
function locks0_good: precondition got status unknown.
[eva] computing for function acquire_lock <- locks0_good.
- Called from lock.i:51.
+ Called from lock.i:52.
[eva] using specification for function acquire_lock
-[eva:alarm] lock.i:51: Warning:
+[eva:alarm] lock.i:52: Warning:
function acquire_lock: precondition got status unknown.
-[eva] lock.i:21: Warning:
- no \from part for clause 'assigns ghost_loctable[0 .. 99];'
[eva] Done for function acquire_lock
[eva] computing for function release_lock <- locks0_good.
- Called from lock.i:52.
+ Called from lock.i:53.
[eva] using specification for function release_lock
-[eva:alarm] lock.i:52: Warning:
+[eva:alarm] lock.i:53: Warning:
function release_lock: precondition got status unknown.
-[eva] lock.i:29: Warning: no \from part for clause 'assigns ghost_loctable[..];'
[eva] Done for function release_lock
[eva] Recording results for locks0_good
[eva] Done for function locks0_good
@@ -36,13 +33,13 @@
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function acquire_lock:
- ghost_loctable[0..99] FROM ANYTHING(origin:Unknown) (and SELF)
+ ghost_loctable[0..99] FROM mutex
[from] Function release_lock:
- ghost_loctable[0..99] FROM ANYTHING(origin:Unknown) (and SELF)
+ ghost_loctable[0..99] FROM mutex
[from] Function locks0_good:
- ghost_loctable[0..99] FROM ANYTHING(origin:Unknown) (and SELF)
+ ghost_loctable[0..99] FROM mutex
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function locks0_good:
ghost_loctable[0..99]
[inout] Inputs for function locks0_good:
- ANYTHING(origin:Unknown)
+ mutex
diff --git a/tests/value/oracle/recursion.2.res.oracle b/tests/value/oracle/recursion.2.res.oracle
index 770f9b3691b3f3e85e52c8678dfb04418388daf6..7c23fb2f46bdc345a531f6c51dd40c56e694ed4a 100644
--- a/tests/value/oracle/recursion.2.res.oracle
+++ b/tests/value/oracle/recursion.2.res.oracle
@@ -7,11 +7,10 @@
[eva] recursion.c:433: Frama_C_show_each_10: {10}
[eva] recursion.c:438: Frama_C_show_each_36: {36}
[eva] using specification for function Frama_C_interval
-[eva] recursion.c:426: User Error:
+[eva:assigns:missing] recursion.c:426: Warning:
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.
+ 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.
[eva] using specification for function sum_nospec
[eva] recursion.c:442: Frama_C_show_each_unreachable: [-2147483648..2147483647]
[eva] ====== VALUES COMPUTED ======
@@ -51,5 +50,5 @@
Frama_C_entropy_source; x; y; tmp; tmp_0; tmp_1
[inout] Inputs for function main_fail:
Frama_C_entropy_source
-[eva] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[eva] Warning: warning assigns:missing treated as deferred error. See above messages for more information.
[kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/oracle/strings.res.oracle b/tests/value/oracle/strings.res.oracle
index e07c92d0d5dcf8d5efe1fc2b5ae5b8d42e44b112..1305ac1781b2ce7a2729dd397e415aa3c74bf9c9 100644
--- a/tests/value/oracle/strings.res.oracle
+++ b/tests/value/oracle/strings.res.oracle
@@ -165,8 +165,6 @@
[eva] computing for function assigns <- long_chain <- main.
Called from strings.i:135.
[eva] using specification for function assigns
-[eva] strings.i:129: Warning:
- no \from part for clause 'assigns *(p + (0 .. s - 1));'
[eva] Done for function assigns
[eva] computing for function strcmp <- long_chain <- main.
Called from strings.i:136.
@@ -323,11 +321,11 @@
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function assigns:
- tc[0..29] FROM ANYTHING(origin:Unknown) (and SELF)
+ tc[0..29] FROM nondet
[from] Function strcmp:
\result FROM s1_0; s2_0; tc[0..29]; long_chain_0[0..30]
[from] Function long_chain:
- \result FROM ANYTHING(origin:Unknown)
+ \result FROM nondet
[from] Function strcpy:
NON TERMINATING - NO EFFECTS
[from] Function string_writes:
@@ -385,7 +383,7 @@
[inout] Out (internal) for function long_chain:
tc[0..29]; long_chain_0[0..31]; x
[inout] Inputs for function long_chain:
- ANYTHING(origin:Unknown)
+ nondet
[inout] Out (internal) for function strcpy:
src; ldst; b[0..4]; tmp_unfold_46; tmp_1_unfold_46; tmp_0_unfold_46;
tmp_unfold_49; tmp_1_unfold_49; tmp_0_unfold_49; tmp_unfold_52;
@@ -421,4 +419,5 @@
[inout] Out (internal) for function main:
s1{[3]; [6]}; s5; s6; cc; Q; R; S; T; U; V; W; X; Y; Z
[inout] Inputs for function main:
- ANYTHING(origin:Unknown)
+ nondet; s1[0..5]; s3; s4; s5; s6; s7; s8; cc; "tutu"[bits 0 to 7];
+ "toto"[bits 0 to 7]
diff --git a/tests/value/oracle/use_spec.0.res.oracle b/tests/value/oracle/use_spec.0.res.oracle
index 860675533da474100fdec794e7fa88d4b497a4d1..942c944e4ecaa136ff3b103a4c2a9a2fa22292fb 100644
--- a/tests/value/oracle/use_spec.0.res.oracle
+++ b/tests/value/oracle/use_spec.0.res.oracle
@@ -1,7 +1,6 @@
[kernel] Parsing use_spec.i (no preprocessing)
-[eva] User Error: no assigns specified for function 'f', for which a builtin
- or the specification will be used. Potential unsoundness.
-[eva] Warning: Generating potentially incorrect assigns for function 'f' for which option -eva-use-spec is set
+[eva:assigns:missing] Warning:
+ No assigns specified for function 'f' for which option -eva-use-spec is set. Generating potentially incorrect assigns.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -75,5 +74,5 @@
x; y
Sure outputs:
w; z
-[eva] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[eva] Warning: warning assigns:missing treated as deferred error. See above messages for more information.
[kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/oracle/use_spec.1.res.oracle b/tests/value/oracle/use_spec.1.res.oracle
index 88fa49960f6ea16fb0c275670748ff79cfa95df0..ceeb03a639742555ef684cd431159b8abe3c0bc6 100644
--- a/tests/value/oracle/use_spec.1.res.oracle
+++ b/tests/value/oracle/use_spec.1.res.oracle
@@ -1,7 +1,6 @@
[kernel] Parsing use_spec.i (no preprocessing)
-[eva] User Error: no assigns specified for function 'f', for which a builtin
- or the specification will be used. Potential unsoundness.
-[eva] Warning: Generating potentially incorrect assigns for function 'f' for which option -eva-use-spec is set
+[eva:assigns:missing] Warning:
+ No assigns specified for function 'f' for which option -eva-use-spec is set. Generating potentially incorrect assigns.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -75,5 +74,5 @@
x; y
Sure outputs:
w; z
-[eva] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[eva] Warning: warning assigns:missing treated as deferred error. See above messages for more information.
[kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/value/strings.i b/tests/value/strings.i
index fbb7d4654212d35b89d08a8ad9aca758caa09ab0..a2960e19e15a64cf62ba2e9e9a82a3214a24574a 100644
--- a/tests/value/strings.i
+++ b/tests/value/strings.i
@@ -126,7 +126,7 @@ int strcmp(const char *s1, const char *s2)
return (*(unsigned char *)s1 - *(unsigned char *)--s2);
}
-//@ assigns p[0..s-1]; ensures \initialized(&p[0..s-1]);
+//@ assigns p[0..s-1] \from indirect:nondet; ensures \initialized(&p[0..s-1]);
void assigns(char *p, unsigned int s);
int long_chain() {