diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index 18a0e92bcf745d267e58b4a630a8962646e626ed..c44a659ed70c59996a52187b9e77c2f1e8253048 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 526 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc math.h 522 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/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 0f3499f8f38e8e1815a6b7f9bb68d54d3019a961..ace1c0568b9fc422d31f7bfa9b341f94f18c509d 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2161,7 +2161,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 71)
+[ Extern ] Froms (file share/libc/math.h, line 67)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2205,7 +2205,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 95)
+[ Extern ] Froms (file share/libc/math.h, line 91)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2237,28 +2237,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 132)
+[ Extern ] Assigns (file share/libc/math.h, line 128)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 139)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 135)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 132)
+[ Extern ] Froms (file share/libc/math.h, line 128)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 132)
+[ Extern ] Froms (file share/libc/math.h, line 128)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 139)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 135)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 139)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 135)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 135)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 131)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2281,28 +2281,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 146)
+[ Extern ] Assigns (file share/libc/math.h, line 142)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 153)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 149)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 146)
+[ Extern ] Froms (file share/libc/math.h, line 142)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 146)
+[ Extern ] Froms (file share/libc/math.h, line 142)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 153)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 149)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 153)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 149)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 149)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 145)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2325,28 +2325,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 160)
+[ Extern ] Assigns (file share/libc/math.h, line 156)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 167)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 163)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 160)
+[ Extern ] Froms (file share/libc/math.h, line 156)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 160)
+[ Extern ] Froms (file share/libc/math.h, line 156)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 167)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 163)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 167)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 163)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 163)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 159)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2369,28 +2369,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 174)
+[ Extern ] Assigns (file share/libc/math.h, line 170)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 181)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 177)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 174)
+[ Extern ] Froms (file share/libc/math.h, line 170)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 174)
+[ Extern ] Froms (file share/libc/math.h, line 170)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 181)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 177)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 181)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 177)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 177)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 173)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2413,28 +2413,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 188)
+[ Extern ] Assigns (file share/libc/math.h, line 184)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 195)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 191)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 188)
+[ Extern ] Froms (file share/libc/math.h, line 184)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 188)
+[ Extern ] Froms (file share/libc/math.h, line 184)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 195)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 191)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 195)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 191)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 191)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 187)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2457,28 +2457,28 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 202)
+[ Extern ] Assigns (file share/libc/math.h, line 198)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 209)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 205)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 202)
+[ Extern ] Froms (file share/libc/math.h, line 198)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 202)
+[ Extern ] Froms (file share/libc/math.h, line 198)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 209)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 205)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 209)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 205)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 205)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 201)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2504,7 +2504,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 216)
+[ Extern ] Froms (file share/libc/math.h, line 212)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2524,7 +2524,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 223)
+[ Extern ] Froms (file share/libc/math.h, line 219)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2544,7 +2544,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 230)
+[ Extern ] Froms (file share/libc/math.h, line 226)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2561,7 +2561,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 238)
+[ Extern ] Froms (file share/libc/math.h, line 234)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2578,7 +2578,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 245)
+[ Extern ] Froms (file share/libc/math.h, line 241)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2601,7 +2601,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 253)
+[ Extern ] Froms (file share/libc/math.h, line 249)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2621,7 +2621,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 260)
+[ Extern ] Froms (file share/libc/math.h, line 256)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2641,7 +2641,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 267)
+[ Extern ] Froms (file share/libc/math.h, line 263)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2661,7 +2661,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 274)
+[ Extern ] Froms (file share/libc/math.h, line 270)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2681,7 +2681,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 281)
+[ Extern ] Froms (file share/libc/math.h, line 277)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2701,7 +2701,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 288)
+[ Extern ] Froms (file share/libc/math.h, line 284)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2721,10 +2721,10 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 299)
+[ Extern ] Assigns (file share/libc/math.h, line 295)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 310)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 306)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'infinite' nothing
@@ -2733,22 +2733,22 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 299)
+[ Extern ] Froms (file share/libc/math.h, line 295)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 299)
+[ Extern ] Froms (file share/libc/math.h, line 295)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 310)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 306)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 310)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 306)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 306)
+[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 302)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 302)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 298)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2777,10 +2777,10 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 317)
+[ Extern ] Assigns (file share/libc/math.h, line 313)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 328)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 324)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'infinite' nothing
@@ -2789,22 +2789,22 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 317)
+[ Extern ] Froms (file share/libc/math.h, line 313)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 317)
+[ Extern ] Froms (file share/libc/math.h, line 313)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 328)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 324)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 328)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 324)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 324)
+[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 320)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 320)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 316)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2833,10 +2833,10 @@
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 335)
+[ Extern ] Assigns (file share/libc/math.h, line 331)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 346)
+[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 342)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'infinite' nothing
@@ -2845,22 +2845,22 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 335)
+[ Extern ] Froms (file share/libc/math.h, line 331)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 335)
+[ Extern ] Froms (file share/libc/math.h, line 331)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 346)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 342)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 346)
+[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 342)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 342)
+[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 338)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 338)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 334)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2889,7 +2889,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 374)
+[ Extern ] Froms (file share/libc/math.h, line 370)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2909,7 +2909,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 382)
+[ Extern ] Froms (file share/libc/math.h, line 378)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2926,7 +2926,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 412)
+[ Extern ] Froms (file share/libc/math.h, line 408)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2943,7 +2943,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 419)
+[ Extern ] Froms (file share/libc/math.h, line 415)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2960,7 +2960,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 426)
+[ Extern ] Froms (file share/libc/math.h, line 422)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2977,7 +2977,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 433)
+[ Extern ] Froms (file share/libc/math.h, line 429)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2994,7 +2994,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 440)
+[ Extern ] Froms (file share/libc/math.h, line 436)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3011,7 +3011,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 447)
+[ Extern ] Froms (file share/libc/math.h, line 443)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3028,7 +3028,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 454)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3045,7 +3045,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 465)
+[ Extern ] Froms (file share/libc/math.h, line 461)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3062,7 +3062,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 472)
+[ Extern ] Froms (file share/libc/math.h, line 468)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3087,7 +3087,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 498)
+[ Extern ] Froms (file share/libc/math.h, line 494)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3112,7 +3112,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 506)
+[ Extern ] Froms (file share/libc/math.h, line 502)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3137,7 +3137,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 514)
+[ Extern ] Froms (file share/libc/math.h, line 510)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3154,7 +3154,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 527)
+[ Extern ] Froms (file share/libc/math.h, line 523)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3171,7 +3171,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 534)
+[ Extern ] Froms (file share/libc/math.h, line 530)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3197,7 +3197,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 543)
+[ Extern ] Froms (file share/libc/math.h, line 539)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3217,7 +3217,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 551)
+[ Extern ] Froms (file share/libc/math.h, line 547)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3237,7 +3237,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 559)
+[ Extern ] Froms (file share/libc/math.h, line 555)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3254,7 +3254,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 582)
+[ Extern ] Froms (file share/libc/math.h, line 578)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3271,7 +3271,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 588)
+[ Extern ] Froms (file share/libc/math.h, line 584)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3288,7 +3288,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 591)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3305,7 +3305,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 597)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3322,7 +3322,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 607)
+[ Extern ] Froms (file share/libc/math.h, line 603)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3339,7 +3339,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 613)
+[ Extern ] Froms (file share/libc/math.h, line 609)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3356,7 +3356,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 635)
+[ Extern ] Froms (file share/libc/math.h, line 631)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3373,7 +3373,7 @@
[ 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 637)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3390,7 +3390,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 647)
+[ Extern ] Froms (file share/libc/math.h, line 643)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3407,7 +3407,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 661)
+[ Extern ] Froms (file share/libc/math.h, line 657)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3424,7 +3424,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 667)
+[ Extern ] Froms (file share/libc/math.h, line 663)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3441,7 +3441,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 673)
+[ Extern ] Froms (file share/libc/math.h, line 669)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3458,7 +3458,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 680)
+[ Extern ] Froms (file share/libc/math.h, line 676)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3475,7 +3475,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 687)
+[ Extern ] Froms (file share/libc/math.h, line 683)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3492,7 +3492,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 708)
+[ Extern ] Froms (file share/libc/math.h, line 704)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3509,7 +3509,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 715)
+[ Extern ] Froms (file share/libc/math.h, line 711)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3526,13 +3526,47 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 722)
+[ Extern ] Froms (file share/libc/math.h, line 718)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
default behavior
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function '__fc_infinity'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'result_is_infinity'
+ ensures result_is_infinity: \is_plus_infinity(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 766)
+ assigns \result \from \nothing;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function '__fc_nan'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'result_is_nan'
+ ensures result_is_nan: \is_NaN(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 772)
+ assigns \result \from \nothing;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'idct'
--------------------------------------------------------------------------------
@@ -3888,9 +3922,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 173 Completely validated
+ 175 Completely validated
16 Locally validated
- 448 Considered valid
+ 454 Considered valid
56 To be validated
- 693 Total
+ 701 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index d64ea807afda96b59b16bcca76633b124b9864dc..e8cb83c5ada4c1850d6cd7cd3708da2ec16145dc 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -40,7 +40,7 @@
unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
- Undefined functions (382)
+ Undefined functions (384)
=========================
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);
@@ -61,64 +61,64 @@
__builtin_umull_overflow (0 call); __builtin_umulll_overflow (0 call);
__builtin_usub_overflow (0 call); __builtin_usubl_overflow (0 call);
__builtin_usubll_overflow (0 call); __fc_fpclassify (0 call);
- __fc_fpclassifyf (0 call); __va_fcntl_flock (0 call);
- __va_fcntl_int (0 call); __va_fcntl_void (0 call); __va_ioctl_int (0 call);
- __va_ioctl_ptr (0 call); __va_ioctl_void (0 call);
- __va_open_mode_t (0 call); __va_open_void (0 call);
- __va_openat_mode_t (0 call); __va_openat_void (0 call); _exit (0 call);
- abort (0 call); accept (0 call); access (0 call); acos (0 call);
- acosf (0 call); acosh (0 call); acoshf (0 call); acoshl (0 call);
- acosl (0 call); alloca (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); 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);
- close (0 call); closedir (0 call); closelog (0 call); connect (0 call);
- cos (0 call); cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
- difftime (0 call); dirname (0 call); div (0 call); drand48 (0 call);
- dup (0 call); dup2 (0 call); erand48 (0 call); execl (0 call);
- execle (0 call); execlp (0 call); execv (0 call); execve (0 call);
- execvp (0 call); exit (0 call); exp (0 call); expf (0 call); fabsl (0 call);
- fclose (0 call); fcntl (0 call); fdopen (0 call); feof (2 calls);
- feof_unlocked (0 call); ferror (2 calls); ferror_unlocked (0 call);
- fflush (0 call); fgetc (1 call); fgetpos (0 call); fgets (0 call);
- fgetws (0 call); fileno (0 call); fileno_unlocked (0 call); flock (0 call);
- flockfile (0 call); floor (0 call); floorf (0 call); floorl (0 call);
- fmod (0 call); fmodf (0 call); fopen (0 call); fork (0 call);
- fputc (0 call); fputs (0 call); fread (0 call); free (1 call);
- freeaddrinfo (0 call); freopen (0 call); fseek (0 call); fsetpos (0 call);
- ftell (0 call); ftrylockfile (0 call); funlockfile (0 call);
- fwrite (0 call); gai_strerror (0 call); getc (0 call);
- getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
- getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
- gethostname (0 call); getitimer (0 call); getopt (0 call);
- getopt_long (0 call); getopt_long_only (0 call); getpgid (0 call);
- getpgrp (0 call); getpid (0 call); getppid (0 call); getpriority (0 call);
- getpwnam (0 call); getpwuid (0 call); getresgid (0 call);
- getresuid (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
- getsid (0 call); getsockopt (0 call); gettimeofday (0 call);
- getuid (0 call); gmtime (0 call); htonl (0 call); htons (0 call);
- iconv (0 call); iconv_close (0 call); iconv_open (0 call);
- inet_addr (2 calls); inet_ntoa (0 call); inet_ntop (0 call);
- inet_pton (0 call); isascii (0 call); isatty (0 call); jrand48 (0 call);
- kill (0 call); killpg (0 call); labs (0 call); lcong48 (0 call);
- ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
- localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
- log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
- logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
- lseek (0 call); malloc (7 calls); mblen (0 call); mbstowcs (0 call);
- mbtowc (0 call); mkdir (0 call); mkstemp (0 call); mktime (0 call);
- mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
- nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
- open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
- pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
- poll (0 call); popen (0 call); pow (0 call); powf (0 call);
- pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
- pthread_cond_init (0 call); pthread_cond_wait (0 call);
- pthread_create (0 call); pthread_join (0 call);
+ __fc_fpclassifyf (0 call); __fc_infinity (0 call); __fc_nan (0 call);
+ __va_fcntl_flock (0 call); __va_fcntl_int (0 call);
+ __va_fcntl_void (0 call); __va_ioctl_int (0 call); __va_ioctl_ptr (0 call);
+ __va_ioctl_void (0 call); __va_open_mode_t (0 call);
+ __va_open_void (0 call); __va_openat_mode_t (0 call);
+ __va_openat_void (0 call); _exit (0 call); abort (0 call); accept (0 call);
+ access (0 call); acos (0 call); acosf (0 call); acosh (0 call);
+ acoshf (0 call); acoshl (0 call); acosl (0 call); alloca (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);
+ 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); close (0 call); closedir (0 call);
+ closelog (0 call); connect (0 call); cos (0 call); cosf (0 call);
+ cosl (0 call); creat (0 call); ctime (0 call); difftime (0 call);
+ dirname (0 call); div (0 call); drand48 (0 call); dup (0 call);
+ dup2 (0 call); erand48 (0 call); execl (0 call); execle (0 call);
+ execlp (0 call); execv (0 call); execve (0 call); execvp (0 call);
+ exit (0 call); exp (0 call); expf (0 call); fabsl (0 call); fclose (0 call);
+ fcntl (0 call); fdopen (0 call); feof (2 calls); feof_unlocked (0 call);
+ ferror (2 calls); ferror_unlocked (0 call); fflush (0 call); fgetc (1 call);
+ fgetpos (0 call); fgets (0 call); fgetws (0 call); fileno (0 call);
+ fileno_unlocked (0 call); flock (0 call); flockfile (0 call);
+ floor (0 call); floorf (0 call); floorl (0 call); fmod (0 call);
+ fmodf (0 call); fopen (0 call); fork (0 call); fputc (0 call);
+ fputs (0 call); fread (0 call); free (1 call); freeaddrinfo (0 call);
+ freopen (0 call); fseek (0 call); fsetpos (0 call); ftell (0 call);
+ ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call);
+ gai_strerror (0 call); getc (0 call); getc_unlocked (0 call);
+ getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
+ getegid (0 call); geteuid (0 call); getgid (0 call); gethostname (0 call);
+ getitimer (0 call); getopt (0 call); getopt_long (0 call);
+ getopt_long_only (0 call); getpgid (0 call); getpgrp (0 call);
+ getpid (0 call); getppid (0 call); getpriority (0 call); getpwnam (0 call);
+ getpwuid (0 call); getresgid (0 call); getresuid (0 call);
+ getrlimit (0 call); getrusage (0 call); gets (0 call); getsid (0 call);
+ getsockopt (0 call); gettimeofday (0 call); getuid (0 call);
+ gmtime (0 call); htonl (0 call); htons (0 call); iconv (0 call);
+ iconv_close (0 call); iconv_open (0 call); inet_addr (2 calls);
+ inet_ntoa (0 call); inet_ntop (0 call); inet_pton (0 call);
+ isascii (0 call); isatty (0 call); jrand48 (0 call); kill (0 call);
+ killpg (0 call); labs (0 call); lcong48 (0 call); ldiv (0 call);
+ listen (0 call); llabs (0 call); lldiv (0 call); localtime (0 call);
+ log (0 call); log10 (0 call); log10f (0 call); log10l (0 call);
+ log2 (0 call); log2f (0 call); log2l (0 call); logf (0 call); logl (0 call);
+ longjmp (0 call); lrand48 (0 call); lseek (0 call); malloc (7 calls);
+ mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call);
+ mkstemp (0 call); mktime (0 call); mrand48 (0 call); nan (0 call);
+ nanf (0 call); nanl (0 call); nanosleep (0 call); nrand48 (0 call);
+ ntohl (0 call); ntohs (0 call); open (0 call); openat (0 call);
+ opendir (0 call); openlog (0 call); pathconf (0 call); pclose (0 call);
+ perror (0 call); pipe (0 call); poll (0 call); popen (0 call); pow (0 call);
+ powf (0 call); pthread_cond_broadcast (0 call);
+ pthread_cond_destroy (0 call); pthread_cond_init (0 call);
+ pthread_cond_wait (0 call); pthread_create (0 call); pthread_join (0 call);
pthread_mutex_destroy (0 call); pthread_mutex_init (0 call);
pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call); putc (0 call);
putc_unlocked (0 call); putchar (0 call); putchar_unlocked (0 call);
@@ -178,7 +178,7 @@
Goto = 89
Assignment = 438
Exit point = 82
- Function = 464
+ Function = 466
Function call = 89
Pointer dereferencing = 158
Cyclomatic complexity = 286
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index d0942621eceadea65324eea022577dd0fad7f0f9..9e6b3562dc1d9f99de259faf0a8313c2badd1ce0 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3379,6 +3379,23 @@ int __finitef(float f);
int __finite(double d);
+/*@ logic float __fc_infinity(ℤ x) = \plus_infinity;
+ */
+/*@ logic float __fc_nan(ℤ x) = \NaN;
+
+*/
+/*@ ensures result_is_infinity: \is_plus_infinity(\result);
+ assigns \result;
+ assigns \result \from \nothing;
+ */
+extern float __fc_infinity(int x);
+
+/*@ ensures result_is_nan: \is_NaN(\result);
+ assigns \result;
+ assigns \result \from \nothing;
+ */
+extern float __fc_nan(int x);
+
/*@ requires finite_arg: \is_finite(x);
ensures res_finite: \is_finite(\result);
ensures positive_result: \result ≥ 0.;