diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 7ba3de0d199c4f9439b87c9657f175d8ff83fc09..871cd1a2e967be8289afa2caf97acea54e2632a8 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 e1ebdb444a629b48de1a4a035ca971c42e172067..00aa3166f88de075b0042ed0a7a5cccd34807ebd 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 a940ec4e07c8d120b964d51d2812f0735d358098..d26ea5986d7f6f4b7d8f01bb1f4ecbfb33efa5dd 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 a2d2aea1a03b92001e491fd95188438caf24580c..40514ec227f70926aff9e222e1eaf5bdb39acfe8 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 2caf779ac2d3dbe01b4529a7926554c84e3dbe36..1b33d5c77ca0a0d02adf9f26b470133fbadf95bc 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 a99ab86cdc08c47d71d001e648ac8e24a7e09805..e61a670f209c4cf6c44b84de7c7a819536a3c74b 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 134e25adc51b4d290a7da7ee64f68d721d0e6eb6..962ffefd985da63b792ea0802ec031e52edf24eb 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: