diff --git a/Makefile b/Makefile
index 4290dd453852e363b88dd566e6c3818d727f290b..768fbbbee1cf4def300cb836047b1fe192c451e2 100644
--- a/Makefile
+++ b/Makefile
@@ -612,6 +612,7 @@ KERNEL_CMO=\
src/kernel_services/ast_transformations/filter.cmo \
src/kernel_services/ast_transformations/inline.cmo \
src/kernel_internals/runtime/dump_config.cmo \
+ src/kernel_services/ast_transformations/contract_special_float.cmo \
src/kernel_internals/runtime/special_hooks.cmo \
src/kernel_internals/runtime/messages.cmo
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 04a3971297756004bf40464bf6bf81e8f531e7ac..0a01c138627760c0a6a488dc48e6aec1281d5653 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -567,6 +567,8 @@ src/kernel_services/ast_queries/logic_typing.mli: CEA_INRIA_LGPL
src/kernel_services/ast_queries/logic_utils.ml: CEA_INRIA_LGPL
src/kernel_services/ast_queries/logic_utils.mli: CEA_INRIA_LGPL
src/kernel_services/ast_transformations/README.md: .ignore
+src/kernel_services/ast_transformations/contract_special_float.ml: CEA_LGPL
+src/kernel_services/ast_transformations/contract_special_float.mli: CEA_LGPL
src/kernel_services/ast_transformations/clone.ml: CEA_LGPL
src/kernel_services/ast_transformations/clone.mli: CEA_LGPL
src/kernel_services/ast_transformations/filter.ml: CEA_LGPL
diff --git a/share/libc/math.h b/share/libc/math.h
index f8b370fae2ef29472cc6a2f7aac0defa95979607..6924d5cab8983f2d1d60cfc9794e965e0e986a71 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -128,118 +128,342 @@ int __fc_fpclassify(double x);
(sizeof(x) == sizeof(float) ? __fc_fpclassifyf(x) == FP_NORMAL : __fc_fpclassify(x) == FP_NORMAL)
-/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes in_domain: \is_finite(x) && \abs(x) <= 1;
assigns \result \from x;
ensures positive_result: \is_finite(\result) && \result >= 0;
+ ensures no_error: errno == \old(errno);
+ behavior domain_error:
+ assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double acos(double x);
-/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes in_domain: \is_finite(x) && \abs(x) <= 1;
assigns \result \from x;
ensures positive_result: \is_finite(\result) && \result >= 0;
+ ensures no_error: errno == \old(errno);
+ behavior domain_error:
+ assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float acosf(float x);
-/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes in_domain: \is_finite(x) && \abs(x) <= 1;
assigns \result \from x;
ensures positive_result: \is_finite(\result) && \result >= 0;
+ ensures no_error: errno == \old(errno);
+ behavior domain_error:
+ assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double acosl(long double x);
-/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes in_domain: \is_finite(x) && \abs(x) <= 1;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior domain_error:
+ assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double asin(double x);
-/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes in_domain: \is_finite(x) && \abs(x) <= 1;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior domain_error:
+ assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float asinf(float x);
-/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes in_domain: \is_finite(x) && \abs(x) <= 1;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior domain_error:
+ assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double asinl(long double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior normal:
+ assumes finite_arg: !\is_NaN(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1.571 <= \result <= 1.571;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float atanf(float x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior normal:
+ assumes number_arg: !\is_NaN(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1.571 <= \result <= 1.571;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double atan(double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior normal:
+ assumes number_arg: !\is_NaN(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1.571 <= \result <= 1.571;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double atanl(long double x);
-/*@ requires finite_args: \is_finite(x) && \is_finite(y);
- requires finite_result: \is_finite(atan2(x, y));
- assigns \result \from x, y;
+/*@
+ assigns \result \from x, y;
+ behavior normal:
+ assumes number_args: !\is_NaN(x) && !\is_NaN(y);
ensures finite_result: \is_finite(\result);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x) || \is_NaN(y);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double atan2(double y, double x);
-/*@ requires finite_args: \is_finite(x) && \is_finite(y);
- requires finite_logic_result: \is_finite(atan2f(x, y));
- assigns \result \from x, y;
+/*@
+ assigns \result \from x, y;
+ behavior normal:
+ assumes number_args: !\is_NaN(x) && !\is_NaN(y);
ensures finite_result: \is_finite(\result);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x) || \is_NaN(y);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float atan2f(float y, float x);
+/*@
+ assigns \result \from x, y;
+ behavior normal:
+ assumes number_args: !\is_NaN(x) && !\is_NaN(y);
+ ensures finite_result: \is_finite(\result);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x) || \is_NaN(y);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
+*/
extern long double atan2l(long double y, long double x);
-/*@ requires finite_arg: \is_finite(x);
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. <= \result <= 1.;
+ ensures no_error: errno == \old(errno);
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: !\is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double cos(double x);
-/*@ requires finite_arg: \is_finite(x);
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. <= \result <= 1.;
+ ensures no_error: errno == \old(errno);
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: !\is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float cosf(float x);
-/*@ requires finite_arg: \is_finite(x);
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. <= \result <= 1.;
+ ensures no_error: errno == \old(errno);
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: !\is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double cosl(long double x);
-/*@ requires finite_arg: \is_finite(x);
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. <= \result <= 1.;
+ ensures no_error: errno == \old(errno);
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: !\is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double sin(double x);
-/*@ requires finite_arg: \is_finite(x);
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. <= \result <= 1.;
+ ensures no_error: errno == \old(errno);
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: !\is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float sinf(float x);
-/*@ requires finite_arg: \is_finite(x);
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. <= \result <= 1.;
+ ensures no_error: errno == \old(errno);
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: !\is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double sinl(long double x);
@@ -248,55 +472,79 @@ extern float tanf(float x);
extern long double tanl(long double x);
/*@
- assigns __fc_errno, \result \from x;
+ assigns errno, \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) && x >= 1;
assigns \result \from x;
ensures positive_result: \is_finite(\result) && \result >= 0;
+ ensures no_error: errno == \old(errno);
behavior infinite:
assumes is_plus_infinity: \is_plus_infinity(x);
assigns \result \from x;
ensures result_plus_infinity: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
behavior domain_error:
assumes out_of_domain: \is_minus_infinity(x) || (\is_finite(x) && x < 1);
- assigns __fc_errno, \result \from x;
- ensures errno_set: __fc_errno == 1;
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
disjoint behaviors;
*/
extern double acosh(double x);
/*@
- assigns __fc_errno, \result \from x;
+ assigns errno, \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) && x >= 1;
assigns \result \from x;
ensures positive_result: \is_finite(\result) && \result >= 0;
+ ensures no_error: errno == \old(errno);
behavior infinite:
assumes is_plus_infinity: \is_plus_infinity(x);
assigns \result \from x;
ensures result_plus_infinity: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
behavior domain_error:
assumes out_of_domain: \is_minus_infinity(x) || (\is_finite(x) && x < 1);
- assigns __fc_errno, \result \from x;
- ensures errno_set: __fc_errno == 1;
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
disjoint behaviors;
*/
extern float acoshf(float x);
/*@
- assigns __fc_errno, \result \from x;
+ assigns errno, \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) && x >= 1;
assigns \result \from x;
ensures positive_result: \is_finite(\result) && \result >= 0;
+ ensures no_error: errno == \old(errno);
behavior infinite:
assumes is_plus_infinity: \is_plus_infinity(x);
assigns \result \from x;
ensures result_plus_infinity: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
behavior domain_error:
assumes out_of_domain: \is_minus_infinity(x) || (\is_finite(x) && x < 1);
- assigns __fc_errno, \result \from x;
- ensures errno_set: __fc_errno == 1;
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
disjoint behaviors;
*/
extern long double acoshl(long double x);
@@ -321,19 +569,77 @@ extern double tanh(double x);
extern float tanhf(float x);
extern long double tanhl(long double x);
-/*@ requires finite_arg: \is_finite(x);
- requires finite_domain: x <= 0x1.62e42fefa39efp+9;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes domain_arg: x >= -0x1.74910d52d3051p9 && x <= 0x1.62e42fefa39efp+9;
assigns \result \from x;
ensures res_finite: \is_finite(\result);
ensures positive_result: \result > 0.;
+ ensures no_error: errno == \old(errno);
+ behavior overflow:
+ assumes overflow_arg: \is_finite(x) && x > 0x1.62e42fefa39efp+9;
+ ensures infinite_res: \is_plus_infinity(\result);
+ ensures errno_set: errno == ERANGE;
+ behavior plus_infinity:
+ assumes plus_infinity_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinity_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior underflow:
+ assumes underflow_arg: \is_finite(x) && x < -0x1.74910d52d3051p9;
+ ensures zero_res: \result == 0.;
+ ensures errno_set: errno == ERANGE;
+ behavior minus_infinity:
+ assumes plus_infinity_arg: \is_minus_infinity(x);
+ assigns \result \from x;
+ ensures zero_result: \is_finite(\result) && \result == 0.;
+ ensures no_error: errno == \old(errno);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double exp(double x);
-/*@ requires finite_arg: \is_finite(x);
- requires res_finite: x <= 0x1.62e42ep+6;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes domain_arg: x >= -0x1.9fe368p6 && x <= 0x1.62e42ep+6;
assigns \result \from x;
ensures res_finite: \is_finite(\result);
ensures positive_result: \result > 0.;
+ ensures no_error: errno == \old(errno);
+ behavior overflow:
+ assumes overflow_arg: \is_finite(x) && x > 0x1.62e42ep+6;
+ ensures infinite_res: \is_plus_infinity(\result);
+ ensures errno_set: errno == ERANGE;
+ behavior plus_infinity:
+ assumes plus_infinity_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinity_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior underflow:
+ assumes underflow_arg: \is_finite(x) && x < -0x1.9fe368p6;
+ ensures zero_res: \result == 0.;
+ ensures errno_set: errno == ERANGE;
+ behavior minus_infinity:
+ assumes plus_infinity_arg: \is_minus_infinity(x);
+ assigns \result \from x;
+ ensures zero_result: \is_finite(\result) && \result == 0.;
+ ensures no_error: errno == \old(errno);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float expf(float x);
@@ -359,45 +665,189 @@ extern double ldexp(double x, int exp);
extern float ldexpf(float x, int exp);
extern long double ldexpl(long double x, int exp);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_positive: x > 0;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x > 0;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures infinite_result: \is_minus_infinity(\result); // -HUGE_VAL
+ ensures errno_set: errno == ERANGE;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double log(double x);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_positive: x > 0;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x > 0;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures infinite_result: \is_minus_infinity(\result); // -HUGE_VALF
+ ensures errno_set: errno == ERANGE;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float logf(float x);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_pos: x > 0;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x > 0;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures infinite_result: \is_minus_infinity(\result); // -HUGE_VALL
+ ensures errno_set: errno == ERANGE;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double logl(long double x);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_positive: x > 0;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x > 0;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures infinite_result: \is_minus_infinity(\result); // -HUGE_VAL
+ ensures errno_set: errno == ERANGE;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double log10(double x);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_positive: x > 0;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x > 0;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures infinite_result: \is_minus_infinity(\result); // -HUGE_VALF
+ ensures errno_set: errno == ERANGE;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float log10f(float x);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_postive: x > 0;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x > 0;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures infinite_result: \is_minus_infinity(\result); // -HUGE_VALL
+ ensures errno_set: errno == ERANGE;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double log10l(long double x);
@@ -405,24 +855,96 @@ extern double log1p(double x);
extern float log1pf(float x);
extern long double log1pl(long double x);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_positive: x > 0;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x > 0;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures infinite_result: \is_minus_infinity(\result); // -HUGE_VAL
+ ensures errno_set: errno == ERANGE;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double log2(double x);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_positive: x > 0;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x > 0;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures infinite_result: \is_minus_infinity(\result); // -HUGE_VALF
+ ensures errno_set: errno == ERANGE;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float log2f(float x);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_positive: x > 0;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x > 0;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures infinite_result: \is_minus_infinity(\result); // -HUGE_VALL
+ ensures errno_set: errno == ERANGE;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double log2l(long double x);
@@ -446,27 +968,57 @@ extern double cbrt(double x);
extern float cbrtf(float x);
extern long double cbrtl(long double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
ensures res_finite: \is_finite(\result);
ensures positive_result: \result >= 0.;
ensures equal_magnitude_result: \result == x || \result == -x;
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_plus_infinity(\result);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double fabs(double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
ensures res_finite: \is_finite(\result);
ensures positive_result: \result >= 0.;
ensures equal_magnitude_result: \result == x || \result == -x;
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_plus_infinity(\result);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float fabsf(float x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
ensures res_finite: \is_finite(\result);
ensures positive_result: \result >= 0.;
ensures equal_magnitude_result: \result == x || \result == -x;
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_plus_infinity(\result);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double fabsl(long double x);
@@ -474,45 +1026,121 @@ extern double hypot(double x, double y);
extern float hypotf(float x, float y);
extern long double hypotl(long double x, long double y);
-/*@ requires finite_args: \is_finite(x) && \is_finite(y);
- requires finite_logic_res: \is_finite(pow(x, y));
- assigns \result \from x, y;
+/*@
+ assigns errno, \result \from x, y;
+ behavior normal:
+ assumes finite_logic_res: \is_finite(pow(x, y));
ensures finite_result: \is_finite(\result);
+ ensures errno: errno == ERANGE || errno == \old(errno);
+ behavior overflow:
+ assumes infinite_logic_res: !\is_finite(pow(x, y));
+ ensures infinite_result: !\is_finite(\result);
+ ensures errno: errno == ERANGE || errno == EDOM || errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double pow(double x, double y);
-/*@ requires finite_args: \is_finite(x) && \is_finite(y);
- requires finite_logic_res: \is_finite(powf(x, y));
- assigns \result \from x, y;
+/*@
+ assigns errno, \result \from x, y;
+ behavior normal:
+ assumes finite_logic_res: \is_finite(pow(x, y));
ensures finite_result: \is_finite(\result);
+ ensures errno: errno == ERANGE || errno == \old(errno);
+ behavior overflow:
+ assumes infinite_logic_res: !\is_finite(pow(x, y));
+ ensures infinite_result: !\is_finite(\result);
+ ensures errno: errno == ERANGE || errno == EDOM || errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float powf(float x, float y);
extern long double powl(long double x, long double y);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_positive: x >= -0.;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x >= -0.;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result >= -0.;
ensures result_value: \result == sqrt(x);
+ ensures no_error: errno == \old(errno);
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior infinity:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double sqrt(double x);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_positive: x >= -0.;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x >= -0.;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result >= -0.;
- ensures result_value: \result == sqrtf(x);
+ ensures result_value: \result == sqrt(x);
+ ensures no_error: errno == \old(errno);
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior infinity:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float sqrtf(float x);
-/*@ requires finite_arg: \is_finite(x);
- requires arg_positive: x >= -0.;
+/*@
+ assigns errno, \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_positive: x >= -0.;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result >= -0.;
+ ensures no_error: errno == \old(errno);
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < -0.);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior infinity:
+ assumes infinite_arg: \is_plus_infinity(x);
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ ensures no_error: errno == \old(errno);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double sqrtl(long double x);
@@ -532,40 +1160,105 @@ extern double tgamma(double x);
extern float tgammaf(float x);
extern long double tgammal(long double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double ceil(double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
-
extern float ceilf(float x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double ceill(long double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double floor(double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float floorf(float x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double floorl(long double x);
@@ -585,21 +1278,54 @@ extern long long int llrint(double x);
extern long long int llrintf(float x);
extern long long int llrintl(long double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double round(double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float roundf(float x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double roundl(long double x);
@@ -611,35 +1337,96 @@ extern long long int llround(double x);
extern long long int llroundf(float x);
extern long long int llroundl(long double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double trunc(double x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float truncf(float x);
-/*@ requires finite_arg: \is_finite(x);
- assigns \result \from x;
+/*@
+ assigns \result \from x;
+ behavior finite:
+ assumes finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures equal_result: \result == x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
*/
extern long double truncl(long double x);
-/*@ requires finite_args: \is_finite(x) && \is_finite(y);
- requires finite_logic_result: \is_finite(fmod(x, y));
+/*@
+ assigns errno, \result \from x, y;
+ behavior normal:
+ assumes in_domain: !\is_NaN(x) && !\is_NaN(y) && y != 0.;
assigns \result \from x, y;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior domain_error:
+ assumes out_of_domain: \is_infinite(x) || y == 0.;
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_args: \is_NaN(x) || \is_NaN(y);
+ assigns \result \from x, y;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern double fmod(double x, double y);
-/*@ requires finite_args: \is_finite(x) && \is_finite(y);
- requires finite_logic_result: \is_finite(fmodf(x, y));
+/*@
+ assigns errno, \result \from x, y;
+ behavior normal:
+ assumes in_domain: !\is_NaN(x) && !\is_NaN(y) && y != 0.;
assigns \result \from x, y;
ensures finite_result: \is_finite(\result);
+ ensures no_error: errno == \old(errno);
+ behavior domain_error:
+ assumes out_of_domain: \is_infinite(x) || y == 0.;
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_args: \is_NaN(x) || \is_NaN(y);
+ assigns \result \from x, y;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
*/
extern float fmodf(float x, float y);
diff --git a/src/kernel_services/ast_transformations/contract_special_float.ml b/src/kernel_services/ast_transformations/contract_special_float.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8eeaed7dcb14e11c4bc98304e1aeb04bf8933693
--- /dev/null
+++ b/src/kernel_services/ast_transformations/contract_special_float.ml
@@ -0,0 +1,138 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+let is_special_float_term term =
+ match term.term_node with
+ | TLval (TVar {lv_name = "\\plus_infinity"}, _)
+ | TLval (TVar {lv_name = "\\minus_infinity"}, _) ->
+ Kernel.SpecialFloat.get () = "non-finite"
+ | TLval (TVar {lv_name = "\\NaN"}, _) -> true
+ | _ -> false
+
+let rec is_special_float_pred pred =
+ match pred.pred_content with
+ | Pand (a, b) -> is_special_float_pred a || is_special_float_pred b
+ | Por (a, b) -> is_special_float_pred a && is_special_float_pred b
+ | Papp (logic_info, [], [_]) ->
+ begin
+ match logic_info.l_var_info.lv_name with
+ | "\\is_NaN" -> true
+ | "\\is_plus_infinity" | "\\is_minus_infinity" | "\\is_infinite" ->
+ Kernel.SpecialFloat.get () = "non-finite"
+ | _ -> false
+ end
+ | Pnot {pred_content = Papp
+ ({l_var_info = {lv_name = "\\is_finite"}}, [], [_])} ->
+ true
+ | Prel (Req, t1, t2) ->
+ (is_special_float_term t1) <> (is_special_float_term t2)
+ | _ -> false
+
+let ensures_special_float = function
+ | Normal, ip -> is_special_float_pred ip.ip_content.tp_statement
+ | _ -> false
+
+let are_complete_disjoint spec behaviors =
+ match spec.spec_complete_behaviors, spec.spec_disjoint_behaviors with
+ | [complete], [disjoint] ->
+ let mem bhv = List.(mem bhv.b_name complete && mem bhv.b_name disjoint) in
+ List.for_all mem behaviors
+ | _ -> false
+
+let find_behavior name spec =
+ let rec find acc = function
+ | [] -> None, spec.spec_behavior
+ | b :: tl -> if b.b_name = name then Some b, acc @ tl else find (b :: acc) tl
+ in
+ find [] spec.spec_behavior
+
+let update_spec spec =
+ let default, behaviors = find_behavior Cil.default_behavior_name spec in
+ let filter bhv = List.exists ensures_special_float bhv.b_post_cond in
+ let disabled, normal = List.partition filter behaviors in
+ if disabled <> [] then
+ match normal with
+ | [ bhv ] when are_complete_disjoint spec behaviors ->
+ let requires = bhv.b_requires @ bhv.b_assumes in
+ let default =
+ match default with
+ | None ->
+ bhv.b_name <- Cil.default_behavior_name;
+ bhv.b_requires <- requires;
+ bhv.b_assumes <- [];
+ bhv
+ | Some default ->
+ default.b_requires <- default.b_requires @ requires;
+ if bhv.b_assigns <> WritesAny
+ then default.b_assigns <- bhv.b_assigns;
+ if bhv.b_allocation <> FreeAllocAny
+ then default.b_allocation <- bhv.b_allocation;
+ default.b_post_cond <- default.b_post_cond @ bhv.b_post_cond;
+ default.b_extended <- default.b_extended @ bhv.b_extended;
+ default
+ in
+ spec.spec_behavior <- [default];
+ spec.spec_complete_behaviors <- [];
+ spec.spec_disjoint_behaviors <- [];
+ | _ ->
+ let requires =
+ List.map
+ (fun bhv ->
+ let neg_assumes =
+ List.map
+ (fun e -> (Logic_const.pnot (e.ip_content.tp_statement)))
+ (bhv.b_requires @ bhv.b_assumes)
+ in
+ Logic_const.(new_predicate (pors neg_assumes)))
+ disabled
+ in
+ let default =
+ match default with
+ | None -> Cil.mk_behavior ~requires ()
+ | Some default ->
+ default.b_requires <- default.b_requires @ requires;
+ default
+ in
+ spec.spec_behavior <- default :: normal;
+ let filter name = List.for_all (fun b -> b.b_name <> name) disabled in
+ let map_filter = List.map (List.filter filter) in
+ spec.spec_complete_behaviors <- map_filter spec.spec_complete_behaviors;
+ spec.spec_disjoint_behaviors <- map_filter spec.spec_disjoint_behaviors
+
+let visitor = object
+ inherit Cil.nopCilVisitor
+ method! vspec spec = update_spec spec; Cil.SkipChildren
+end
+
+let run ast =
+ if Kernel.SpecialFloat.get () <> "none" then
+ Cil.visitCilFileSameGlobals visitor ast
+
+let transform =
+ File.register_code_transformation_category "contract_special_float"
+
+let () =
+ File.add_code_transformation_before_cleanup
+ ~deps:[(module Kernel.SpecialFloat)]
+ transform run
diff --git a/src/kernel_services/ast_transformations/contract_special_float.mli b/src/kernel_services/ast_transformations/contract_special_float.mli
new file mode 100644
index 0000000000000000000000000000000000000000..cce51dc83ef23f10bb7ed95d5a93dfc632b91896
--- /dev/null
+++ b/src/kernel_services/ast_transformations/contract_special_float.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index 445f2843ae3c712b2b47065c1d72f36a0c2d9ec8..7b609dc39a328eb5284ad2ae82207be1a2b7ec44 100644
--- a/src/plugins/report/tests/report/oracle/csv.csv
+++ b/src/plugins/report/tests/report/oracle/csv.csv
@@ -1,5 +1,5 @@
directory file line function property kind status property
-FRAMAC_SHARE/libc math.h 478 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc math.h 1032 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
tests/report csv.c 11 main1 signed_overflow Unknown -2147483648 ≤ x * x
tests/report csv.c 11 main1 signed_overflow Unknown x * x ≤ 2147483647
tests/report csv.c 12 main1 index_bound Unknown 0 ≤ x
diff --git a/src/plugins/report/tests/report/oracle/csv.res.oracle b/src/plugins/report/tests/report/oracle/csv.res.oracle
index aaf1752f36f4d2a5614f9f35f6bd27d7e986d277..9d56ae932a09b6dedae6578ae8985c22c6dbb1e8 100644
--- a/src/plugins/report/tests/report/oracle/csv.res.oracle
+++ b/src/plugins/report/tests/report/oracle/csv.res.oracle
@@ -31,8 +31,6 @@
[eva] computing for function main3 <- main.
Called from tests/report/csv.c:56.
[eva] tests/report/csv.c:33: Call to builtin pow
-[eva] tests/report/csv.c:33:
- function pow: precondition 'finite_args' got status valid.
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
@@ -62,11 +60,12 @@
[eva:final-states] Values at end of function main4:
d ∈ [1. .. 1.79769313486e+308]
[eva:final-states] Values at end of function main3:
+ __fc_errno ∈ [--..--]
f1 ∈ [-2147483648. .. 2147483647.]
f2 ∈ [-2147483648. .. 2147483647.]
r ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[eva:final-states] Values at end of function main:
-
+ __fc_errno ∈ [--..--]
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
5 functions analyzed (out of 5): 100% coverage.
@@ -84,8 +83,8 @@
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 0 valid 0 unknown 0 invalid 0 total
- Preconditions 2 valid 4 unknown 1 invalid 7 total
- 28% of the logical properties reached have been proven.
+ Preconditions 1 valid 4 unknown 1 invalid 6 total
+ 16% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[report] Dumping properties in 'tests/report/result/csv.csv'
[eva] Analyzing a complete application starting at main
@@ -167,11 +166,12 @@
[eva:final-states] Values at end of function main4:
d ∈ [1. .. 1.79769313486e+308]
[eva:final-states] Values at end of function main3:
+ __fc_errno ∈ [--..--]
f1 ∈ [-2147483648. .. 2147483647.]
f2 ∈ [-2147483648. .. 2147483647.]
r ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[eva:final-states] Values at end of function main:
-
+ __fc_errno ∈ [--..--]
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
5 functions analyzed (out of 5): 100% coverage.
@@ -189,6 +189,6 @@
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 0 valid 0 unknown 0 invalid 0 total
- Preconditions 2 valid 4 unknown 1 invalid 7 total
- 28% of the logical properties reached have been proven.
+ Preconditions 1 valid 4 unknown 1 invalid 6 total
+ 16% of the logical properties reached have been proven.
----------------------------------------------------------------------------
diff --git a/tests/float/contract_special_float.c b/tests/float/contract_special_float.c
new file mode 100644
index 0000000000000000000000000000000000000000..b3627110e9d0efb478e9e42f6bf861a0f0fc7066
--- /dev/null
+++ b/tests/float/contract_special_float.c
@@ -0,0 +1,99 @@
+/* run.config*
+ OPT: -eva @EVA_CONFIG@ -warn-special-float non-finite
+ OPT: -eva @EVA_CONFIG@ -warn-special-float nan
+ OPT: -eva @EVA_CONFIG@ -warn-special-float none
+*/
+
+/*@
+ assigns \result \from x;
+ behavior normal:
+ assumes domain_arg: \is_plus_infinity(x) || (\is_finite(x) && x >= 1.);
+ ensures finite_result: \is_finite(\result);
+ ensures positive_result: \result >= 0.;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < 0.);
+ ensures nan_result: \is_NaN(\result);
+ behavior infinite:
+ assumes small_arg: \is_finite(x) && x >= 0. && x < 1.;
+ ensures infinite_result: \is_plus_infinity(\result);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
+*/
+extern double fun(double x);
+
+/*@
+ behavior normal:
+ assumes domain_arg: \is_plus_infinity(x) || (\is_finite(x) && x >= 1.);
+ assigns \result \from x;
+ ensures finite_result: \is_finite(\result);
+ ensures positive_result: \result >= 0.;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < 0.);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ behavior infinite:
+ assumes small_arg: \is_finite(x) && x >= 0. && x < 1.;
+ assigns \result \from x;
+ ensures infinite_result: \is_plus_infinity(\result);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
+*/
+extern double fun_no_default(double x);
+
+/*@
+ assigns \result \from x;
+ behavior normal:
+ assumes domain_arg: \is_plus_infinity(x) || (\is_finite(x) && x >= 1.);
+ ensures finite_result: \is_finite(\result);
+ ensures positive_result: \result >= 0.;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < 0.);
+ ensures nan_result: \is_NaN(\result);
+ behavior infinite:
+ assumes small_arg: \is_finite(x) && x >= 0. && x < 1.;
+ ensures infinite_result: \is_plus_infinity(\result);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+*/
+extern double fun_no_disjoint(double x);
+
+/*@
+ assigns \result \from x;
+ behavior normal:
+ assumes domain_arg: \is_plus_infinity(x) || (\is_finite(x) && x >= 1.);
+ ensures finite_result: \is_finite(\result);
+ ensures positive_result: \result >= 0.;
+ behavior negative:
+ assumes negative_arg: \is_minus_infinity(x) || (\is_finite(x) && x < 0.);
+ ensures nan_result: \is_NaN(\result);
+ behavior infinite:
+ assumes small_arg: \is_finite(x) && x >= 0. && x < 1.;
+ ensures infinite_result: \is_plus_infinity(\result);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ disjoint behaviors;
+*/
+extern double fun_no_complete(double x);
+
+volatile double v;
+
+int main(){
+ double a = v;
+ double w = fun(a);
+ double b = v;
+ double x = fun_no_default(b); // no default behavior
+ double c = v;
+ double y = fun_no_disjoint(c); // no disjoint behaviors
+ double d = v;
+ double z = fun_no_complete(d); // no complete behaviors
+}
diff --git a/tests/float/oracle/builtins.res.oracle b/tests/float/oracle/builtins.res.oracle
index 66f30707d3259e2969df47d8e280f469eb3f74b4..e6023b3d1ca5662c47bc5c0b07a77b5eb4feb48e 100644
--- a/tests/float/oracle/builtins.res.oracle
+++ b/tests/float/oracle/builtins.res.oracle
@@ -99,30 +99,46 @@
function log10: precondition 'arg_positive' got status invalid.
[eva] tests/float/builtins.c:85: Call to builtin exp
[eva] tests/float/builtins.c:85:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
[eva] tests/float/builtins.c:85:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/builtins.c:85:
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/builtins.c:88: Call to builtin exp
[eva] tests/float/builtins.c:88:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/builtins.c:88:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/builtins.c:88:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/builtins.c:91: Call to builtin exp
[eva] tests/float/builtins.c:91:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/builtins.c:91:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/builtins.c:91:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva:alarm] tests/float/builtins.c:94: Warning: assertion got status unknown.
[eva] tests/float/builtins.c:95: Call to builtin exp
-[eva] tests/float/builtins.c:95:
- function exp: precondition 'finite_arg' got status valid.
[eva:alarm] tests/float/builtins.c:95: Warning:
- function exp: precondition 'finite_domain' got status unknown.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status unknown.
+[eva] tests/float/builtins.c:95:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/builtins.c:95:
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/builtins.c:98: Call to builtin exp
-[eva] tests/float/builtins.c:98:
- function exp: precondition 'finite_arg' got status valid.
[eva:alarm] tests/float/builtins.c:98: Warning:
- function exp: precondition 'finite_domain' got status invalid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status invalid.
+[eva] tests/float/builtins.c:98:
+ function exp: no state left, precondition ¬(plus_infinity_arg:
+ \is_plus_infinity(x)) got status valid.
+[eva] tests/float/builtins.c:98:
+ function exp: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/builtins.c:102: Call to builtin log
[eva] tests/float/builtins.c:102:
function log: precondition 'finite_arg' got status valid.
@@ -131,9 +147,12 @@
[eva] tests/float/builtins.c:103: assertion got status valid.
[eva] tests/float/builtins.c:104: Call to builtin exp
[eva] tests/float/builtins.c:104:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/builtins.c:104:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/builtins.c:104:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva:alarm] tests/float/builtins.c:107: Warning:
pointer downcast. assert (unsigned int)(&d) ≤ 2147483647;
[eva:alarm] tests/float/builtins.c:107: Warning:
@@ -155,6 +174,7 @@
assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main_log_exp:
+ __fc_errno ∈ [--..--]
l1 ∈ {0} or UNINITIALIZED
l2 ∈ {1.00063188031} or UNINITIALIZED
l3 ∈ {1.09861228867} or UNINITIALIZED
diff --git a/tests/float/oracle/contract_special_float.0.res.oracle b/tests/float/oracle/contract_special_float.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c94819b6e7cfb0a13240953645d175cee9307247
--- /dev/null
+++ b/tests/float/oracle/contract_special_float.0.res.oracle
@@ -0,0 +1,67 @@
+[kernel] Parsing tests/float/contract_special_float.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ v ∈ [--..--]
+[eva:alarm] tests/float/contract_special_float.c:91: Warning:
+ non-finite double value. assert \is_finite(v);
+[eva] computing for function fun <- main.
+ Called from tests/float/contract_special_float.c:92.
+[eva] using specification for function fun
+[eva:alarm] tests/float/contract_special_float.c:92: Warning:
+ function fun: precondition 'domain_arg' got status unknown.
+[eva] Done for function fun
+[eva:alarm] tests/float/contract_special_float.c:93: Warning:
+ non-finite double value. assert \is_finite(v);
+[eva] computing for function fun_no_default <- main.
+ Called from tests/float/contract_special_float.c:94.
+[eva] using specification for function fun_no_default
+[eva:alarm] tests/float/contract_special_float.c:94: Warning:
+ function fun_no_default: precondition 'domain_arg' got status unknown.
+[eva] Done for function fun_no_default
+[eva:alarm] tests/float/contract_special_float.c:95: Warning:
+ non-finite double value. assert \is_finite(v);
+[eva] computing for function fun_no_disjoint <- main.
+ Called from tests/float/contract_special_float.c:96.
+[eva] using specification for function fun_no_disjoint
+[eva:alarm] tests/float/contract_special_float.c:96: Warning:
+ function fun_no_disjoint: precondition ¬(negative_arg:
+ \is_minus_infinity(x) ∨
+ (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva:alarm] tests/float/contract_special_float.c:96: Warning:
+ function fun_no_disjoint: precondition ¬(small_arg:
+ \is_finite(x) ∧ x ≥ 0. ∧
+ x < 1.) got status unknown.
+[eva] tests/float/contract_special_float.c:96:
+ function fun_no_disjoint: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun_no_disjoint
+[eva:alarm] tests/float/contract_special_float.c:97: Warning:
+ non-finite double value. assert \is_finite(v);
+[eva] computing for function fun_no_complete <- main.
+ Called from tests/float/contract_special_float.c:98.
+[eva] using specification for function fun_no_complete
+[eva:alarm] tests/float/contract_special_float.c:98: Warning:
+ function fun_no_complete: precondition ¬(negative_arg:
+ \is_minus_infinity(x) ∨
+ (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva:alarm] tests/float/contract_special_float.c:98: Warning:
+ function fun_no_complete: precondition ¬(small_arg:
+ \is_finite(x) ∧ x ≥ 0. ∧
+ x < 1.) got status unknown.
+[eva] tests/float/contract_special_float.c:98:
+ function fun_no_complete: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun_no_complete
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ a ∈ [1. .. 1.79769313486e+308]
+ w ∈ [-0. .. 1.79769313486e+308]
+ b ∈ [1. .. 1.79769313486e+308]
+ x ∈ [-0. .. 1.79769313486e+308]
+ c ∈ [1. .. 1.79769313486e+308]
+ y ∈ [-0. .. 1.79769313486e+308]
+ d ∈ [1. .. 1.79769313486e+308]
+ z ∈ [-0. .. 1.79769313486e+308]
+ __retres ∈ {0}
diff --git a/tests/float/oracle/contract_special_float.1.res.oracle b/tests/float/oracle/contract_special_float.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..47a549ed31074554153b6732f79c08a9ebd8063b
--- /dev/null
+++ b/tests/float/oracle/contract_special_float.1.res.oracle
@@ -0,0 +1,69 @@
+[kernel] Parsing tests/float/contract_special_float.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ v ∈ [--..--]
+[eva:alarm] tests/float/contract_special_float.c:91: Warning:
+ NaN double value. assert ¬\is_NaN(v);
+[eva] computing for function fun <- main.
+ Called from tests/float/contract_special_float.c:92.
+[eva] using specification for function fun
+[eva:alarm] tests/float/contract_special_float.c:92: Warning:
+ function fun: precondition ¬(negative_arg:
+ \is_minus_infinity(x) ∨
+ (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva] tests/float/contract_special_float.c:92:
+ function fun: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun
+[eva:alarm] tests/float/contract_special_float.c:93: Warning:
+ NaN double value. assert ¬\is_NaN(v);
+[eva] computing for function fun_no_default <- main.
+ Called from tests/float/contract_special_float.c:94.
+[kernel] tests/float/contract_special_float.c:94: Warning:
+ No code nor explicit assigns clause for function fun_no_default, generating default assigns from the specification
+[eva] using specification for function fun_no_default
+[eva:alarm] tests/float/contract_special_float.c:94: Warning:
+ function fun_no_default: precondition ¬(negative_arg:
+ \is_minus_infinity(x) ∨
+ (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva] tests/float/contract_special_float.c:94:
+ function fun_no_default: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun_no_default
+[eva:alarm] tests/float/contract_special_float.c:95: Warning:
+ NaN double value. assert ¬\is_NaN(v);
+[eva] computing for function fun_no_disjoint <- main.
+ Called from tests/float/contract_special_float.c:96.
+[eva] using specification for function fun_no_disjoint
+[eva:alarm] tests/float/contract_special_float.c:96: Warning:
+ function fun_no_disjoint: precondition ¬(negative_arg:
+ \is_minus_infinity(x) ∨
+ (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva] tests/float/contract_special_float.c:96:
+ function fun_no_disjoint: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun_no_disjoint
+[eva:alarm] tests/float/contract_special_float.c:97: Warning:
+ NaN double value. assert ¬\is_NaN(v);
+[eva] computing for function fun_no_complete <- main.
+ Called from tests/float/contract_special_float.c:98.
+[eva] using specification for function fun_no_complete
+[eva:alarm] tests/float/contract_special_float.c:98: Warning:
+ function fun_no_complete: precondition ¬(negative_arg:
+ \is_minus_infinity(x) ∨
+ (\is_finite(x) ∧ x < 0.)) got status unknown.
+[eva] tests/float/contract_special_float.c:98:
+ function fun_no_complete: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function fun_no_complete
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ a ∈ [-0. .. inf]
+ w ∈ [-0. .. inf]
+ b ∈ [-0. .. inf]
+ x ∈ [-0. .. inf]
+ c ∈ [-0. .. inf]
+ y ∈ [-0. .. inf]
+ d ∈ [-1.79769313486e+308 .. inf]
+ z ∈ [-inf .. inf] ∪ {NaN}
+ __retres ∈ {0}
diff --git a/tests/float/oracle/contract_special_float.2.res.oracle b/tests/float/oracle/contract_special_float.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c2ded998a7dc6580b0897db4a376efd1a2eeae9e
--- /dev/null
+++ b/tests/float/oracle/contract_special_float.2.res.oracle
@@ -0,0 +1,37 @@
+[kernel] Parsing tests/float/contract_special_float.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ v ∈ [--..--]
+[eva] computing for function fun <- main.
+ Called from tests/float/contract_special_float.c:92.
+[eva] using specification for function fun
+[eva] Done for function fun
+[eva] computing for function fun_no_default <- main.
+ Called from tests/float/contract_special_float.c:94.
+[kernel] tests/float/contract_special_float.c:94: Warning:
+ No code nor explicit assigns clause for function fun_no_default, generating default assigns from the specification
+[eva] using specification for function fun_no_default
+[eva] Done for function fun_no_default
+[eva] computing for function fun_no_disjoint <- main.
+ Called from tests/float/contract_special_float.c:96.
+[eva] using specification for function fun_no_disjoint
+[eva] Done for function fun_no_disjoint
+[eva] computing for function fun_no_complete <- main.
+ Called from tests/float/contract_special_float.c:98.
+[eva] using specification for function fun_no_complete
+[eva] Done for function fun_no_complete
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ a ∈ [-inf .. inf] ∪ {NaN}
+ w ∈ [-0. .. inf] ∪ {NaN}
+ b ∈ [-inf .. inf] ∪ {NaN}
+ x ∈ [-0. .. inf] ∪ {NaN}
+ c ∈ [-inf .. inf] ∪ {NaN}
+ y ∈ [-0. .. inf] ∪ {NaN}
+ d ∈ [-inf .. inf] ∪ {NaN}
+ z ∈ [-inf .. inf] ∪ {NaN}
+ __retres ∈ {0}
diff --git a/tests/float/oracle/math_builtins.res.oracle b/tests/float/oracle/math_builtins.res.oracle
index c72c70a0e4c8f3b114abd0704e8097c133d6c236..14723be574dbd03a221bebd1519fe28699bd41f8 100644
--- a/tests/float/oracle/math_builtins.res.oracle
+++ b/tests/float/oracle/math_builtins.res.oracle
@@ -145,23 +145,23 @@
Called from tests/float/math_builtins.c:730.
[eva] tests/float/math_builtins.c:87: Call to builtin atan
[eva] tests/float/math_builtins.c:87:
- function atan: precondition 'finite_arg' got status valid.
+ 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 'finite_arg' got status unknown.
+ function atan: precondition 'number_arg' got status unknown.
[eva] tests/float/math_builtins.c:89: Call to builtin atan
[eva] tests/float/math_builtins.c:89:
- function atan: precondition 'finite_arg' got status valid.
+ function atan: precondition 'number_arg' got status valid.
[eva] tests/float/math_builtins.c:90: Call to builtin atan
[eva] tests/float/math_builtins.c:90:
- function atan: precondition 'finite_arg' got status valid.
+ function atan: precondition 'number_arg' got status valid.
[eva] computing for function double_interval <- test_atan <- main.
Called from tests/float/math_builtins.c:91.
[eva] Recording results for double_interval
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:92: Call to builtin atan
[eva] tests/float/math_builtins.c:92:
- function atan: precondition 'finite_arg' got status valid.
+ function atan: precondition 'number_arg' got status valid.
[eva] tests/float/math_builtins.c:94: Call to builtin atanf
[eva] tests/float/math_builtins.c:94:
function atanf: precondition 'finite_arg' got status valid.
@@ -175,81 +175,55 @@
[eva] tests/float/math_builtins.c:99:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:99:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:99:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:100:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:100:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:100:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:101:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:101:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:101:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:102:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:102:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:102:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:103:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:103:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:103:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:104:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:104:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:104:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:105:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:105:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:105:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:106:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:106:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:106:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:107:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:107:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:107:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:108:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:108:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:108:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:109:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:109:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:109:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:110:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:110:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:110:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:111:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:111:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:111:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] Recording results for test_atan2_det
[eva] Done for function test_atan2_det
[eva] computing for function test_atan2 <- main.
@@ -265,9 +239,7 @@
[eva] tests/float/math_builtins.c:118:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:118:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:118:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] computing for function double_interval <- test_atan2 <- main.
Called from tests/float/math_builtins.c:119.
[eva] Recording results for double_interval
@@ -275,9 +247,7 @@
[eva] tests/float/math_builtins.c:120:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:120:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:120:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] computing for function double_interval <- test_atan2 <- main.
Called from tests/float/math_builtins.c:121.
[eva] Recording results for double_interval
@@ -285,9 +255,7 @@
[eva] tests/float/math_builtins.c:122:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:122:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:122:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] computing for function double_interval <- test_atan2 <- main.
Called from tests/float/math_builtins.c:123.
[eva] Recording results for double_interval
@@ -295,9 +263,7 @@
[eva] tests/float/math_builtins.c:124:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:124:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:124:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] computing for function double_interval <- test_atan2 <- main.
Called from tests/float/math_builtins.c:125.
[eva] Recording results for double_interval
@@ -305,9 +271,7 @@
[eva] tests/float/math_builtins.c:126:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:126:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:126:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] computing for function double_interval <- test_atan2 <- main.
Called from tests/float/math_builtins.c:127.
[eva] Recording results for double_interval
@@ -319,9 +283,7 @@
[eva] tests/float/math_builtins.c:129:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:129:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:129:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] computing for function double_interval <- test_atan2 <- main.
Called from tests/float/math_builtins.c:130.
[eva] Recording results for double_interval
@@ -329,9 +291,7 @@
[eva] tests/float/math_builtins.c:131:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:131:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:131:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] computing for function double_interval <- test_atan2 <- main.
Called from tests/float/math_builtins.c:132.
[eva] Recording results for double_interval
@@ -339,9 +299,7 @@
[eva] tests/float/math_builtins.c:133:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:133:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:133:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] computing for function double_interval <- test_atan2 <- main.
Called from tests/float/math_builtins.c:134.
[eva] Recording results for double_interval
@@ -349,9 +307,7 @@
[eva] tests/float/math_builtins.c:135:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:135:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:135:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] computing for function double_interval <- test_atan2 <- main.
Called from tests/float/math_builtins.c:136.
[eva] Recording results for double_interval
@@ -359,83 +315,57 @@
[eva] tests/float/math_builtins.c:137:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:137:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:137:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:138:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:138:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:138:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:139:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:139:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:139:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:140:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:140:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:140:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] tests/float/math_builtins.c:141:
Call to builtin Frama_C_atan2 for function atan2
[eva] tests/float/math_builtins.c:141:
- function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:141:
- function atan2: precondition 'finite_result' got status valid.
+ function atan2: precondition 'number_args' got status valid.
[eva] Recording results for test_atan2
[eva] Done for function test_atan2
[eva] computing for function test_pow_det <- main.
Called from tests/float/math_builtins.c:733.
[eva] tests/float/math_builtins.c:145:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:145:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:145:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:146:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:146:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:146:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:147:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:147:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:147:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:148:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:148:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:148:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:149:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:149:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:149:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:150:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:150:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:150:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:151:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:151:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:151:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:152:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:152:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:152:
function pow: precondition 'finite_logic_res' got status valid.
[eva] Recording results for test_pow_det
@@ -448,14 +378,10 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:170:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:170:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:170: Warning:
function pow: precondition 'finite_logic_res' got status invalid.
[eva] tests/float/math_builtins.c:172:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:172:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:172: Warning:
function pow: precondition 'finite_logic_res' got status invalid.
[eva] computing for function double_interval <- test_pow_singleton_exp <- main.
@@ -464,26 +390,18 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:176:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:176:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:176: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] tests/float/math_builtins.c:177:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:177:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:177: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] tests/float/math_builtins.c:180:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:180:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:180: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] tests/float/math_builtins.c:181:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:181:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:181: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow_singleton_exp <- main.
@@ -492,8 +410,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:185:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:185:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:185: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow_singleton_exp <- main.
@@ -502,8 +418,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:187:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:187:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:187: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow_singleton_exp <- main.
@@ -512,8 +426,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:191:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:191:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:191:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:192:
@@ -524,8 +436,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:194:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:194:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:194:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:195:
@@ -533,14 +443,10 @@
[0.2500000000000000*2^-1022 .. 1.2707064924076672*2^-330]
[eva] tests/float/math_builtins.c:199:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:199:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:199:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:200:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:200:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:200:
function pow: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_pow_singleton_exp <- main.
@@ -549,32 +455,22 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:203:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:203:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:203:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:204:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:204:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:204:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:205:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:205:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:205:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:206:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:206:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:206:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:207:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:207:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:207:
function pow: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_pow_singleton_exp <- main.
@@ -583,14 +479,10 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:210:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:210:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:210:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:211:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:211:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:211:
function pow: precondition 'finite_logic_res' got status valid.
[eva] Recording results for test_pow_singleton_exp
@@ -603,8 +495,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:218:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:218:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:218:
function pow: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_pow <- main.
@@ -613,8 +503,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:220:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:220:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:220:
function pow: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_pow <- main.
@@ -623,8 +511,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:222:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:222:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:222:
function pow: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_pow <- main.
@@ -637,8 +523,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:230:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:230:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:230: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -647,8 +531,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:232:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:232:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:232: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -657,8 +539,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:234:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:234:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:234: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -671,8 +551,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:237:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:237:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:237:
function pow: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_pow <- main.
@@ -685,8 +563,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:242:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:242:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:242:
function pow: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_pow <- main.
@@ -699,8 +575,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:247:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:247:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:247: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -713,8 +587,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:250:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:250:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:250: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -727,8 +599,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:256:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:256:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:256: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -741,8 +611,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:261:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:261:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:261: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -755,8 +623,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:266:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:266:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:266:
function pow: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_pow <- main.
@@ -769,8 +635,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:271:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:271:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:271: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -783,8 +647,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:276:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:276:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:276: Warning:
function pow: precondition 'finite_logic_res' got status invalid.
[eva] computing for function double_interval <- test_pow <- main.
@@ -793,8 +655,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:278:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:278:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:278: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -803,8 +663,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:280:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:280:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:280: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -813,8 +671,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:282:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:282:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:282: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_pow <- main.
@@ -827,8 +683,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:287:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:287:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:287: Warning:
function pow: precondition 'finite_logic_res' got status invalid.
[eva] computing for function double_interval <- test_pow <- main.
@@ -841,8 +695,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:292:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:292:
- function pow: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:292: Warning:
function pow: precondition 'finite_logic_res' got status unknown.
[eva] tests/float/math_builtins.c:292: Frama_C_show_each_unreachable:
@@ -852,8 +704,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:295:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:295:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:295:
function pow: precondition 'finite_logic_res' got status valid.
[eva] Recording results for test_pow
@@ -863,45 +713,31 @@
[eva] tests/float/math_builtins.c:405:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:405:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:405:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:406:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:406:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:406:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:407:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:407:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:407:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:408:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:408:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:408:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:409:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:409:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:409:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:410:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:410:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:410:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:411:
Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:411:
- function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:411: Warning:
- function fmod: precondition 'finite_logic_result' got status invalid.
+ function fmod: precondition 'in_domain' got status invalid.
[eva] Recording results for test_fmod_det
[eva] Done for function test_fmod_det
[eva] computing for function test_fmod <- main.
@@ -913,27 +749,19 @@
[eva] tests/float/math_builtins.c:417:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:417:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:417:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:418:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:418:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:418:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:419:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:419:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:419:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:420:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:420:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:420:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:421.
[eva] Recording results for double_interval
@@ -941,15 +769,11 @@
[eva] tests/float/math_builtins.c:422:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:422:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:422:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:423:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:423:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:423:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:424.
[eva] Recording results for double_interval
@@ -961,9 +785,7 @@
[eva] tests/float/math_builtins.c:426:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:426:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:426:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:427.
[eva] Recording results for double_interval
@@ -975,15 +797,11 @@
[eva] tests/float/math_builtins.c:429:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:429:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:429:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] tests/float/math_builtins.c:430:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:430:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:430:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:431.
[eva] Recording results for double_interval
@@ -994,10 +812,8 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:433:
Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:433:
- function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:433: Warning:
- function fmod: precondition 'finite_logic_result' got status unknown.
+ function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:434.
[eva] Recording results for double_interval
@@ -1008,40 +824,32 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:436:
Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:436:
- function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:436: Warning:
- function fmod: precondition 'finite_logic_result' got status unknown.
+ function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:437.
[eva] Recording results for double_interval
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:438:
Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:438:
- function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:438: Warning:
- function fmod: precondition 'finite_logic_result' got status invalid.
+ function fmod: precondition 'in_domain' got status invalid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:439.
[eva] Recording results for double_interval
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:440:
Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:440:
- function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:440: Warning:
- function fmod: precondition 'finite_logic_result' got status unknown.
+ function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:441.
[eva] Recording results for double_interval
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:442:
Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:442:
- function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:442: Warning:
- function fmod: precondition 'finite_logic_result' got status unknown.
+ function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:443.
[eva] Recording results for double_interval
@@ -1049,9 +857,7 @@
[eva] tests/float/math_builtins.c:444:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:444:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:444:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:445.
[eva] Recording results for double_interval
@@ -1059,9 +865,7 @@
[eva] tests/float/math_builtins.c:446:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:446:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:446:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:447.
[eva] Recording results for double_interval
@@ -1069,9 +873,7 @@
[eva] tests/float/math_builtins.c:448:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:448:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:448:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:449.
[eva] Recording results for double_interval
@@ -1079,9 +881,7 @@
[eva] tests/float/math_builtins.c:450:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:450:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:450:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:451.
[eva] Recording results for double_interval
@@ -1089,9 +889,7 @@
[eva] tests/float/math_builtins.c:452:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:452:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:452:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:453.
[eva] Recording results for double_interval
@@ -1099,9 +897,7 @@
[eva] tests/float/math_builtins.c:454:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:454:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:454:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:455.
[eva] Recording results for double_interval
@@ -1109,9 +905,7 @@
[eva] tests/float/math_builtins.c:456:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:456:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:456:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:457.
[eva] Recording results for double_interval
@@ -1119,9 +913,7 @@
[eva] tests/float/math_builtins.c:458:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:458:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:458:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:459.
[eva] Recording results for double_interval
@@ -1133,9 +925,7 @@
[eva] tests/float/math_builtins.c:461:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:461:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:461:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:462.
[eva] Recording results for double_interval
@@ -1143,9 +933,7 @@
[eva] tests/float/math_builtins.c:463:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:463:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:463:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:464.
[eva] Recording results for double_interval
@@ -1153,9 +941,7 @@
[eva] tests/float/math_builtins.c:465:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:465:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:465:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:466.
[eva] Recording results for double_interval
@@ -1163,9 +949,7 @@
[eva] tests/float/math_builtins.c:467:
Call to builtin Frama_C_fmod for function fmod
[eva] tests/float/math_builtins.c:467:
- function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:467:
- function fmod: precondition 'finite_logic_result' got status valid.
+ function fmod: precondition 'in_domain' got status valid.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:468.
[eva] Recording results for double_interval
@@ -1176,30 +960,24 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:470:
Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:470:
- function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:470: Warning:
- function fmod: precondition 'finite_logic_result' got status unknown.
+ function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:471.
[eva] Recording results for double_interval
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:472:
Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:472:
- function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:472: Warning:
- function fmod: precondition 'finite_logic_result' got status unknown.
+ function fmod: precondition 'in_domain' got status unknown.
[eva] computing for function double_interval <- test_fmod <- main.
Called from tests/float/math_builtins.c:473.
[eva] Recording results for double_interval
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:474:
Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:474:
- function fmod: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:474: Warning:
- function fmod: precondition 'finite_logic_result' got status unknown.
+ function fmod: precondition 'in_domain' got status unknown.
[eva] Recording results for test_fmod
[eva] Done for function test_fmod
[eva] computing for function test_sqrt_det <- main.
@@ -1285,39 +1063,58 @@
[eva] tests/float/math_builtins.c:516:
Call to builtin Frama_C_exp for function exp
[eva] tests/float/math_builtins.c:516:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/math_builtins.c:516:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:516:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:517:
Call to builtin Frama_C_exp for function exp
[eva] tests/float/math_builtins.c:517:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/math_builtins.c:517:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:517:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:518:
Call to builtin Frama_C_exp for function exp
[eva] tests/float/math_builtins.c:518:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
[eva] tests/float/math_builtins.c:518:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:518:
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:519:
Call to builtin Frama_C_exp for function exp
[eva] tests/float/math_builtins.c:519:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/math_builtins.c:519:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:519:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:520:
Call to builtin Frama_C_exp for function exp
[eva] tests/float/math_builtins.c:520:
- function exp: precondition 'finite_arg' got status valid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+[eva] tests/float/math_builtins.c:520:
+ function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:520:
- function exp: precondition 'finite_domain' got status valid.
+ function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:521:
Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:521:
- function exp: precondition 'finite_arg' got status valid.
[eva:alarm] tests/float/math_builtins.c:521: Warning:
- function exp: precondition 'finite_domain' got status invalid.
+ function exp: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status invalid.
+[eva] tests/float/math_builtins.c:521:
+ function exp: no state left, precondition ¬(plus_infinity_arg:
+ \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:521:
+ function exp: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] Recording results for test_exp_det
[eva] Done for function test_exp_det
[eva] computing for function test_log_det <- main.
@@ -1404,50 +1201,34 @@
Called from tests/float/math_builtins.c:744.
[eva] tests/float/math_builtins.c:156:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:156:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:156:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:157:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:157:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:157:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:158:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:158:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:158:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:159:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:159:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:159:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:160:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:160:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:160:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:161:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:161:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:161:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:162:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:162:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:162:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:163:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:163:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:163:
function powf: precondition 'finite_logic_res' got status valid.
[eva] Recording results for test_powf_det
@@ -1460,14 +1241,10 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:303:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:303:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:303: Warning:
function powf: precondition 'finite_logic_res' got status invalid.
[eva] tests/float/math_builtins.c:305:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:305:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:305: Warning:
function powf: precondition 'finite_logic_res' got status invalid.
[eva] computing for function double_interval <- test_powf_singleton_exp <- main.
@@ -1476,26 +1253,18 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:309:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:309:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:309: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] tests/float/math_builtins.c:310:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:310:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:310: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] tests/float/math_builtins.c:313:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:313:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:313: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] tests/float/math_builtins.c:314:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:314:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:314: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_powf_singleton_exp <- main.
@@ -1504,8 +1273,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:318:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:318:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:318:
function powf: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_powf_singleton_exp <- main.
@@ -1514,8 +1281,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:320:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:320:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:320: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_powf_singleton_exp <- main.
@@ -1524,8 +1289,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:324:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:324:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:324:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:325:
@@ -1536,21 +1299,15 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:327:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:327:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:327:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:328: Frama_C_show_each_j: {0}
[eva] tests/float/math_builtins.c:332:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:332:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:332:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:333:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:333:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:333:
function powf: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_powf_singleton_exp <- main.
@@ -1559,32 +1316,22 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:336:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:336:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:336:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:337:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:337:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:337:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:338:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:338:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:338:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:339:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:339:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:339:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:340:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:340:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:340:
function powf: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_powf_singleton_exp <- main.
@@ -1593,14 +1340,10 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:343:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:343:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:343:
function powf: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:344:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:344:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:344:
function powf: precondition 'finite_logic_res' got status valid.
[eva] Recording results for test_powf_singleton_exp
@@ -1613,8 +1356,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:351:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:351:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:351:
function powf: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1623,8 +1364,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:353:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:353:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:353:
function powf: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1633,8 +1372,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:355:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:355:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:355:
function powf: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1647,8 +1384,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:363:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:363:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:363: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1657,8 +1392,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:365:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:365:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:365: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1667,8 +1400,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:367:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:367:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:367: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1681,8 +1412,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:370:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:370:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:370:
function powf: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1695,8 +1424,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:375:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:375:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:375:
function powf: precondition 'finite_logic_res' got status valid.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1709,8 +1436,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:380:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:380:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:380: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1723,8 +1448,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:385:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:385:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:385: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1737,8 +1460,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:391:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:391:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:391: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1751,8 +1472,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:396:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:396:
- function powf: precondition 'finite_args' got status valid.
[eva:alarm] tests/float/math_builtins.c:396: Warning:
function powf: precondition 'finite_logic_res' got status unknown.
[eva] computing for function double_interval <- test_powf <- main.
@@ -1765,8 +1484,6 @@
[eva] Done for function double_interval
[eva] tests/float/math_builtins.c:401:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:401:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:401:
function powf: precondition 'finite_logic_res' got status valid.
[eva] Recording results for test_powf
@@ -1854,33 +1571,48 @@
[eva] tests/float/math_builtins.c:525:
Call to builtin Frama_C_expf for function expf
[eva] tests/float/math_builtins.c:525:
- function expf: precondition 'finite_arg' got status valid.
+ function expf: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
+[eva] tests/float/math_builtins.c:525:
+ function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:525:
- function expf: precondition 'res_finite' got status valid.
+ function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:526:
Call to builtin Frama_C_expf for function expf
[eva] tests/float/math_builtins.c:526:
- function expf: precondition 'finite_arg' got status valid.
+ function expf: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
[eva] tests/float/math_builtins.c:526:
- function expf: precondition 'res_finite' got status valid.
+ function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:526:
+ function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:527:
Call to builtin Frama_C_expf for function expf
[eva] tests/float/math_builtins.c:527:
- function expf: precondition 'finite_arg' got status valid.
+ function expf: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
+[eva] tests/float/math_builtins.c:527:
+ function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:527:
- function expf: precondition 'res_finite' got status valid.
+ function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:528:
Call to builtin Frama_C_expf for function expf
[eva] tests/float/math_builtins.c:528:
- function expf: precondition 'finite_arg' got status valid.
+ function expf: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
+[eva] tests/float/math_builtins.c:528:
+ function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
[eva] tests/float/math_builtins.c:528:
- function expf: precondition 'res_finite' got status valid.
+ function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] tests/float/math_builtins.c:529:
Call to builtin Frama_C_expf for function expf
[eva] tests/float/math_builtins.c:529:
- function expf: precondition 'finite_arg' got status valid.
+ function expf: precondition ¬(overflow_arg:
+ \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
[eva] tests/float/math_builtins.c:529:
- function expf: precondition 'res_finite' got status valid.
+ function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+[eva] tests/float/math_builtins.c:529:
+ function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
[eva] Recording results for test_expf_det
[eva] Done for function test_expf_det
[eva] computing for function test_logf_det <- main.
@@ -1967,14 +1699,10 @@
Called from tests/float/math_builtins.c:753.
[eva] tests/float/math_builtins.c:569:
Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:569:
- function pow: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:569:
function pow: precondition 'finite_logic_res' got status valid.
[eva] tests/float/math_builtins.c:570:
Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:570:
- function powf: precondition 'finite_args' got status valid.
[eva] tests/float/math_builtins.c:570:
function powf: precondition 'finite_logic_res' got status valid.
[eva] Recording results for test_diff_pow_powf
@@ -2524,15 +2252,18 @@
y ∈ {1.0000000000000000}
z ∈ {1.0806046117362795*2^-1}
[eva:final-states] Values at end of function test_diff_pow_powf:
+ __fc_errno ∈ [--..--]
d ∈ {1.3824840787361052*2^-96}
f32__f ∈ {1.382483*2^-96}
[eva:final-states] Values at end of function test_exp_det:
+ __fc_errno ∈ [--..--]
a ∈ {1.7094457008275896*2^60}
b ∈ {1.0826822658929016*2^-3}
c ∈ {1.0000000000000000}
d ∈ {1.0000000000000000}
e ∈ {1.4715177646857693*2^-2}
[eva:final-states] Values at end of function test_expf_det:
+ __fc_errno ∈ [--..--]
f32__a ∈ {1.709445*2^60}
f32__b ∈ {1.082682*2^-3}
f32__c ∈ {1.000000}
@@ -2613,6 +2344,7 @@
f32__a ∈ {3.740641}
f32__b ∈ {-2.079441}
[eva:final-states] Values at end of function test_pow:
+ __fc_errno ∈ [--..--]
x ∈ [-1.4551915228366852*2^36 .. -1.1641532182693481*2^33]
y ∈ [-1.0000000000000000*2^-1 .. 9.5000000000000000]
a ∈ {1.0000000000000000}
@@ -2634,6 +2366,7 @@
q ∈ [-1.9999999999999998*2^1023 .. 1.9999999999999998*2^1023]
r ∈ [1.2649110640673517*2^-2 .. 1.4725502860585131*2^31]
[eva:final-states] Values at end of function test_pow_det:
+ __fc_errno ∈ [--..--]
a ∈ {1.0000000000000000}
b ∈ {0}
c ∈ {1.0000000000000000}
@@ -2643,6 +2376,7 @@
g ∈ {1.6817928305074290*2^-21}
h ∈ {1.0000000000000000}
[eva:final-states] Values at end of function test_pow_singleton_exp:
+ __fc_errno ∈ [--..--]
x ∈ [-3.5000000000000000 .. -1.0000000000000000*2^-3]
c ∈ [0.0000000000000000 .. 4.5603590867386749]
d ∈ [1.7542478229978975*2^-3 .. 1.9999999999999998*2^1023]
@@ -2662,6 +2396,7 @@
r ∈ [1.3061224489795917*2^-4 .. 64.0000000000000000]
s ∈ [-8.0000000000000000 .. -1.1428571428571428*2^-2]
[eva:final-states] Values at end of function test_powf:
+ __fc_errno ∈ [--..--]
f32__x ∈ [-0.000000 .. 10.000000]
f32__y ∈ [-0.000000 .. 5.000000]
f32__a ∈ {1.000000}
@@ -2678,6 +2413,7 @@
f32__l ∈ [-1024.000000 .. 256.000000]
f32__m ∈ [-0.000000 .. 1.525878*2^16]
[eva:final-states] Values at end of function test_powf_det:
+ __fc_errno ∈ [--..--]
f32__a ∈ {1.000000}
f32__b ∈ {0}
f32__c ∈ {1.000000}
@@ -2687,6 +2423,7 @@
f32__g ∈ {1.681792*2^-21}
f32__h ∈ {1.000000}
[eva:final-states] Values at end of function test_powf_singleton_exp:
+ __fc_errno ∈ [--..--]
f32__x ∈ [-3.500000 .. -1.000000*2^-3]
f32__c ∈ [0.000000 .. 4.560359]
f32__d ∈ [1.754247*2^-3 .. 1.999999*2^127]
@@ -2778,6 +2515,7 @@
f32__e ∈ {-0.000000}
f32__f ∈ {-1.000000}
[eva:final-states] Values at end of function main:
+ __fc_errno ∈ [--..--]
__retres ∈ {0}
[from] Computing for function double_interval
[from] Done for function double_interval
@@ -2948,8 +2686,10 @@
[from] Function double_interval:
\result FROM min; max; nondet
[from] Function exp:
+ __fc_errno FROM x
\result FROM x
[from] Function expf:
+ __fc_errno FROM x
\result FROM x
[from] Function floor:
\result FROM x
@@ -2966,8 +2706,10 @@
[from] Function logf:
\result FROM x
[from] Function pow:
+ __fc_errno FROM x; y
\result FROM x; y
[from] Function powf:
+ __fc_errno FROM x; y
\result FROM x; y
[from] Function round:
\result FROM x
@@ -3000,11 +2742,11 @@
[from] Function test_cos_det:
NO EFFECTS
[from] Function test_diff_pow_powf:
- NO EFFECTS
+ __fc_errno FROM \nothing
[from] Function test_exp_det:
- NO EFFECTS
+ __fc_errno FROM \nothing
[from] Function test_expf_det:
- NO EFFECTS
+ __fc_errno FROM \nothing
[from] Function test_floor:
NO EFFECTS
[from] Function test_floor_det:
@@ -3026,17 +2768,17 @@
[from] Function test_logf_det:
NO EFFECTS
[from] Function test_pow:
- NO EFFECTS
+ __fc_errno FROM nondet
[from] Function test_pow_det:
- NO EFFECTS
+ __fc_errno FROM \nothing
[from] Function test_pow_singleton_exp:
- NO EFFECTS
+ __fc_errno FROM nondet
[from] Function test_powf:
- NO EFFECTS
+ __fc_errno FROM nondet
[from] Function test_powf_det:
- NO EFFECTS
+ __fc_errno FROM \nothing
[from] Function test_powf_singleton_exp:
- NO EFFECTS
+ __fc_errno FROM nondet
[from] Function test_round:
NO EFFECTS
[from] Function test_round_det:
@@ -3068,6 +2810,7 @@
[from] Function test_truncf_det:
NO EFFECTS
[from] Function main:
+ __fc_errno FROM \nothing
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function double_interval:
@@ -3118,15 +2861,15 @@
[inout] Inputs for function test_cos_det:
\nothing
[inout] Out (internal) for function test_diff_pow_powf:
- d; f32__f
+ __fc_errno; d; f32__f
[inout] Inputs for function test_diff_pow_powf:
\nothing
[inout] Out (internal) for function test_exp_det:
- a; b; c; d; e
+ __fc_errno; a; b; c; d; e
[inout] Inputs for function test_exp_det:
nondet
[inout] Out (internal) for function test_expf_det:
- f32__a; f32__b; f32__c; f32__d; f32__e
+ __fc_errno; f32__a; f32__b; f32__c; f32__d; f32__e
[inout] Inputs for function test_expf_det:
\nothing
[inout] Out (internal) for function test_floor:
@@ -3171,32 +2914,33 @@
[inout] Inputs for function test_logf_det:
nondet
[inout] Out (internal) for function test_pow:
- x; y; a; b; c; d; e; f; g; h; i; j; k; l; m; n; o; p; q; r
+ __fc_errno; x; y; a; b; c; d; e; f; g; h; i; j; k; l; m; n; o; p; q; r
[inout] Inputs for function test_pow:
nondet
[inout] Out (internal) for function test_pow_det:
- a; b; c; d; e; f; g; h
+ __fc_errno; a; b; c; d; e; f; g; h
[inout] Inputs for function test_pow_det:
\nothing
[inout] Out (internal) for function test_pow_singleton_exp:
- x; c; d; e; f; g; h; i; j; k; l; m; n; o; p; q; r; s
+ __fc_errno; x; c; d; e; f; g; h; i; j; k; l; m; n; o; p; q; r; s
[inout] Inputs for function test_pow_singleton_exp:
nondet
[inout] Out (internal) for function test_powf:
- f32__x; f32__y; tmp; f32__a; tmp_1; f32__b; tmp_3; f32__c; tmp_5; tmp_6;
- f32__d; tmp_8; f32__e; tmp_10; f32__f; tmp_12; tmp_13; f32__g; tmp_15;
- tmp_16; f32__h; tmp_18; tmp_19; f32__i; tmp_21; tmp_22; f32__j; tmp_24;
- tmp_25; f32__k; tmp_27; tmp_28; f32__l; tmp_30; tmp_31; f32__m
+ __fc_errno; f32__x; f32__y; tmp; f32__a; tmp_1; f32__b; tmp_3; f32__c;
+ tmp_5; tmp_6; f32__d; tmp_8; f32__e; tmp_10; f32__f; tmp_12; tmp_13;
+ f32__g; tmp_15; tmp_16; f32__h; tmp_18; tmp_19; f32__i; tmp_21; tmp_22;
+ f32__j; tmp_24; tmp_25; f32__k; tmp_27; tmp_28; f32__l; tmp_30; tmp_31;
+ f32__m
[inout] Inputs for function test_powf:
nondet
[inout] Out (internal) for function test_powf_det:
- f32__a; f32__b; f32__c; f32__d; f32__e; f32__f; f32__g; f32__h
+ __fc_errno; f32__a; f32__b; f32__c; f32__d; f32__e; f32__f; f32__g; f32__h
[inout] Inputs for function test_powf_det:
\nothing
[inout] Out (internal) for function test_powf_singleton_exp:
- f32__x; tmp; tmp_0; f32__c; f32__d; f32__e; f32__f; tmp_5; f32__g;
- tmp_7; f32__h; tmp_9; f32__i; tmp_11; f32__j; f32__k; f32__l; tmp_15;
- f32__m; f32__n; f32__o; f32__p; f32__q; tmp_21; f32__r; f32__s
+ __fc_errno; f32__x; tmp; tmp_0; f32__c; f32__d; f32__e; f32__f; tmp_5;
+ f32__g; tmp_7; f32__h; tmp_9; f32__i; tmp_11; f32__j; f32__k; f32__l;
+ tmp_15; f32__m; f32__n; f32__o; f32__p; f32__q; tmp_21; f32__r; f32__s
[inout] Inputs for function test_powf_singleton_exp:
nondet
[inout] Out (internal) for function test_round:
@@ -3252,7 +2996,7 @@
[inout] Inputs for function test_truncf_det:
\nothing
[inout] Out (internal) for function main:
- __retres
+ __fc_errno; __retres
[inout] Inputs for function main:
nondet; any_double; any_float
/* Generated by Frama-C */
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 02d4b53e0b88d1de3344dd38408a5e06a4b952bc..236b5f91450558595cd5c4d24239700a18dbe80a 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2418,10 +2418,13 @@
[ Extern ] Post-condition 'positive_result'
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 132)
+[ Extern ] Froms (file share/libc/math.h, line 135)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2435,10 +2438,13 @@
[ Extern ] Post-condition 'positive_result'
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 138)
+[ Extern ] Froms (file share/libc/math.h, line 156)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2452,10 +2458,13 @@
[ Extern ] Post-condition 'positive_result'
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 144)
+[ Extern ] Froms (file share/libc/math.h, line 177)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2469,10 +2478,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 150)
+[ Extern ] Froms (file share/libc/math.h, line 198)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2486,10 +2498,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 156)
+[ Extern ] Froms (file share/libc/math.h, line 219)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2503,10 +2518,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 162)
+[ Extern ] Froms (file share/libc/math.h, line 240)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2526,7 +2544,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 168)
+[ Extern ] Froms (file share/libc/math.h, line 258)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2546,7 +2564,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 175)
+[ Extern ] Froms (file share/libc/math.h, line 272)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2566,7 +2584,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 182)
+[ Extern ] Froms (file share/libc/math.h, line 286)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2583,7 +2601,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 190)
+[ Extern ] Froms (file share/libc/math.h, line 300)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2600,7 +2618,24 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 197)
+[ Extern ] Froms (file share/libc/math.h, line 313)
+ assigns \result \from x, y;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'atan2l'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 326)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2620,10 +2655,13 @@
[ Extern ] Post-condition 'result_domain'
ensures result_domain: -1. ≤ \result ≤ 1.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 205)
+[ Extern ] Froms (file share/libc/math.h, line 342)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2640,10 +2678,13 @@
[ Extern ] Post-condition 'result_domain'
ensures result_domain: -1. ≤ \result ≤ 1.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 212)
+[ Extern ] Froms (file share/libc/math.h, line 364)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2660,10 +2701,13 @@
[ Extern ] Post-condition 'result_domain'
ensures result_domain: -1. ≤ \result ≤ 1.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 219)
+[ Extern ] Froms (file share/libc/math.h, line 386)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2680,10 +2724,13 @@
[ Extern ] Post-condition 'result_domain'
ensures result_domain: -1. ≤ \result ≤ 1.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 226)
+[ Extern ] Froms (file share/libc/math.h, line 408)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2700,10 +2747,13 @@
[ Extern ] Post-condition 'result_domain'
ensures result_domain: -1. ≤ \result ≤ 1.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 233)
+[ Extern ] Froms (file share/libc/math.h, line 430)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2720,10 +2770,13 @@
[ Extern ] Post-condition 'result_domain'
ensures result_domain: -1. ≤ \result ≤ 1.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 240)
+[ Extern ] Froms (file share/libc/math.h, line 452)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2734,208 +2787,178 @@
--- Properties of Function 'acosh'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition for 'normal' 'positive_result'
+[ Extern ] Post-condition 'positive_result'
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
Unverifiable but considered Valid.
-[ Extern ] Post-condition for 'infinite' 'result_plus_infinity'
- ensures result_plus_infinity: \is_plus_infinity(\result)
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Post-condition for 'domain_error' 'errno_set'
- ensures errno_set: __fc_errno ≡ 1
+[ Extern ] Assigns nothing
+ assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 251)
- assigns __fc_errno, \result;
+[ Extern ] Froms (file share/libc/math.h, line 478)
+ assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 262)
- assigns __fc_errno, \result;
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'acoshf'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'positive_result'
+ ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'infinite' nothing
- assigns \nothing;
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'normal' nothing
+[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 251)
- assigns __fc_errno \from x;
- Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 251)
+[ Extern ] Froms (file share/libc/math.h, line 504)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 262)
- assigns __fc_errno \from x;
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'acoshl'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'positive_result'
+ ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 262)
- assigns \result \from x;
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 258)
- assigns \result \from x;
+[ Extern ] Assigns nothing
+ assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 254)
+[ Extern ] Froms (file share/libc/math.h, line 530)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
-[ Valid ] Behavior 'domain_error'
- behavior domain_error
- by Frama-C kernel.
-[ Valid ] Behavior 'infinite'
- behavior infinite
- by Frama-C kernel.
-[ Valid ] Behavior 'normal'
- behavior normal
- by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'acoshf'
+--- Properties of Function 'exp'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition for 'normal' 'res_finite'
+ ensures res_finite: \is_finite(\result)
+ Unverifiable but considered Valid.
[ Extern ] Post-condition for 'normal' 'positive_result'
- ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
+ ensures positive_result: \result > 0.
Unverifiable but considered Valid.
-[ Extern ] Post-condition for 'infinite' 'result_plus_infinity'
- ensures result_plus_infinity: \is_plus_infinity(\result)
+[ Extern ] Post-condition for 'normal' 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Post-condition for 'domain_error' 'errno_set'
- ensures errno_set: __fc_errno ≡ 1
+[ Extern ] Post-condition for 'underflow' 'zero_res'
+ ensures zero_res: \result ≡ 0.
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 269)
- assigns __fc_errno, \result;
+[ Extern ] Post-condition for 'underflow' 'errno_set'
+ ensures errno_set: __fc_errno ≡ 34
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'minus_infinity' 'zero_result'
+ ensures zero_result: \is_finite(\result) ∧ \result ≡ 0.
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'minus_infinity' 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 280)
+[ Extern ] Assigns (file share/libc/math.h, line 573)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'infinite' nothing
+[ Extern ] Assigns for 'minus_infinity' nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 269)
+[ Extern ] Froms (file share/libc/math.h, line 573)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 269)
+[ Extern ] Froms (file share/libc/math.h, line 573)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 280)
- assigns __fc_errno \from x;
- Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 280)
- assigns \result \from x;
- Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 276)
+[ Extern ] Froms for 'minus_infinity' (file share/libc/math.h, line 596)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 272)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 577)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
-[ Valid ] Behavior 'domain_error'
- behavior domain_error
- by Frama-C kernel.
-[ Valid ] Behavior 'infinite'
- behavior infinite
+[ Valid ] Behavior 'minus_infinity'
+ behavior minus_infinity
by Frama-C kernel.
[ Valid ] Behavior 'normal'
behavior normal
by Frama-C kernel.
+[ Valid ] Behavior 'underflow'
+ behavior underflow
+ by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'acoshl'
+--- Properties of Function 'expf'
--------------------------------------------------------------------------------
+[ Extern ] Post-condition for 'normal' 'res_finite'
+ ensures res_finite: \is_finite(\result)
+ Unverifiable but considered Valid.
[ Extern ] Post-condition for 'normal' 'positive_result'
- ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
+ ensures positive_result: \result > 0.
Unverifiable but considered Valid.
-[ Extern ] Post-condition for 'infinite' 'result_plus_infinity'
- ensures result_plus_infinity: \is_plus_infinity(\result)
+[ Extern ] Post-condition for 'normal' 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Post-condition for 'domain_error' 'errno_set'
- ensures errno_set: __fc_errno ≡ 1
+[ Extern ] Post-condition for 'underflow' 'zero_res'
+ ensures zero_res: \result ≡ 0.
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 287)
- assigns __fc_errno, \result;
+[ Extern ] Post-condition for 'underflow' 'errno_set'
+ ensures errno_set: __fc_errno ≡ 34
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'minus_infinity' 'zero_result'
+ ensures zero_result: \is_finite(\result) ∧ \result ≡ 0.
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 298)
+[ Extern ] Post-condition for 'minus_infinity' 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 610)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'infinite' nothing
+[ Extern ] Assigns for 'minus_infinity' nothing
assigns \nothing;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 287)
+[ Extern ] Froms (file share/libc/math.h, line 610)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 287)
+[ Extern ] Froms (file share/libc/math.h, line 610)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 298)
- assigns __fc_errno \from x;
- Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 298)
+[ Extern ] Froms for 'minus_infinity' (file share/libc/math.h, line 633)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 294)
- assigns \result \from x;
- Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 290)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 614)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
-[ Valid ] Behavior 'domain_error'
- behavior domain_error
- by Frama-C kernel.
-[ Valid ] Behavior 'infinite'
- behavior infinite
+[ Valid ] Behavior 'minus_infinity'
+ behavior minus_infinity
by Frama-C kernel.
[ Valid ] Behavior 'normal'
behavior normal
by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'exp'
---------------------------------------------------------------------------------
-
-[ Extern ] Post-condition 'res_finite'
- ensures res_finite: \is_finite(\result)
- Unverifiable but considered Valid.
-[ Extern ] Post-condition 'positive_result'
- ensures positive_result: \result > 0.
- Unverifiable but considered Valid.
-[ Extern ] Assigns nothing
- assigns \nothing;
- Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 326)
- assigns \result \from x;
- Unverifiable but considered Valid.
-[ Valid ] Default behavior
- default behavior
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'expf'
---------------------------------------------------------------------------------
-
-[ Extern ] Post-condition 'res_finite'
- ensures res_finite: \is_finite(\result)
- Unverifiable but considered Valid.
-[ Extern ] Post-condition 'positive_result'
- ensures positive_result: \result > 0.
- Unverifiable but considered Valid.
-[ Extern ] Assigns nothing
- assigns \nothing;
- Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 334)
- assigns \result \from x;
- Unverifiable but considered Valid.
-[ Valid ] Default behavior
- default behavior
+[ Valid ] Behavior 'underflow'
+ behavior underflow
by Frama-C kernel.
--------------------------------------------------------------------------------
@@ -2945,10 +2968,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 364)
+[ Extern ] Froms (file share/libc/math.h, line 673)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2962,10 +2988,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 371)
+[ Extern ] Froms (file share/libc/math.h, line 704)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2979,10 +3008,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 378)
+[ Extern ] Froms (file share/libc/math.h, line 735)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2996,10 +3028,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 385)
+[ Extern ] Froms (file share/libc/math.h, line 766)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3013,10 +3048,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 392)
+[ Extern ] Froms (file share/libc/math.h, line 797)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3030,10 +3068,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 399)
+[ Extern ] Froms (file share/libc/math.h, line 828)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3047,10 +3088,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 410)
+[ Extern ] Froms (file share/libc/math.h, line 863)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3064,10 +3108,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 417)
+[ Extern ] Froms (file share/libc/math.h, line 894)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3081,10 +3128,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 424)
+[ Extern ] Froms (file share/libc/math.h, line 925)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3109,7 +3159,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 450)
+[ Extern ] Froms (file share/libc/math.h, line 972)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3134,7 +3184,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 458)
+[ Extern ] Froms (file share/libc/math.h, line 990)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3159,7 +3209,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 466)
+[ Extern ] Froms (file share/libc/math.h, line 1008)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3173,10 +3223,17 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
-[ Extern ] Assigns nothing
- assigns \nothing;
+[ Extern ] Post-condition '__fc_errno'
+ ensures
+ __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 479)
+[ Extern ] Assigns (file share/libc/math.h, line 1030)
+ assigns __fc_errno, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 1030)
+ assigns __fc_errno \from x, y;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 1030)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3190,10 +3247,17 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
-[ Extern ] Assigns nothing
- assigns \nothing;
+[ Extern ] Post-condition '__fc_errno'
+ ensures
+ __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 1045)
+ assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 486)
+[ Extern ] Froms (file share/libc/math.h, line 1045)
+ assigns __fc_errno \from x, y;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 1045)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3219,10 +3283,13 @@
[ Extern ] Post-condition 'result_value'
ensures result_value: \result ≡ sqrt(\old(x))
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 495)
+[ Extern ] Froms (file share/libc/math.h, line 1066)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3240,12 +3307,15 @@
ensures positive_result: \result ≥ -0.
Unverifiable but considered Valid.
[ Extern ] Post-condition 'result_value'
- ensures result_value: \result ≡ sqrtf(\old(x))
+ ensures result_value: \result ≡ sqrt((double)\old(x))
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 504)
+[ Extern ] Froms (file share/libc/math.h, line 1095)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3262,10 +3332,13 @@
[ Extern ] Post-condition 'positive_result'
ensures positive_result: \result ≥ -0.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 513)
+[ Extern ] Froms (file share/libc/math.h, line 1124)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3282,7 +3355,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 536)
+[ Extern ] Froms (file share/libc/math.h, line 1164)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3299,7 +3372,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 542)
+[ Extern ] Froms (file share/libc/math.h, line 1181)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3316,7 +3389,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 549)
+[ Extern ] Froms (file share/libc/math.h, line 1198)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3333,7 +3406,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 555)
+[ Extern ] Froms (file share/libc/math.h, line 1215)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3350,7 +3423,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 561)
+[ Extern ] Froms (file share/libc/math.h, line 1232)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3367,7 +3440,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 567)
+[ Extern ] Froms (file share/libc/math.h, line 1249)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3384,7 +3457,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 589)
+[ Extern ] Froms (file share/libc/math.h, line 1282)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3401,7 +3474,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 595)
+[ Extern ] Froms (file share/libc/math.h, line 1299)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3418,7 +3491,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 601)
+[ Extern ] Froms (file share/libc/math.h, line 1316)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3435,7 +3508,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 615)
+[ Extern ] Froms (file share/libc/math.h, line 1341)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3452,7 +3525,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 621)
+[ Extern ] Froms (file share/libc/math.h, line 1358)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3469,7 +3542,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 627)
+[ Extern ] Froms (file share/libc/math.h, line 1375)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3483,10 +3556,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 634)
+[ Extern ] Froms (file share/libc/math.h, line 1395)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3500,10 +3576,13 @@
[ Extern ] Post-condition 'finite_result'
ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 641)
+[ Extern ] Froms (file share/libc/math.h, line 1416)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3520,7 +3599,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 662)
+[ Extern ] Froms (file share/libc/math.h, line 1449)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3537,7 +3616,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 669)
+[ Extern ] Froms (file share/libc/math.h, line 1456)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3554,7 +3633,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 676)
+[ Extern ] Froms (file share/libc/math.h, line 1463)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3574,7 +3653,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 706)
+[ Extern ] Froms (file share/libc/math.h, line 1493)
assigns \result \from f;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3600,7 +3679,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 719)
+[ Extern ] Froms (file share/libc/math.h, line 1506)
assigns \result \from d;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3623,7 +3702,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 746)
+[ Extern ] Froms (file share/libc/math.h, line 1533)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3640,7 +3719,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 752)
+[ Extern ] Froms (file share/libc/math.h, line 1539)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4002,9 +4081,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 175 Completely validated
+ 173 Completely validated
16 Locally validated
- 462 Considered valid
+ 488 Considered valid
56 To be validated
- 709 Total
+ 733 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 5ba9d6cd179e271e66d7029f2bbe88fa4b466efe..78e6ae2ca53e3ceb5a196176ee438cf604d5cd7e 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
+[kernel] :0: Warning: unnamed requires
[kernel] share/libc/sys/socket.h:451: Warning:
clause with '\initialized' must contain name 'initialization'
[eva] Analyzing a complete application starting at main
@@ -43,7 +44,7 @@
wcscpy (0 call); wcsdup (0 call); wcslen (3 calls); wcsncat (0 call);
wcsncpy (0 call); wmemcpy (1 call); wmemset (0 call);
- Specified-only functions (414)
+ Specified-only functions (415)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -77,10 +78,10 @@
acoshf (0 call); acoshl (0 call); acosl (0 call); alloca (0 call);
asctime (0 call); asin (0 call); asinf (0 call); asinl (0 call);
at_quick_exit (0 call); atan (0 call); atan2 (0 call); atan2f (0 call);
- atanf (0 call); atanl (0 call); atexit (0 call); atof (0 call);
- atol (0 call); atoll (0 call); basename (0 call); bind (0 call);
- bsearch (0 call); bzero (0 call); ceil (0 call); ceilf (0 call);
- ceill (0 call); cfgetispeed (0 call); cfgetospeed (0 call);
+ atan2l (0 call); atanf (0 call); atanl (0 call); atexit (0 call);
+ atof (0 call); atol (0 call); atoll (0 call); basename (0 call);
+ bind (0 call); bsearch (0 call); bzero (0 call); ceil (0 call);
+ ceilf (0 call); ceill (0 call); cfgetispeed (0 call); cfgetospeed (0 call);
cfsetispeed (0 call); cfsetospeed (0 call); chdir (0 call); chown (0 call);
chroot (0 call); clearerr (0 call); clearerr_unlocked (0 call);
clock (0 call); clock_gettime (0 call); clock_nanosleep (0 call);
@@ -195,7 +196,7 @@
Goto = 98
Assignment = 465
Exit point = 84
- Function = 499
+ Function = 500
Function call = 96
Pointer dereferencing = 159
Cyclomatic complexity = 298
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index fd785f066330f5aec494ac26657707f3754da401..8390d1842cfd8015387e9f05d813f988f2e0609b 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2841,6 +2841,7 @@ int __fc_fpclassify(double x);
/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -2848,6 +2849,7 @@ extern double acos(double x);
/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -2855,6 +2857,7 @@ extern float acosf(float x);
/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -2862,6 +2865,7 @@ extern long double acosl(long double x);
/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -2869,6 +2873,7 @@ extern double asin(double x);
/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -2876,12 +2881,13 @@ extern float asinf(float x);
/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
extern long double asinl(long double x);
-/*@ requires finite_arg: \is_finite(x);
+/*@ requires finite_arg: ¬\is_NaN(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1.571 ≤ \result ≤ 1.571;
assigns \result;
@@ -2889,7 +2895,7 @@ extern long double asinl(long double x);
*/
extern float atanf(float x);
-/*@ requires finite_arg: \is_finite(x);
+/*@ requires number_arg: ¬\is_NaN(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1.571 ≤ \result ≤ 1.571;
assigns \result;
@@ -2897,7 +2903,7 @@ extern float atanf(float x);
*/
extern double atan(double x);
-/*@ requires finite_arg: \is_finite(x);
+/*@ requires number_arg: ¬\is_NaN(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1.571 ≤ \result ≤ 1.571;
assigns \result;
@@ -2905,25 +2911,31 @@ extern double atan(double x);
*/
extern long double atanl(long double x);
-/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y);
- requires finite_result: \is_finite(atan2(x, y));
+/*@ requires number_args: ¬\is_NaN(x) ∧ ¬\is_NaN(y);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x, y;
*/
extern double atan2(double y, double x);
-/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y);
- requires finite_logic_result: \is_finite(atan2f(x, y));
+/*@ requires number_args: ¬\is_NaN(x) ∧ ¬\is_NaN(y);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x, y;
*/
extern float atan2f(float y, float x);
+/*@ requires number_args: ¬\is_NaN(x) ∧ ¬\is_NaN(y);
+ ensures finite_result: \is_finite(\result);
+ assigns \result;
+ assigns \result \from x, y;
+ */
+extern long double atan2l(long double y, long double x);
+
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -2932,6 +2944,7 @@ extern double cos(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -2940,6 +2953,7 @@ extern float cosf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -2948,6 +2962,7 @@ extern long double cosl(long double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -2956,6 +2971,7 @@ extern double sin(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -2964,116 +2980,107 @@ extern float sinf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
extern long double sinl(long double x);
-/*@ assigns __fc_errno, \result;
- assigns __fc_errno \from x;
+/*@ requires in_domain: \is_finite(x) ∧ x ≥ 1;
+ ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
+ assigns \result;
assigns \result \from x;
-
- behavior normal:
- assumes in_domain: \is_finite(x) ∧ x ≥ 1;
- ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
- assigns \result;
- assigns \result \from x;
-
- behavior infinite:
- assumes is_plus_infinity: \is_plus_infinity(x);
- ensures result_plus_infinity: \is_plus_infinity(\result);
- assigns \result;
- assigns \result \from x;
-
- behavior domain_error:
- assumes
- out_of_domain: \is_minus_infinity(x) ∨ (\is_finite(x) ∧ x < 1);
- ensures errno_set: __fc_errno ≡ 1;
- assigns __fc_errno, \result;
- assigns __fc_errno \from x;
- assigns \result \from x;
-
- disjoint behaviors domain_error, infinite, normal;
*/
extern double acosh(double x);
-/*@ assigns __fc_errno, \result;
+/*@ requires in_domain: \is_finite(x) ∧ x ≥ 1;
+ ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
+ assigns \result;
+ assigns \result \from x;
+ */
+extern float acoshf(float x);
+
+/*@ requires in_domain: \is_finite(x) ∧ x ≥ 1;
+ ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
+ assigns \result;
+ assigns \result \from x;
+ */
+extern long double acoshl(long double x);
+
+/*@ requires ¬(overflow_arg: \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9);
+ requires ¬(plus_infinity_arg: \is_plus_infinity(x));
+ requires ¬(nan_arg: \is_NaN(x));
+ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
- assumes in_domain: \is_finite(x) ∧ x ≥ 1;
- ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+ assumes finite_arg: \is_finite(x);
+ assumes
+ domain_arg: x ≥ -0x1.74910d52d3051p9 ∧ x ≤ 0x1.62e42fefa39efp+9;
+ ensures res_finite: \is_finite(\result);
+ ensures positive_result: \result > 0.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
- behavior infinite:
- assumes is_plus_infinity: \is_plus_infinity(x);
- ensures result_plus_infinity: \is_plus_infinity(\result);
- assigns \result;
- assigns \result \from x;
+ behavior underflow:
+ assumes underflow_arg: \is_finite(x) ∧ x < -0x1.74910d52d3051p9;
+ ensures zero_res: \result ≡ 0.;
+ ensures errno_set: __fc_errno ≡ 34;
- behavior domain_error:
- assumes
- out_of_domain: \is_minus_infinity(x) ∨ (\is_finite(x) ∧ x < 1);
- ensures errno_set: __fc_errno ≡ 1;
- assigns __fc_errno, \result;
- assigns __fc_errno \from x;
+ behavior minus_infinity:
+ assumes plus_infinity_arg: \is_minus_infinity(x);
+ ensures zero_result: \is_finite(\result) ∧ \result ≡ 0.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
+ assigns \result;
assigns \result \from x;
- disjoint behaviors domain_error, infinite, normal;
+ complete behaviors minus_infinity, underflow, normal;
+ disjoint behaviors minus_infinity, underflow, normal;
*/
-extern float acoshf(float x);
+extern double exp(double x);
-/*@ assigns __fc_errno, \result;
+/*@ requires ¬(overflow_arg: \is_finite(x) ∧ x > 0x1.62e42ep+6);
+ requires ¬(plus_infinity_arg: \is_plus_infinity(x));
+ requires ¬(nan_arg: \is_NaN(x));
+ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
- assumes in_domain: \is_finite(x) ∧ x ≥ 1;
- ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+ assumes finite_arg: \is_finite(x);
+ assumes domain_arg: x ≥ -0x1.9fe368p6 ∧ x ≤ 0x1.62e42ep+6;
+ ensures res_finite: \is_finite(\result);
+ ensures positive_result: \result > 0.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
- behavior infinite:
- assumes is_plus_infinity: \is_plus_infinity(x);
- ensures result_plus_infinity: \is_plus_infinity(\result);
- assigns \result;
- assigns \result \from x;
+ behavior underflow:
+ assumes underflow_arg: \is_finite(x) ∧ x < -0x1.9fe368p6;
+ ensures zero_res: \result ≡ 0.;
+ ensures errno_set: __fc_errno ≡ 34;
- behavior domain_error:
- assumes
- out_of_domain: \is_minus_infinity(x) ∨ (\is_finite(x) ∧ x < 1);
- ensures errno_set: __fc_errno ≡ 1;
- assigns __fc_errno, \result;
- assigns __fc_errno \from x;
+ behavior minus_infinity:
+ assumes plus_infinity_arg: \is_minus_infinity(x);
+ ensures zero_result: \is_finite(\result) ∧ \result ≡ 0.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
+ assigns \result;
assigns \result \from x;
- disjoint behaviors domain_error, infinite, normal;
- */
-extern long double acoshl(long double x);
-
-/*@ requires finite_arg: \is_finite(x);
- requires finite_domain: x ≤ 0x1.62e42fefa39efp+9;
- ensures res_finite: \is_finite(\result);
- ensures positive_result: \result > 0.;
- assigns \result;
- assigns \result \from x;
- */
-extern double exp(double x);
-
-/*@ requires finite_arg: \is_finite(x);
- requires res_finite: x ≤ 0x1.62e42ep+6;
- ensures res_finite: \is_finite(\result);
- ensures positive_result: \result > 0.;
- assigns \result;
- assigns \result \from x;
+ complete behaviors minus_infinity, underflow, normal;
+ disjoint behaviors minus_infinity, underflow, normal;
*/
extern float expf(float x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -3082,14 +3089,16 @@ extern double log(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
extern float logf(float x);
/*@ requires finite_arg: \is_finite(x);
- requires arg_pos: x > 0;
+ requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -3098,6 +3107,7 @@ extern long double logl(long double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -3106,14 +3116,16 @@ extern double log10(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
extern float log10f(float x);
/*@ requires finite_arg: \is_finite(x);
- requires arg_postive: x > 0;
+ requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -3122,6 +3134,7 @@ extern long double log10l(long double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -3130,6 +3143,7 @@ extern double log2(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -3138,6 +3152,7 @@ extern float log2f(float x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -3157,18 +3172,22 @@ float fabsf(float x);
*/
extern long double fabsl(long double x);
-/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y);
- requires finite_logic_res: \is_finite(pow(x, y));
+/*@ requires finite_logic_res: \is_finite(pow(x, y));
ensures finite_result: \is_finite(\result);
- assigns \result;
+ ensures
+ __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno);
+ assigns __fc_errno, \result;
+ assigns __fc_errno \from x, y;
assigns \result \from x, y;
*/
extern double pow(double x, double y);
-/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y);
- requires finite_logic_res: \is_finite(powf(x, y));
+/*@ requires finite_logic_res: \is_finite(pow((double)x, (double)y));
ensures finite_result: \is_finite(\result);
- assigns \result;
+ ensures
+ __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno);
+ assigns __fc_errno, \result;
+ assigns __fc_errno \from x, y;
assigns \result \from x, y;
*/
extern float powf(float x, float y);
@@ -3178,6 +3197,7 @@ extern float powf(float x, float y);
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
ensures result_value: \result ≡ sqrt(\old(x));
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -3187,7 +3207,8 @@ extern double sqrt(double x);
requires arg_positive: x ≥ -0.;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
- ensures result_value: \result ≡ sqrtf(\old(x));
+ ensures result_value: \result ≡ sqrt((double)\old(x));
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -3197,6 +3218,7 @@ extern float sqrtf(float x);
requires arg_positive: x ≥ -0.;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x;
*/
@@ -3286,17 +3308,17 @@ extern float truncf(float x);
*/
extern long double truncl(long double x);
-/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y);
- requires finite_logic_result: \is_finite(fmod(x, y));
+/*@ requires in_domain: ¬\is_NaN(x) ∧ ¬\is_NaN(y) ∧ y ≢ 0.;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x, y;
*/
extern double fmod(double x, double y);
-/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y);
- requires finite_logic_result: \is_finite(fmodf(x, y));
+/*@ requires in_domain: ¬\is_NaN(x) ∧ ¬\is_NaN(y) ∧ y ≢ 0.;
ensures finite_result: \is_finite(\result);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
assigns \result;
assigns \result \from x, y;
*/
diff --git a/tests/libc/oracle/math_h.res.oracle b/tests/libc/oracle/math_h.res.oracle
index fa3503020a02b12db820f3c973b3e78ca640f169..3f3ed25684677cafeb46616a83e637e1f039b2d2 100644
--- a/tests/libc/oracle/math_h.res.oracle
+++ b/tests/libc/oracle/math_h.res.oracle
@@ -30,242 +30,215 @@
fp_ilogb0 ∈ {-2147483648.}
fp_ilogbnan ∈ {-2147483648.}
[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45:
- function atan: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45:
- function atan: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45:
- function atan: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45:
- function atan: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45:
- function atan: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45:
- function atan: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45:
- function atan: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45:
- function atan: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva:alarm] tests/libc/math_h.c:45: Warning:
- function atan: precondition 'finite_arg' got status unknown.
[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46:
- function atanf: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46:
- function atanf: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46:
- function atanf: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46:
- function atanf: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46:
- function atanf: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46:
- function atanf: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46:
- function atanf: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46:
- function atanf: precondition 'finite_arg' got status valid.
[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva:alarm] tests/libc/math_h.c:46: Warning:
- function atanf: precondition 'finite_arg' got status unknown.
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
[eva] using specification for function atanl
-[eva] tests/libc/math_h.c:47:
- function atanl: precondition 'finite_arg' got status valid.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
-[eva] tests/libc/math_h.c:47:
- function atanl: precondition 'finite_arg' got status valid.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
-[eva] tests/libc/math_h.c:47:
- function atanl: precondition 'finite_arg' got status valid.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
-[eva] tests/libc/math_h.c:47:
- function atanl: precondition 'finite_arg' got status valid.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
-[eva] tests/libc/math_h.c:47:
- function atanl: precondition 'finite_arg' got status valid.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
-[eva] tests/libc/math_h.c:47:
- function atanl: precondition 'finite_arg' got status valid.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
-[eva] tests/libc/math_h.c:47:
- function atanl: precondition 'finite_arg' got status valid.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
-[eva] tests/libc/math_h.c:47:
- function atanl: precondition 'finite_arg' got status valid.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
Called from tests/libc/math_h.c:47.
-[eva:alarm] tests/libc/math_h.c:47: Warning:
- function atanl: precondition 'finite_arg' got status unknown.
[eva] Done for function atanl
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
[eva] using specification for function fabs
-[eva] tests/libc/math_h.c:48:
- function fabs: precondition 'finite_arg' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
-[eva] tests/libc/math_h.c:48:
- function fabs: precondition 'finite_arg' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
-[eva] tests/libc/math_h.c:48:
- function fabs: precondition 'finite_arg' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
-[eva] tests/libc/math_h.c:48:
- function fabs: precondition 'finite_arg' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
-[eva] tests/libc/math_h.c:48:
- function fabs: precondition 'finite_arg' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
-[eva] tests/libc/math_h.c:48:
- function fabs: precondition 'finite_arg' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
-[eva] tests/libc/math_h.c:48:
- function fabs: precondition 'finite_arg' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
-[eva] tests/libc/math_h.c:48:
- function fabs: precondition 'finite_arg' got status valid.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
Called from tests/libc/math_h.c:48.
-[eva:alarm] tests/libc/math_h.c:48: Warning:
- function fabs: precondition 'finite_arg' got status unknown.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:48.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:48.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:48.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:48.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:48.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:48.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:48.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:48.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:48.
[eva] Done for function fabs
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
[eva] using specification for function fabsf
-[eva] tests/libc/math_h.c:49:
- function fabsf: precondition 'finite_arg' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
-[eva] tests/libc/math_h.c:49:
- function fabsf: precondition 'finite_arg' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
-[eva] tests/libc/math_h.c:49:
- function fabsf: precondition 'finite_arg' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
-[eva] tests/libc/math_h.c:49:
- function fabsf: precondition 'finite_arg' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
-[eva] tests/libc/math_h.c:49:
- function fabsf: precondition 'finite_arg' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
-[eva] tests/libc/math_h.c:49:
- function fabsf: precondition 'finite_arg' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
-[eva] tests/libc/math_h.c:49:
- function fabsf: precondition 'finite_arg' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
-[eva] tests/libc/math_h.c:49:
- function fabsf: precondition 'finite_arg' got status valid.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
Called from tests/libc/math_h.c:49.
-[eva:alarm] tests/libc/math_h.c:49: Warning:
- function fabsf: precondition 'finite_arg' got status unknown.
[eva] Done for function fabsf
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
[eva] using specification for function fabsl
-[eva] tests/libc/math_h.c:50:
- function fabsl: precondition 'finite_arg' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
-[eva] tests/libc/math_h.c:50:
- function fabsl: precondition 'finite_arg' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
-[eva] tests/libc/math_h.c:50:
- function fabsl: precondition 'finite_arg' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
-[eva] tests/libc/math_h.c:50:
- function fabsl: precondition 'finite_arg' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
-[eva] tests/libc/math_h.c:50:
- function fabsl: precondition 'finite_arg' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
-[eva] tests/libc/math_h.c:50:
- function fabsl: precondition 'finite_arg' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
-[eva] tests/libc/math_h.c:50:
- function fabsl: precondition 'finite_arg' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
-[eva] tests/libc/math_h.c:50:
- function fabsl: precondition 'finite_arg' got status valid.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
Called from tests/libc/math_h.c:50.
-[eva:alarm] tests/libc/math_h.c:50: Warning:
- function fabsl: precondition 'finite_arg' got status unknown.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabsl
[eva] computing for function __finite <- main.
Called from tests/libc/math_h.c:54.
@@ -332,7 +305,7 @@
atanl_one ∈ [-inf .. inf]
atanl_minus_one ∈ [-inf .. inf]
atanl_large ∈ [-inf .. inf]
- atanl_ld_top ∈ [-inf .. inf]
+ atanl_ld_top ∈ [-inf .. inf] ∪ {NaN}
fabs_pi ∈ {3.14159265359}
fabs_half_pi ∈ {1.57079632679}
fabs_e ∈ {2.71828182846}
@@ -341,7 +314,7 @@
fabs_one ∈ {1.}
fabs_minus_one ∈ {1.}
fabs_large ∈ {1e+38}
- fabs_top ∈ [-0. .. 1.79769313486e+308]
+ fabs_top ∈ [-0. .. inf] ∪ {NaN}
fabsf_f_pi ∈ {3.14159274101}
fabsf_f_half_pi ∈ {1.57079637051}
fabsf_f_e ∈ {2.71828174591}
@@ -350,7 +323,7 @@
fabsf_one ∈ {1.}
fabsf_minus_one ∈ {1.}
fabsf_large ∈ {9.99999968029e+37}
- fabsf_f_top ∈ [-0. .. 3.40282346639e+38]
+ fabsf_f_top ∈ [-0. .. inf] ∪ {NaN}
fabsl_ld_pi ∈ [-inf .. inf]
fabsl_ld_half_pi ∈ [-inf .. inf]
fabsl_ld_e ∈ [-inf .. inf]
@@ -359,6 +332,6 @@
fabsl_one ∈ [-inf .. inf]
fabsl_minus_one ∈ [-inf .. inf]
fabsl_large ∈ [-inf .. inf]
- fabsl_ld_top ∈ [-inf .. inf]
+ fabsl_ld_top ∈ [-inf .. inf] ∪ {NaN}
r ∈ {0}
__retres ∈ {0}