From 8086aa170ef96e8406deb5f9dcecd5d0d2d3c492 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 13 Jul 2022 13:24:43 +0200
Subject: [PATCH] [Eva] minimize warnings when using watchpoints
---
share/libc/__fc_builtin.h | 6 ++
.../aorai/tests/ya/oracle/serial.res.oracle | 6 ++
.../tests/ya/oracle_prove/serial.res.oracle | 2 +-
.../eva/domains/cvalue/builtins_watchpoint.ml | 4 +-
src/plugins/eva/self.ml | 2 +
src/plugins/eva/self.mli | 1 +
.../tests/sarif/oracle/std_string.sarif | 100 ++++++++++++++++++
tests/builtins/oracle/watch.res.oracle | 14 +--
tests/builtins/watch.c | 2 +-
tests/libc/oracle/fc_libc.1.res.oracle | 6 ++
tests/misc/oracle/audit-out.json | 2 +-
11 files changed, 131 insertions(+), 14 deletions(-)
diff --git a/share/libc/__fc_builtin.h b/share/libc/__fc_builtin.h
index ee871970008..fa8e9c3a759 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 e97503c8dd4..fc0a491dcf7 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 3ee9ca8546d..a171b4de92e 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 0098d74293f..08d4cdb4252 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 cf109376c8d..ac6812870f5 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 97b25ff3416..1616d4bc3f7 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 c29b3db8d73..226d230c654 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 d0a7fe337f5..02a90aa3b11 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 80551c78222..2508646370f 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 740ca94c2c5..8ce7b3829c6 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 a30dab60355..8d1c3de1c50 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"
]
}
},
--
GitLab