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