diff --git a/share/libc/__fc_builtin.h b/share/libc/__fc_builtin.h
index ee8719700085117fd7a56bbb58f7455bc0ddbdca..fa8e9c3a759d4c58282e4382453bcf44d4e641ab 100644
--- a/share/libc/__fc_builtin.h
+++ b/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
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index e97503c8dd4ef4f4851fb7dfccf59722b0dfb501..fc0a491dcf7bcadaa3893e54c598d9e997b3bc53 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/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;
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
index 3ee9ca8546d798ee44c5cbfa373696758859ae75..a171b4de92e5e8d97fb60209feb3f84a58c6fe4a 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,5 +1,5 @@
[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
diff --git a/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml b/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
index 0098d74293fd9354d2f6981b24fd7536c5a79fe9..08d4cdb425225371372801b64953cb31a54c6bdf 100644
--- a/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
+++ b/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;
diff --git a/src/plugins/eva/self.ml b/src/plugins/eva/self.ml
index cf109376c8d05157ea5bf5e21d2d9e153e99658e..ac6812870f5aa0d082d510152f469e0ba333e035 100644
--- a/src/plugins/eva/self.ml
+++ b/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
diff --git a/src/plugins/eva/self.mli b/src/plugins/eva/self.mli
index 97b25ff341643a3f700ffffb5f2fe9a0ab4a8ddb..1616d4bc3f7734b633f0a9f7bdc2e11974ed50fb 100644
--- a/src/plugins/eva/self.mli
+++ b/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
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index c29b3db8d73bf9099204e617f2593294fb004cb2..226d230c654e28da68998015f8a04d48db53ab90 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/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",
diff --git a/tests/builtins/oracle/watch.res.oracle b/tests/builtins/oracle/watch.res.oracle
index d0a7fe337f5359bd6bd41e7536d4d1c6d7489935..02a90aa3b1191882577a22f6aa273fdb59c43408 100644
--- a/tests/builtins/oracle/watch.res.oracle
+++ b/tests/builtins/oracle/watch.res.oracle
@@ -1,10 +1,6 @@
[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.
diff --git a/tests/builtins/watch.c b/tests/builtins/watch.c
index 80551c782227b4a090236e58b1af57092dc93739..2508646370f5e013419fac5076f5a89d9871c655 100644
--- a/tests/builtins/watch.c
+++ b/tests/builtins/watch.c
@@ -2,7 +2,7 @@
EXIT: 1
STDOPT:
*/
-
+#include "__fc_builtin.h"
int x,y,z;
int main(int c){
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 740ca94c2c576e8051f3a7454075ab85eb96ec5b..8ce7b3829c60d4afb7a416be103cf3f7f2894c5f 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/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;
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index a30dab6035590e9ad28c191c7141cfbb4dda5a71..8d1c3de1c501006d251af2aea1021d8751c5d3eb 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/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"
]
}
},