incompatibilité de libc/math.h ??
ID0002491:
**This issue was created automatically from Mantis Issue 2491. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002491 | Frama-C | Plug-in > clang | public | 2020-01-22 | 2020-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nicky | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
l'instruction
#include <math.h>
provoque les messages d'erreur:
/usr/local/share/frama-c/libc/math.h:134:40: unknown identifier '\is_infinite'
/usr/local/share/frama-c/libc/math.h:148:40: unknown identifier '\is_infinite'
/usr/local/share/frama-c/libc/math.h:158:38: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:176:40: unknown identifier '\is_infinite'
/usr/local/share/frama-c/libc/math.h:190:40: unknown identifier '\is_infinite'
/usr/local/share/frama-c/libc/math.h:200:38: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:225:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:233:45: calls to C++ functions/methods like 'atan2' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:240:52: calls to C++ functions/methods like 'atan2f' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:262:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:283:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:301:48: unknown identifier '\is_plus_infinity'
/usr/local/share/frama-c/libc/math.h:319:48: unknown identifier '\is_plus_infinity'
/usr/local/share/frama-c/libc/math.h:333:38: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:420:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:441:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:466:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:509:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:522:46: calls to C++ functions/methods like 'pow' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:529:47: calls to C++ functions/methods like 'powf' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:553:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:590:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:608:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:642:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:668:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:675:50: calls to C++ functions/methods like 'fmod' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:682:51: calls to C++ functions/methods like 'fmodf' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:719:42: No suitable candidate found for function \is_NaN.
/usr/local/share/frama-c/libc/math.h:759:56: unknown identifier '\plus_infinity'
/usr/local/share/frama-c/libc/math.h:765:48: unknown identifier '\is_plus_infinity'
### Additional Information :
parsing partiellement réussi, voici op_test_math:
[kernel] Parsing test_math.cpp (external front-end)
Now output intermediate result
/* Generated by Frama-C */
/*@
axiomatic MemCmp {
logic ℤ memcmp{L1, L2}(char *s1, char *s2, ℤ n)
reads \at(*(s1 + (0 .. n - 1)),L1), \at(*(s2 + (0 .. n - 1)),L2);
axiom memcmp_zero{L1, L2}:
∀ char *s1, char *s2;
∀ ℤ n;
memcmp{L1, L2}(s1, s2, n) ≡ 0 ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ \at(*(s1 + i),L1) ≡ \at(*(s2 + i),L2));
}
*/
/*@
axiomatic MemChr {
logic 𝔹 memchr{L}(char *s, ℤ c, ℤ n)
reads *(s + (0 .. n - 1));
logic ℤ memchr_off{L}(char *s, ℤ c, ℤ n)
reads *(s + (0 .. n - 1));
axiom memchr_def{L}:
∀ char *s;
∀ ℤ c;
∀ ℤ n;
memchr(s, c, n) ≢ (0 ≢ 0) ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
*/
/*@
axiomatic MemSet {
logic 𝔹 memset{L}(char *s, ℤ c, ℤ n)
reads *(s + (0 .. n - 1));
axiom memset_def{L}:
∀ char *s;
∀ ℤ c;
∀ ℤ n;
memset(s, c, n) ≢ (0 ≢ 0) ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
*/
/*@
axiomatic StrLen {
logic ℤ strlen{L}(char *s)
reads *(s + (0 ..));
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
*(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
(∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
axiom strlen_at_null{L}:
∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i ≤ strlen(s) ⇒ strlen(s + i) ≡ strlen(s) - i;
axiom strlen_create{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
∀ ℤ n;
memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s1) < n ⇒
strlen(s1) ≡ strlen(s2);
axiom memcmp_strlen_right{L}:
∀ char *s1, char *s2;
∀ ℤ n;
memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s2) < n ⇒
strlen(s1) ≡ strlen(s2);
axiom memcmp_strlen_shift_left{L}:
∀ char *s1, char *s2;
∀ ℤ k, ℤ n;
memcmp{L, L}(s1, s2 + k, n) ≡ 0 ≤ k ∧ strlen(s1) < n ⇒
0 ≤ strlen(s2) ≤ k + strlen(s1);
axiom memcmp_strlen_shift_right{L}:
∀ char *s1, char *s2;
∀ ℤ k, ℤ n;
memcmp{L, L}(s1 + k, s2, n) ≡ 0 ≤ k ∧ strlen(s2) < n ⇒
0 ≤ strlen(s1) ≤ k + strlen(s2);
}
*/
/*@
axiomatic StrCmp {
logic ℤ strcmp{L}(char *s1, char *s2)
reads *(s1 + (0 .. strlen(s1))), *(s2 + (0 .. strlen(s2)));
axiom strcmp_zero{L}:
∀ char *s1, char *s2;
strcmp(s1, s2) ≡ 0 ⇔
strlen(s1) ≡ strlen(s2) ∧
(∀ ℤ i; 0 ≤ i ≤ strlen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic StrNCmp {
logic ℤ strncmp{L}(char *s1, char *s2, ℤ n)
reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
axiom strncmp_zero{L}:
∀ char *s1, char *s2;
∀ ℤ n;
strncmp(s1, s2, n) ≡ 0 ⇔
(strlen(s1) < n ∧ strcmp(s1, s2) ≡ 0) ∨
(∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic StrChr {
logic 𝔹 strchr{L}(char *s, ℤ c)
reads *(s + (0 .. strlen(s)));
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
strchr(s, c) ≢ (0 ≢ 0) ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
*/
/*@
axiomatic WMemChr {
logic 𝔹 wmemchr{L}(int *s, int c, ℤ n)
reads *(s + (0 .. n - 1));
logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
reads *(s + (0 .. n - 1));
axiom wmemchr_def{L}:
∀ int *s;
∀ int c;
∀ ℤ n;
wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
*/
/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
axiom wcslen_pos_or_null{L}:
∀ int *s;
∀ ℤ i;
0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (int)0) ∧
*(s + i) ≡ (int)0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
∀ int *s;
(∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (int)0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ int *s;
∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (int)0;
axiom wcslen_at_null{L}:
∀ int *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (int)0;
axiom wcslen_not_zero{L}:
∀ int *s;
∀ int i;
0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (int)0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ int *s;
∀ int i;
0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (int)0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ int *s;
∀ int i; 0 ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ int *s;
∀ int i; 0 ≤ i ≤ wcslen(s) ⇒ wcslen(s + i) ≡ wcslen(s) - i;
axiom wcslen_create{L}:
∀ int *s;
∀ int i; 0 ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ int *s;
∀ int i;
∀ int k;
0 ≤ k ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
/*@
axiomatic WcsCmp {
logic ℤ wcscmp{L}(int *s1, int *s2)
reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
axiom wcscmp_zero{L}:
∀ int *s1, int *s2;
wcscmp(s1, s2) ≡ 0 ⇔
wcslen(s1) ≡ wcslen(s2) ∧
(∀ ℤ i; 0 ≤ i ≤ wcslen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic WcsNCmp {
logic ℤ wcsncmp{L}(int *s1, int *s2, ℤ n)
reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
axiom wcsncmp_zero{L}:
∀ int *s1, int *s2;
∀ ℤ n;
wcsncmp(s1, s2, n) ≡ 0 ⇔
(wcslen(s1) < n ∧ wcscmp(s1, s2) ≡ 0) ∨
(∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic WcsChr {
logic 𝔹 wcschr{L}(int *wcs, ℤ wc)
reads *(wcs + (0 .. wcslen(wcs)));
axiom wcschr_def{L}:
∀ int *wcs;
∀ ℤ wc;
wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
(∃ ℤ i; 0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (int)((int)wc));
}
*/
/*@ logic ℤ minimum(ℤ i, ℤ j) = i < j? i: j;
*/
/*@ logic ℤ maximum(ℤ i, ℤ j) = i < j? j: i;
*/
/*@
predicate valid_string{L}(char *s) =
0 ≤ strlen(s) ∧ \valid(s + (0 .. strlen(s)));
*/
/*@
predicate valid_read_string{L}(char *s) =
0 ≤ strlen(s) ∧ \valid_read(s + (0 .. strlen(s)));
*/
/*@
predicate valid_read_nstring{L}(char *s, ℤ n) =
(\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨
valid_read_string(s);
*/
/*@
predicate valid_string_or_null{L}(char *s) = s ≡ \null ∨ valid_string(s);
*/
/*@
predicate valid_wstring{L}(int *s) =
0 ≤ wcslen(s) ∧ \valid(s + (0 .. wcslen(s)));
*/
/*@
predicate valid_read_wstring{L}(int *s) =
0 ≤ wcslen(s) ∧ \valid_read(s + (0 .. wcslen(s)));
*/
/*@
predicate valid_read_nwstring{L}(int *s, ℤ n) =
(\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨
valid_read_wstring(s);
*/
/*@
predicate valid_wstring_or_null{L}(int *s) =
s ≡ \null ∨ valid_wstring(s);
*/
int __fc_errno;
char *program_invocation_name;
char *program_invocation_short_name;
/*@ assigns \result;
assigns \result \from x;
behavior nan:
assumes is_nan: \is_NaN(x);
ensures fp_nan: \result ≡ 0;
behavior inf:
assumes is_infinite: ¬\is_NaN(x) ∧ ¬\is_finite(x);
ensures fp_infinite: \result ≡ 1;
behavior zero:
assumes is_a_zero: x ≡ 0.0;
ensures fp_zero: \result ≡ 2;
behavior subnormal:
assumes is_finite: \is_finite(x);
assumes
is_subnormal:
(x > 0.0 ∧ x < 0x1p-126) ∨ (x < 0.0 ∧ x > -0x1p-126);
ensures fp_subnormal: \result ≡ 3;
behavior normal:
assumes is_finite: \is_finite(x);
assumes not_subnormal: x ≤ -0x1p-126 ∨ x ≥ 0x1p-126;
ensures fp_normal: \result ≡ 4;
complete behaviors normal, subnormal, zero, inf, nan;
disjoint behaviors normal, subnormal, zero, inf, nan;
*/
int __fc_fpclassifyf(float x);
/*@ assigns \result;
assigns \result \from x;
behavior nan:
assumes is_nan: \is_NaN(x);
ensures fp_nan: \result ≡ 0;
behavior inf:
assumes is_infinite: ¬\is_NaN(x) ∧ ¬\is_finite(x);
ensures fp_infinite: \result ≡ 1;
behavior zero:
assumes is_a_zero: x ≡ 0.0;
ensures fp_zero: \result ≡ 2;
behavior subnormal:
assumes is_finite: \is_finite(x);
assumes
is_subnormal:
(x > 0.0 ∧ x < 0x1p-1022) ∨ (x < 0.0 ∧ x > -0x1p-1022);
ensures fp_subnormal: \result ≡ 3;
behavior normal:
assumes is_finite: \is_finite(x);
assumes not_subnormal: x ≤ -0x1p-1022 ∨ x ≥ 0x1p-1022;
ensures fp_normal: \result ≡ 4;
complete behaviors normal, subnormal, zero, inf, nan;
disjoint behaviors normal, subnormal, zero, inf, nan;
*/
int __fc_fpclassify(double x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
assigns \result;
assigns \result \from x;
behavior domain_error:
*/
double acos(double x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
assigns \result;
assigns \result \from x;
behavior domain_error:
*/
float acosf(float x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
*/
long double acosl(long double x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
behavior domain_error:
*/
double asin(double x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
behavior domain_error:
*/
float asinf(float x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
*/
long double asinl(long double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1.571 ≤ \result ≤ 1.571;
assigns \result;
assigns \result \from x;
*/
float atanf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1.571 ≤ \result ≤ 1.571;
assigns \result;
assigns \result \from x;
*/
double atan(double x);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
double atan2(double y, double x);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
float atan2f(float y, float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
assigns \result;
assigns \result \from x;
*/
double cos(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
assigns \result;
assigns \result \from x;
*/
float cosf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
assigns \result;
assigns \result \from x;
*/
double sin(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
assigns \result;
assigns \result \from x;
*/
float sinf(float 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;
assigns \result;
assigns \result \from x;
behavior infinite:
*/
double acosh(double 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;
assigns \result;
assigns \result \from x;
behavior infinite:
*/
float acoshf(float x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
*/
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;
*/
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;
*/
float expf(float x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double log(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float logf(float x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double log10(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float log10f(float x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double log2(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float log2f(float x);
/*@ requires finite_arg: \is_finite(x);
ensures res_finite: \is_finite(\result);
ensures positive_result: \result ≥ 0.;
ensures
equal_magnitude_result: \result ≡ \old(x) ∨ \result ≡ -\old(x);
assigns \result;
assigns \result \from x;
*/
double fabs(double x);
/*@ requires finite_arg: \is_finite(x);
ensures res_finite: \is_finite(\result);
ensures positive_result: \result ≥ 0.;
ensures
equal_magnitude_result: \result ≡ \old(x) ∨ \result ≡ -\old(x);
assigns \result;
assigns \result \from x;
*/
float fabsf(float x);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
double pow(double x, double y);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
float powf(float x, float y);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x ≥ -0.;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
assigns \result;
assigns \result \from x;
*/
double sqrt(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x ≥ -0.;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
assigns \result;
assigns \result \from x;
*/
float sqrtf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double ceil(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float ceilf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double floor(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float floorf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double round(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float roundf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double trunc(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float truncf(float x);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
double fmod(double x, double y);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
float fmodf(float x, float y);
/*@ requires tagp_valid_string: valid_read_string(tagp);
ensures result_is_nan: \is_NaN(\result);
assigns \result;
assigns \result \from (indirect: *(tagp + (0 ..)));
*/
double nan(char const *tagp);
/*@ requires tagp_valid_string: valid_read_string(tagp);
ensures result_is_nan: \is_NaN(\result);
assigns \result;
assigns \result \from (indirect: *(tagp + (0 ..)));
*/
float nanf(char const *tagp);
/*@ requires tagp_valid_string: valid_read_string(tagp);
assigns \result;
assigns \result \from (indirect: *(tagp + (0 ..)));
*/
long double nanl(char const *tagp);
/*@ ensures result_is_nan: \is_NaN(\result);
assigns \result;
assigns \result \from \nothing;
*/
float __fc_nan(int x);
### Steps To Reproduce :
frama-c test_math.cpp -print > op_test_math
## Attachments
- [test_math.cpp](/uploads/bce7c18e055ca2e12eb308736c0934fb/test_math.cpp)
issue