Merge branch 'fix/andre/watchpoint' into 'master'

[Eva] minimize warnings when using watchpoints

See merge request frama-c/frama-c!3877

share/libc/__fc_builtin.h

@@ -191,6 +191,12 @@ extern long long Frama_C_abstract_max(long long i);
 //@ assigns \result \from i;
 extern long long Frama_C_abstract_min(long long i);
 
+//@ assigns \nothing;
+extern void Frama_C_watch_value(void *p, size_t size, int i, int n);
+
+//@ assigns \nothing;
+extern void Frama_C_watch_cardinal(void *p, size_t size, int i, int n);
+
 __END_DECLS
 
 __POP_FC_STDLIB

src/plugins/aorai/tests/ya/oracle/serial.res.oracle

@@ -517,6 +517,12 @@ extern long long Frama_C_abstract_max(long long i);
     assigns \result \from i; */
 extern long long Frama_C_abstract_min(long long i);
 
+/*@ assigns \nothing; */
+extern void Frama_C_watch_value(void *p, size_t size, int i, int n);
+
+/*@ assigns \nothing; */
+extern void Frama_C_watch_cardinal(void *p, size_t size, int i, int n);
+
 int volatile indefinitely;
 int buffer[5];
 int n = 0;

src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle

 [kernel] Parsing serial.c (with preprocessing)
 [kernel] Parsing TMPDIR/aorai_serial_0_prove.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0_prove.i:1450: Warning: 
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0_prove.i:1456: Warning: 
   Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype

src/plugins/eva/domains/cvalue/builtins_watchpoint.ml

@@ -113,8 +113,8 @@ let watch_hook (stmt, _callstack, states) =
          in
          if watching
          then begin
-           Self.feedback ~once:true ~current:true
-             "Watchpoint: %a %a%t"
+           Self.warning ~wkey:Self.wkey_watchpoint ~once:true ~current:true
+             "%a %a%t"
              Printer.pp_exp name
              V.pretty vs
              Eva_utils.pp_callstack;

src/plugins/eva/self.ml

@@ -133,3 +133,5 @@ let () = set_warn_status wkey_invalid_assigns Log.Wfeedback
 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"
+let wkey_watchpoint = register_warn_category "watchpoint"
+let () = set_warn_status wkey_watchpoint Log.Wfeedback

src/plugins/eva/self.mli

@@ -78,3 +78,4 @@ val wkey_invalid_assigns : warn_category
 val wkey_experimental : warn_category
 val wkey_unknown_size : warn_category
 val wkey_ensures_false : warn_category
+val wkey_watchpoint : warn_category

src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif

@@ -4387,6 +4387,106 @@
             }
           ]
         },
+        {
+          "ruleId": "user-spec",
+          "kind": "pass",
+          "level": "none",
+          "message": {
+            "text": "behavior default! in function Frama_C_watch_cardinal."
+          },
+          "locations": [
+            {
+              "physicalLocation": {
+                "artifactLocation": {
+                  "uri": "libc/__fc_builtin.h",
+                  "uriBaseId": "FRAMAC_SHARE"
+                },
+                "region": {
+                  "startLine": 198,
+                  "startColumn": 12,
+                  "endLine": 198,
+                  "endColumn": 34,
+                  "byteLength": 22
+                }
+              }
+            }
+          ]
+        },
+        {
+          "ruleId": "user-spec",
+          "kind": "pass",
+          "level": "none",
+          "message": {
+            "text": "assigns clause in function Frama_C_watch_cardinal."
+          },
+          "locations": [
+            {
+              "physicalLocation": {
+                "artifactLocation": {
+                  "uri": "libc/__fc_builtin.h",
+                  "uriBaseId": "FRAMAC_SHARE"
+                },
+                "region": {
+                  "startLine": 198,
+                  "startColumn": 12,
+                  "endLine": 198,
+                  "endColumn": 34,
+                  "byteLength": 22
+                }
+              }
+            }
+          ]
+        },
+        {
+          "ruleId": "user-spec",
+          "kind": "pass",
+          "level": "none",
+          "message": {
+            "text": "behavior default! in function Frama_C_watch_value."
+          },
+          "locations": [
+            {
+              "physicalLocation": {
+                "artifactLocation": {
+                  "uri": "libc/__fc_builtin.h",
+                  "uriBaseId": "FRAMAC_SHARE"
+                },
+                "region": {
+                  "startLine": 195,
+                  "startColumn": 12,
+                  "endLine": 195,
+                  "endColumn": 31,
+                  "byteLength": 19
+                }
+              }
+            }
+          ]
+        },
+        {
+          "ruleId": "user-spec",
+          "kind": "pass",
+          "level": "none",
+          "message": {
+            "text": "assigns clause in function Frama_C_watch_value."
+          },
+          "locations": [
+            {
+              "physicalLocation": {
+                "artifactLocation": {
+                  "uri": "libc/__fc_builtin.h",
+                  "uriBaseId": "FRAMAC_SHARE"
+                },
+                "region": {
+                  "startLine": 195,
+                  "startColumn": 12,
+                  "endLine": 195,
+                  "endColumn": 31,
+                  "byteLength": 19
+                }
+              }
+            }
+          ]
+        },
         {
           "ruleId": "user-spec",
           "kind": "pass",

tests/builtins/oracle/watch.res.oracle

 [kernel] Parsing watch.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] watch.c:10: Warning: 
