[Eva] change 'invalid assigns' clause warning to feedback

src/plugins/value/engine/transfer_specification.ml

@@ -138,6 +138,7 @@ let reduce_to_valid_location out loc =
       begin
         if is_assigns out && not (Locations.is_bottom_loc loc) then
           Value_parameters.warning ~current:true ~once:true
+            ~wkey:Value_parameters.wkey_invalid_assigns
             "@[Completely invalid destination@ for %a.@ \
              Ignoring.@]" pp_assign_free_alloc out;
         None

src/plugins/value/value_parameters.ml

@@ -98,6 +98,8 @@ let () = set_warn_status wkey_missing_loop_unroll Log.Winactive
 let wkey_missing_loop_unroll_for = register_warn_category "missing-loop-unroll: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 () = set_warn_status wkey_invalid_assigns Log.Wfeedback
 
 module ForceValues =
   WithOutput

src/plugins/value/value_parameters.mli

@@ -204,6 +204,9 @@ val wkey_missing_loop_unroll_for : warn_category
 (** Warning category for signed overflows *)
 val wkey_signed_overflow : warn_category
 
+(** Warning category for 'completely invalid' assigns clause *)
+val wkey_invalid_assigns : warn_category
+
 (** Debug category used to print information about invalid pointer comparisons*)
 val dkey_pointer_comparison: category
 

tests/builtins/oracle/imprecise.res.oracle

@@ -39,7 +39,7 @@
 [eva] computing for function f <- invalid_assigns_imprecise <- main.
   Called from tests/builtins/imprecise.c:11.
 [eva] using specification for function f
-[eva] tests/builtins/imprecise.c:11: Warning: 
+[eva:invalid-assigns] tests/builtins/imprecise.c:11: 
   Completely invalid destination for assigns clause *p. Ignoring.
 [eva] Done for function f
 [eva] Recording results for invalid_assigns_imprecise

tests/libc/oracle/libgen_h.res.oracle

@@ -15,7 +15,7 @@
   Called from tests/libc/libgen_h.c:11.
 [eva] tests/libc/libgen_h.c:11: 
   function basename: precondition 'null_or_valid_string_path' got status valid.
-[eva] tests/libc/libgen_h.c:11: Warning: 
+[eva:invalid-assigns] tests/libc/libgen_h.c:11: 
   Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
 [eva] Done for function basename
 [eva:alarm] tests/libc/libgen_h.c:12: Warning: assertion got status unknown.
@@ -30,7 +30,7 @@
   Called from tests/libc/libgen_h.c:16.
 [eva] tests/libc/libgen_h.c:16: 
   function dirname: precondition 'null_or_valid_string_path' got status valid.
-[eva] tests/libc/libgen_h.c:16: Warning: 
+[eva:invalid-assigns] tests/libc/libgen_h.c:16: 
   Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
 [eva] Done for function dirname
 [eva:alarm] tests/libc/libgen_h.c:17: Warning: assertion got status unknown.

tests/libc/oracle/string_h.res.oracle

@@ -134,7 +134,7 @@
   function strtok: precondition 'valid_string_delim' got status valid.
 [eva] tests/libc/string_h.c:72: 
   function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status valid.
-[eva] tests/libc/string_h.c:72: Warning: 
+[eva:invalid-assigns] tests/libc/string_h.c:72: 
   Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
 [eva] Done for function strtok
 [eva:alarm] tests/libc/string_h.c:73: Warning: assertion got status unknown.
@@ -144,7 +144,7 @@
   function strtok: precondition 'valid_string_delim' got status valid.
 [eva:alarm] tests/libc/string_h.c:75: Warning: 
   function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva] tests/libc/string_h.c:75: Warning: 
+[eva:invalid-assigns] tests/libc/string_h.c:75: 
   Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
 [eva] Done for function strtok
 [eva:alarm] tests/libc/string_h.c:76: Warning: 
@@ -221,7 +221,7 @@
   function strtok_r: precondition 'valid_saveptr' got status valid.
 [eva] tests/libc/string_h.c:102: 
   function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status valid.
-[eva] tests/libc/string_h.c:102: Warning: 
+[eva:invalid-assigns] tests/libc/string_h.c:102: 
   Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
 [eva] Done for function strtok_r
 [eva:alarm] tests/libc/string_h.c:103: Warning: assertion got status unknown.
@@ -233,7 +233,7 @@
   function strtok_r: precondition 'valid_saveptr' got status valid.
 [eva:alarm] tests/libc/string_h.c:105: Warning: 
   function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva] tests/libc/string_h.c:105: Warning: 
+[eva:invalid-assigns] tests/libc/string_h.c:105: 
   Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
 [eva] Done for function strtok_r
 [eva:alarm] tests/libc/string_h.c:106: Warning: 

tests/value/oracle/leaf_spec.0.res.oracle

@@ -27,7 +27,7 @@
 [kernel:annot:missing-spec] tests/value/leaf_spec.i:22: Warning: 
   Neither code nor specification for function k, generating default assigns from the prototype
 [eva] using specification for function k
-[eva] tests/value/leaf_spec.i:22: Warning: 
+[eva:invalid-assigns] tests/value/leaf_spec.i:22: 
   Completely invalid destination for assigns clause *l. Ignoring.
 [eva] Done for function k
 [eva] computing for function k0 <- main.

tests/value/oracle/leaf_spec.1.res.oracle

@@ -9,9 +9,9 @@
 [kernel:annot:missing-spec] tests/value/leaf_spec.i:27: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
-[eva] tests/value/leaf_spec.i:27: Warning: 
+[eva:invalid-assigns] tests/value/leaf_spec.i:27: 
   Completely invalid destination for assigns clause *x. Ignoring.
-[eva] tests/value/leaf_spec.i:27: Warning: 
+[eva:invalid-assigns] tests/value/leaf_spec.i:27: 
   Completely invalid destination for assigns clause *y. Ignoring.
 [eva] Done for function f
 [eva] Recording results for main1