From aa730d2f8c032f2cd841c5426b686b27677d32b0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 29 Sep 2021 09:23:10 +0200
Subject: [PATCH] [kernel] Special float contract: always generates requires
clauses with a name.
---
.../contract_special_float.ml | 23 +++---
tests/float/oracle/builtins.res.oracle | 43 +++++-----
.../contract_special_float.0.res.oracle | 20 ++---
.../contract_special_float.1.res.oracle | 24 ++----
tests/float/oracle/math_builtins.res.oracle | 78 ++++++++-----------
tests/libc/oracle/fc_libc.0.res.oracle | 1 -
tests/libc/oracle/fc_libc.1.res.oracle | 30 ++++---
7 files changed, 95 insertions(+), 124 deletions(-)
diff --git a/src/kernel_services/ast_transformations/contract_special_float.ml b/src/kernel_services/ast_transformations/contract_special_float.ml
index 8eeaed7dcb1..fa2996946b0 100644
--- a/src/kernel_services/ast_transformations/contract_special_float.ml
+++ b/src/kernel_services/ast_transformations/contract_special_float.ml
@@ -53,6 +53,17 @@ let ensures_special_float = function
| Normal, ip -> is_special_float_pred ip.ip_content.tp_statement
| _ -> false
+let negate_behavior_preconds bhv =
+ let neg_preconds =
+ List.map
+ (fun e -> (Logic_const.pnot (e.ip_content.tp_statement)))
+ (bhv.b_requires @ bhv.b_assumes)
+ in
+ let pred = Logic_const.pors neg_preconds in
+ let name = "not_" ^ bhv.b_name in
+ let pred = { pred with pred_name = name :: pred.pred_name } in
+ Logic_const.new_predicate pred
+
let are_complete_disjoint spec behaviors =
match spec.spec_complete_behaviors, spec.spec_disjoint_behaviors with
| [complete], [disjoint] ->
@@ -96,17 +107,7 @@ let update_spec spec =
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 requires = List.map negate_behavior_preconds disabled in
let default =
match default with
| None -> Cil.mk_behavior ~requires ()
diff --git a/tests/float/oracle/builtins.res.oracle b/tests/float/oracle/builtins.res.oracle
index e6023b3d1ca..bc6ed7b1cda 100644
--- a/tests/float/oracle/builtins.res.oracle
+++ b/tests/float/oracle/builtins.res.oracle
@@ -99,46 +99,40 @@
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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+ function exp: precondition 'not_overflow' got status valid.
[eva] tests/float/builtins.c:85:
- function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function exp: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/builtins.c:85:
- function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: precondition 'not_nan' got status valid.
[eva] tests/float/builtins.c:88: Call to builtin exp
[eva] tests/float/builtins.c:88:
- function exp: precondition ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+ function exp: precondition 'not_overflow' got status valid.
[eva] tests/float/builtins.c:88:
- function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function exp: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/builtins.c:88:
- function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: precondition 'not_nan' got status valid.
[eva] tests/float/builtins.c:91: Call to builtin exp
[eva] tests/float/builtins.c:91:
- function exp: precondition ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+ function exp: precondition 'not_overflow' got status valid.
[eva] tests/float/builtins.c:91:
- function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function exp: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/builtins.c:91:
- function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: precondition 'not_nan' 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:alarm] tests/float/builtins.c:95: Warning:
- function exp: precondition ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status unknown.
+ function exp: precondition 'not_overflow' got status unknown.
[eva] tests/float/builtins.c:95:
- function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function exp: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/builtins.c:95:
- function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: precondition 'not_nan' got status valid.
[eva] tests/float/builtins.c:98: Call to builtin exp
[eva:alarm] tests/float/builtins.c:98: Warning:
- function exp: precondition ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status invalid.
+ function exp: precondition 'not_overflow' 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.
+ function exp: no state left, precondition 'not_plus_infinity' got status valid.
[eva] tests/float/builtins.c:98:
- function exp: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: no state left, precondition 'not_nan' 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.
@@ -147,12 +141,11 @@
[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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+ function exp: precondition 'not_overflow' got status valid.
[eva] tests/float/builtins.c:104:
- function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function exp: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/builtins.c:104:
- function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: precondition 'not_nan' 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:
diff --git a/tests/float/oracle/contract_special_float.0.res.oracle b/tests/float/oracle/contract_special_float.0.res.oracle
index c94819b6e7c..6dd5017555a 100644
--- a/tests/float/oracle/contract_special_float.0.res.oracle
+++ b/tests/float/oracle/contract_special_float.0.res.oracle
@@ -26,15 +26,11 @@
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.
+ function fun_no_disjoint: precondition 'not_negative' 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.
+ function fun_no_disjoint: precondition 'not_infinite' got status unknown.
[eva] tests/float/contract_special_float.c:96:
- function fun_no_disjoint: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function fun_no_disjoint: precondition 'not_nan' 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);
@@ -42,15 +38,11 @@
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.
+ function fun_no_complete: precondition 'not_negative' 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.
+ function fun_no_complete: precondition 'not_infinite' got status unknown.
[eva] tests/float/contract_special_float.c:98:
- function fun_no_complete: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function fun_no_complete: precondition 'not_nan' got status valid.
[eva] Done for function fun_no_complete
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/float/oracle/contract_special_float.1.res.oracle b/tests/float/oracle/contract_special_float.1.res.oracle
index 47a549ed310..f3e809bfdfc 100644
--- a/tests/float/oracle/contract_special_float.1.res.oracle
+++ b/tests/float/oracle/contract_special_float.1.res.oracle
@@ -10,11 +10,9 @@
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.
+ function fun: precondition 'not_negative' got status unknown.
[eva] tests/float/contract_special_float.c:92:
- function fun: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function fun: precondition 'not_nan' 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);
@@ -24,11 +22,9 @@
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.
+ function fun_no_default: precondition 'not_negative' got status unknown.
[eva] tests/float/contract_special_float.c:94:
- function fun_no_default: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function fun_no_default: precondition 'not_nan' 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);
@@ -36,11 +32,9 @@
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.
+ function fun_no_disjoint: precondition 'not_negative' got status unknown.
[eva] tests/float/contract_special_float.c:96:
- function fun_no_disjoint: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function fun_no_disjoint: precondition 'not_nan' 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);
@@ -48,11 +42,9 @@
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.
+ function fun_no_complete: precondition 'not_negative' got status unknown.
[eva] tests/float/contract_special_float.c:98:
- function fun_no_complete: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function fun_no_complete: precondition 'not_nan' got status valid.
[eva] Done for function fun_no_complete
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/float/oracle/math_builtins.res.oracle b/tests/float/oracle/math_builtins.res.oracle
index 9a64da6cd76..a940ec4e07c 100644
--- a/tests/float/oracle/math_builtins.res.oracle
+++ b/tests/float/oracle/math_builtins.res.oracle
@@ -1063,58 +1063,51 @@
[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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+ function exp: precondition 'not_overflow' got status valid.
[eva] tests/float/math_builtins.c:516:
- function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function exp: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:516:
- function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: precondition 'not_nan' 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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+ function exp: precondition 'not_overflow' got status valid.
[eva] tests/float/math_builtins.c:517:
- function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function exp: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:517:
- function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: precondition 'not_nan' 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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+ function exp: precondition 'not_overflow' got status valid.
[eva] tests/float/math_builtins.c:518:
- function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function exp: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:518:
- function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: precondition 'not_nan' 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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+ function exp: precondition 'not_overflow' got status valid.
[eva] tests/float/math_builtins.c:519:
- function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function exp: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:519:
- function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: precondition 'not_nan' 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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status valid.
+ function exp: precondition 'not_overflow' got status valid.
[eva] tests/float/math_builtins.c:520:
- function exp: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function exp: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:520:
- function exp: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: precondition 'not_nan' got status valid.
[eva] tests/float/math_builtins.c:521:
Call to builtin Frama_C_exp for function exp
[eva:alarm] tests/float/math_builtins.c:521: Warning:
- function exp: precondition ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9) got status invalid.
+ function exp: precondition 'not_overflow' 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.
+ function exp: no state left, precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:521:
- function exp: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function exp: no state left, precondition 'not_nan' 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.
@@ -1571,48 +1564,43 @@
[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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
+ function expf: precondition 'not_overflow' got status valid.
[eva] tests/float/math_builtins.c:525:
- function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function expf: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:525:
- function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function expf: precondition 'not_nan' 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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
+ function expf: precondition 'not_overflow' got status valid.
[eva] tests/float/math_builtins.c:526:
- function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function expf: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:526:
- function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function expf: precondition 'not_nan' 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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
+ function expf: precondition 'not_overflow' got status valid.
[eva] tests/float/math_builtins.c:527:
- function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function expf: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:527:
- function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function expf: precondition 'not_nan' 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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
+ function expf: precondition 'not_overflow' got status valid.
[eva] tests/float/math_builtins.c:528:
- function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function expf: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:528:
- function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function expf: precondition 'not_nan' 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 ¬(overflow_arg:
- \is_finite(x) ∧ x > 0x1.62e42ep+6) got status valid.
+ function expf: precondition 'not_overflow' got status valid.
[eva] tests/float/math_builtins.c:529:
- function expf: precondition ¬(plus_infinity_arg: \is_plus_infinity(x)) got status valid.
+ function expf: precondition 'not_plus_infinity' got status valid.
[eva] tests/float/math_builtins.c:529:
- function expf: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+ function expf: precondition 'not_nan' 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.
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 28ef97a7b90..e78d1082652 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -206,7 +206,6 @@
Function call = 141
Pointer dereferencing = 249
Cyclomatic complexity = 369
-[kernel] :0: Warning: unnamed requires
[kernel] share/libc/sys/socket.h:451: Warning:
clause with '\initialized' must contain name 'initialization'
/* Generated by Frama-C */
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 9d463988652..6bc8c7e7ed6 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3782,9 +3782,11 @@ extern float acoshf(float 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));
+/*@ requires
+ not_overflow:
+ ¬(overflow_arg: \is_finite(x) ∧ x > 0x1.62e42fefa39efp+9);
+ requires not_plus_infinity: ¬(plus_infinity_arg: \is_plus_infinity(x));
+ requires not_nan: ¬(nan_arg: \is_NaN(x));
assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
@@ -3816,9 +3818,10 @@ extern long double acoshl(long double x);
*/
extern double exp(double x);
-/*@ requires ¬(overflow_arg: \is_finite(x) ∧ x > 0x1.62e42ep+6);
- requires ¬(plus_infinity_arg: \is_plus_infinity(x));
- requires ¬(nan_arg: \is_NaN(x));
+/*@ requires
+ not_overflow: ¬(overflow_arg: \is_finite(x) ∧ x > 0x1.62e42ep+6);
+ requires not_plus_infinity: ¬(plus_infinity_arg: \is_plus_infinity(x));
+ requires not_nan: ¬(nan_arg: \is_NaN(x));
assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
@@ -3851,8 +3854,9 @@ extern float expf(float x);
/*@ requires valid_exp: \valid(exp);
requires
- ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
- requires ¬(nan_arg: \is_NaN(x));
+ not_infinite:
+ ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
+ requires not_nan: ¬(nan_arg: \is_NaN(x));
assigns \result, *exp;
assigns \result \from x;
assigns *exp \from x;
@@ -3878,8 +3882,9 @@ extern double frexp(double x, int *exp);
/*@ requires valid_exp: \valid(exp);
requires
- ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
- requires ¬(nan_arg: \is_NaN(x));
+ not_infinite:
+ ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
+ requires not_nan: ¬(nan_arg: \is_NaN(x));
assigns \result, *exp;
assigns \result \from x;
assigns *exp \from x;
@@ -3905,8 +3910,9 @@ extern float frexpf(float x, int *exp);
/*@ requires valid_exp: \valid(exp);
requires
- ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
- requires ¬(nan_arg: \is_NaN(x));
+ not_infinite:
+ ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
+ requires not_nan: ¬(nan_arg: \is_NaN(x));
assigns \result, *exp;
assigns \result \from x;
assigns *exp \from x;
--
GitLab