-  Calling undeclared function Frama_C_watch_value. Old style K&R code?
 [kernel:typing:implicit-function-declaration] watch.c:16: Warning: 
   Calling undeclared function u. Old style K&R code?
-[kernel:annot:missing-spec] watch.c:8: Warning: 
-  Neither code nor specification for function Frama_C_watch_value, generating default assigns from the prototype
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -13,16 +9,16 @@
   y ∈ {0}
   z ∈ {0}
 [eva] watch.c:10: Call to builtin Frama_C_watch_value
-[eva] watch.c:13: Watchpoint: & c [--..--]
-[eva] watch.c:14: Watchpoint: & c [--..--]
+[eva:watchpoint] watch.c:13: (void *)(& c) [--..--]
+[eva:watchpoint] watch.c:14: (void *)(& c) [--..--]
 [kernel:annot:missing-spec] watch.c:16: Warning: 
   Neither code nor specification for function u, generating default assigns from the prototype
 [eva] computing for function u <- main.
   Called from watch.c:16.
 [eva] using specification for function u
 [eva] Done for function u
-[eva] watch.c:17: Watchpoint: & c [--..--]
-[eva] watch.c:18: Watchpoint: & c [--..--]
-[eva] watch.c:19: Watchpoint: & c [--..--]
+[eva:watchpoint] watch.c:17: (void *)(& c) [--..--]
+[eva:watchpoint] watch.c:18: (void *)(& c) [--..--]
+[eva:watchpoint] watch.c:19: (void *)(& c) [--..--]
 [eva] User Error: Watchpoint builtin: countdown to zero
 [kernel] Plug-in eva aborted: invalid user input.

tests/builtins/watch.c

@@ -2,7 +2,7 @@
  EXIT: 1
    STDOPT:
 */
-
+#include "__fc_builtin.h"
 int x,y,z;
 
 int main(int c){

tests/libc/oracle/fc_libc.1.res.oracle

@@ -512,6 +512,12 @@ extern long long Frama_C_abstract_max(long long i);
     assigns \result \from i; */
 extern long long Frama_C_abstract_min(long long i);
 
+/*@ assigns \nothing; */
+extern void Frama_C_watch_value(void *p, size_t size, int i, int n);
+
+/*@ assigns \nothing; */
+extern void Frama_C_watch_cardinal(void *p, size_t size, int i, int n);
+
 unsigned int volatile __fc_unsigned_int_entropy;
 long volatile __fc_long_entropy;
 unsigned long volatile __fc_unsigned_long_entropy;

tests/misc/oracle/audit-out.json

@@ -45,7 +45,7 @@
       "disabled": [
         "garbled-mix", "invalid-assigns", "loop-unroll:auto",
         "loop-unroll:missing", "loop-unroll:missing:for",
-        "loop-unroll:partial", "malloc:weak"
+        "loop-unroll:partial", "malloc:weak", "watchpoint"
       ]
     }
   },