From d80e4a34bf58e1e86bc3cbf20d4a378e8f761f04 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 6 Oct 2021 09:10:28 +0200
Subject: [PATCH] [Eva] Emits indeterminate alarms on call arguments to
builtins.
'Indeterminate' alarms are alarms about uninitialized memory, escaping pointers
and special floating-point values (infinite and NaN).
These alarms are emitted for functions specified by -eva-warn-copy-indeterminate
option, which is @all by default. These alarms can be disabled for some function
by -eva-warn-copy-indeterminate=-f, in which case they are also disabled for
the argument expressions of calls to [f].
However:
- the @all default value did not include functions without definition
(for which a specification or a builtin is used).
- 'indeterminate' alarms were emitted anyway for the arguments of calls to
functions without definition, except for builtins.
So no indeterminate alarms were emitted for the argument expressions of calls
to builtins (unless their definitions were included).
This commit fixes this behavior:
the @all default of -eva-warn-copy-indeterminate option include all functions
and special case for functions without definition or builtins are removed.
It still avoids to emit surch alarms on Eva directives such as Frama_C_show_each.
---
src/plugins/value/engine/transfer_stmt.ml | 10 +++----
src/plugins/value/value_parameters.ml | 2 +-
tests/float/oracle/math_builtins.res.oracle | 26 ++++++++++++++++---
tests/libc/oracle/math_h.1.res.oracle | 12 ++++++---
tests/libc/oracle/math_h.2.res.oracle | 12 ++++++---
tests/value/initialized_copy.i | 4 +--
.../oracle/initialized_copy.1.res.oracle | 18 ++++++-------
7 files changed, 52 insertions(+), 32 deletions(-)
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 7ba3de0d199..871cd1a2e96 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -80,15 +80,11 @@ let do_copy_at = function
not (warn_indeterminate kf)
with Not_found -> assert false
-(* Warn for arguments that contain uninitialized/escaping if:
- - kf is a non-special leaf function (TODO: should we keep this?)
- - the user asked for this *)
+(* Warn for call arguments that contain uninitialized/escaping except on
+ [Frama_C_show_each] directives or if the user disables these alarms. *)
let is_determinate kf =
let name = Kernel_function.get_name kf in
- warn_indeterminate kf
- || not (Kernel_function.is_definition kf (* Should we keep this? *)
- || (name >= "Frama_C" && name < "Frama_D")
- || Builtins.is_builtin_overridden kf)
+ warn_indeterminate kf && not (Ast_info.is_frama_c_builtin name)
let subdivide_stmt = Value_util.get_subdivision
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index e1ebdb444a6..00aa3166f88 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -489,7 +489,7 @@ let () =
specification is used@ to interpret them.@]")
let () = Parameter_customize.set_group alarms
-
+let () = Parameter_customize.argument_may_be_fundecl ();
module WarnCopyIndeterminate =
Kernel_function_set
(struct
diff --git a/tests/float/oracle/math_builtins.res.oracle b/tests/float/oracle/math_builtins.res.oracle
index a940ec4e07c..d26ea5986d7 100644
--- a/tests/float/oracle/math_builtins.res.oracle
+++ b/tests/float/oracle/math_builtins.res.oracle
@@ -52,6 +52,8 @@
[eva] tests/float/math_builtins.c:33: Call to builtin acos
[eva] tests/float/math_builtins.c:33:
function acos: precondition 'in_domain' got status valid.
+[eva:alarm] tests/float/math_builtins.c:34: Warning:
+ non-finite double value. assert \is_finite(any_double);
[eva] tests/float/math_builtins.c:34: Call to builtin acos
[eva:alarm] tests/float/math_builtins.c:34: Warning:
function acos: precondition 'in_domain' got status unknown.
@@ -83,6 +85,8 @@
[eva] tests/float/math_builtins.c:50: Call to builtin acosf
[eva] tests/float/math_builtins.c:50:
function acosf: precondition 'in_domain' got status valid.
+[eva:alarm] tests/float/math_builtins.c:51: Warning:
+ non-finite float value. assert \is_finite(any_float);
[eva] tests/float/math_builtins.c:51: Call to builtin acosf
[eva:alarm] tests/float/math_builtins.c:51: Warning:
function acosf: precondition 'in_domain' got status unknown.
@@ -102,6 +106,8 @@
[eva] tests/float/math_builtins.c:61: Call to builtin asin
[eva] tests/float/math_builtins.c:61:
function asin: precondition 'in_domain' got status valid.
+[eva:alarm] tests/float/math_builtins.c:62: Warning:
+ non-finite double value. assert \is_finite(any_double);
[eva] tests/float/math_builtins.c:62: Call to builtin asin
[eva:alarm] tests/float/math_builtins.c:62: Warning:
function asin: precondition 'in_domain' got status unknown.
@@ -133,6 +139,8 @@
[eva] tests/float/math_builtins.c:78: Call to builtin asinf
[eva] tests/float/math_builtins.c:78:
function asinf: precondition 'in_domain' got status valid.
+[eva:alarm] tests/float/math_builtins.c:79: Warning:
+ non-finite float value. assert \is_finite(any_float);
[eva] tests/float/math_builtins.c:79: Call to builtin asinf
[eva:alarm] tests/float/math_builtins.c:79: Warning:
function asinf: precondition 'in_domain' got status unknown.
@@ -146,9 +154,11 @@
[eva] tests/float/math_builtins.c:87: Call to builtin atan
[eva] tests/float/math_builtins.c:87:
function atan: precondition 'number_arg' got status valid.
-[eva] tests/float/math_builtins.c:88: Call to builtin atan
[eva:alarm] tests/float/math_builtins.c:88: Warning:
- function atan: precondition 'number_arg' got status unknown.
+ non-finite double value. assert \is_finite(any_double);
+[eva] tests/float/math_builtins.c:88: Call to builtin atan
+[eva] tests/float/math_builtins.c:88:
+ function atan: precondition 'number_arg' got status valid.
[eva] tests/float/math_builtins.c:89: Call to builtin atan
[eva] tests/float/math_builtins.c:89:
function atan: precondition 'number_arg' got status valid.
@@ -165,9 +175,11 @@
[eva] tests/float/math_builtins.c:94: Call to builtin atanf
[eva] tests/float/math_builtins.c:94:
function atanf: precondition 'number_arg' got status valid.
-[eva] tests/float/math_builtins.c:95: Call to builtin atanf
[eva:alarm] tests/float/math_builtins.c:95: Warning:
- function atanf: precondition 'number_arg' got status unknown.
+ non-finite float value. assert \is_finite(any_float);
+[eva] tests/float/math_builtins.c:95: Call to builtin atanf
+[eva] tests/float/math_builtins.c:95:
+ function atanf: precondition 'number_arg' got status valid.
[eva] Recording results for test_atan
[eva] Done for function test_atan
[eva] computing for function test_atan2_det <- main.
@@ -3030,6 +3042,7 @@ void test_acos(void)
double half_pi = acos(0.);
double pi = acos(- 1.);
double zero = acos(1.);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(any_double); */
double acos_image = acos(any_double);
if (nondet) {
double bottom = acos(- 1.5);
@@ -3046,6 +3059,7 @@ void test_acos(void)
float f32__half_pi = acosf(0.f);
float f32__pi = acosf(- 1.f);
float f32__zero = acosf(1.f);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(any_float); */
float f32__acosf_image = acosf(any_float);
if (nondet) {
float bottom_1 = acosf(2.f);
@@ -3059,6 +3073,7 @@ void test_asin(void)
double zero = asin(0.);
double minus_half_pi = asin(- 1.);
double half_pi = asin(1.);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(any_double); */
double asin_image = asin(any_double);
if (nondet) {
double bottom = asin(- 1.5);
@@ -3075,6 +3090,7 @@ void test_asin(void)
float f32__zero = asinf(0.f);
float f32__minus_half_pi = asinf(- 1.f);
float f32__half_pi = asinf(1.f);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(any_float); */
float f32__asinf_image = asinf(any_float);
if (nondet) {
float bottom_1 = asinf(2.f);
@@ -3086,12 +3102,14 @@ void test_asin(void)
void test_atan(void)
{
double zero = atan(0.);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(any_double); */
double atan_image = atan(any_double);
double d64__x = atan(- 2.);
double d64__y = atan(2.);
double d64__xy = double_interval(- 2.,2.);
d64__xy = atan(d64__xy);
float f32__zero = atanf(0.f);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(any_float); */
float f32__atanf_image = atanf(any_float);
return;
}
diff --git a/tests/libc/oracle/math_h.1.res.oracle b/tests/libc/oracle/math_h.1.res.oracle
index a2d2aea1a03..40514ec227f 100644
--- a/tests/libc/oracle/math_h.1.res.oracle
+++ b/tests/libc/oracle/math_h.1.res.oracle
@@ -58,9 +58,11 @@
[eva] tests/libc/math_h.c:86: Call to builtin atan
[eva] tests/libc/math_h.c:86:
function atan: precondition 'number_arg' got status valid.
-[eva] tests/libc/math_h.c:86: Call to builtin atan
[eva:alarm] tests/libc/math_h.c:86: Warning:
- function atan: precondition 'number_arg' got status unknown.
+ NaN double value. assert ¬\is_NaN(top);
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
[eva] tests/libc/math_h.c:86: Call to builtin atanf
[eva] tests/libc/math_h.c:86:
function atanf: precondition 'number_arg' got status valid.
@@ -85,9 +87,11 @@
[eva] tests/libc/math_h.c:86: Call to builtin atanf
[eva] tests/libc/math_h.c:86:
function atanf: precondition 'number_arg' got status valid.
-[eva] tests/libc/math_h.c:86: Call to builtin atanf
[eva:alarm] tests/libc/math_h.c:86: Warning:
- function atanf: precondition 'number_arg' got status unknown.
+ NaN float value. assert ¬\is_NaN(f_top);
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:86.
[eva] using specification for function atanl
diff --git a/tests/libc/oracle/math_h.2.res.oracle b/tests/libc/oracle/math_h.2.res.oracle
index 2caf779ac2d..1b33d5c77ca 100644
--- a/tests/libc/oracle/math_h.2.res.oracle
+++ b/tests/libc/oracle/math_h.2.res.oracle
@@ -51,9 +51,11 @@
[eva] tests/libc/math_h.c:86: Call to builtin atan
[eva] tests/libc/math_h.c:86:
function atan: precondition 'number_arg' got status valid.
-[eva] tests/libc/math_h.c:86: Call to builtin atan
[eva:alarm] tests/libc/math_h.c:86: Warning:
- function atan: precondition 'number_arg' got status unknown.
+ non-finite double value. assert \is_finite(top);
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
[eva] tests/libc/math_h.c:86: Call to builtin atanf
[eva] tests/libc/math_h.c:86:
function atanf: precondition 'number_arg' got status valid.
@@ -78,9 +80,11 @@
[eva] tests/libc/math_h.c:86: Call to builtin atanf
[eva] tests/libc/math_h.c:86:
function atanf: precondition 'number_arg' got status valid.
-[eva] tests/libc/math_h.c:86: Call to builtin atanf
[eva:alarm] tests/libc/math_h.c:86: Warning:
- function atanf: precondition 'number_arg' got status unknown.
+ non-finite float value. assert \is_finite(f_top);
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:86.
[eva] using specification for function atanl
diff --git a/tests/value/initialized_copy.i b/tests/value/initialized_copy.i
index a99ab86cdc0..e61a670f209 100644
--- a/tests/value/initialized_copy.i
+++ b/tests/value/initialized_copy.i
@@ -132,7 +132,7 @@ int main() {
if (v) {
int a;
- g(a); // completely indeterminate. We also warn when the option is not active, as g has no body
+ g(a); // completely indeterminate.
Frama_C_show_each_unreached();
}
@@ -148,7 +148,7 @@ int main() {
int a;
if (v)
a = 1;
- g(a); // possibly determinate. We also warn when the option is not active, as g has no body
+ g(a); // possibly determinate.
Frama_C_dump_each();
}
diff --git a/tests/value/oracle/initialized_copy.1.res.oracle b/tests/value/oracle/initialized_copy.1.res.oracle
index 134e25adc51..962ffefd985 100644
--- a/tests/value/oracle/initialized_copy.1.res.oracle
+++ b/tests/value/oracle/initialized_copy.1.res.oracle
@@ -75,8 +75,13 @@
[eva] Recording results for f
[eva] Done for function f
[eva] tests/value/initialized_copy.i:130: Frama_C_show_each_unreached:
-[eva:alarm] tests/value/initialized_copy.i:135: Warning:
- accessing uninitialized left-value. assert \initialized(&a_6);
+[eva] computing for function g <- main.
+ Called from tests/value/initialized_copy.i:135.
+[kernel:annot:missing-spec] tests/value/initialized_copy.i:135: Warning:
+ Neither code nor specification for function g, generating default assigns from the prototype
+[eva] using specification for function g
+[eva] Done for function g
+[eva] tests/value/initialized_copy.i:136: Frama_C_show_each_unreached:
[eva] computing for function f <- main.
Called from tests/value/initialized_copy.i:143.
[eva] Recording results for f
@@ -89,26 +94,19 @@
a_7 ∈ {1} or UNINITIALIZED
__retres ∈ UNINITIALIZED
==END OF DUMP==
-[eva:alarm] tests/value/initialized_copy.i:151: Warning:
- accessing uninitialized left-value. assert \initialized(&a_8);
[eva] computing for function g <- main.
Called from tests/value/initialized_copy.i:151.
-[kernel:annot:missing-spec] tests/value/initialized_copy.i:151: Warning:
- Neither code nor specification for function g, generating default assigns from the prototype
-[eva] using specification for function g
[eva] Done for function g
[eva] tests/value/initialized_copy.i:152:
Frama_C_dump_each:
# cvalue:
w[0..9] ∈ {0; 12} or UNINITIALIZED
v ∈ [--..--]
- a_8 ∈ {1}
+ a_8 ∈ {1} or UNINITIALIZED
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] Recording results for main
[eva] done for function main
-[eva] tests/value/initialized_copy.i:135:
- assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
--
GitLab