Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002491Frama-CPlug-in > clangpublic2020-01-22 15:082020-01-23 15:35
Reporternicky 
Assigned Tofvedrine 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0002491: incompatibilité de libc/math.h ??
Descriptionl'instruction #include 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'
Steps To Reproduceframa-c test_math.cpp -print > op_test_math
Additional Informationparsing 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);
TagsNo tags attached.
Attached Filescpp file icon test_math.cpp [^] (18 bytes) 2020-01-22 15:08

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2020-01-22 15:08 nicky New Issue
2020-01-22 15:08 nicky Status new => assigned
2020-01-22 15:08 nicky Assigned To => fvedrine
2020-01-22 15:08 nicky File Added: test_math.cpp
2020-01-23 15:32 nicky File Added: op_test_math_std
2020-01-23 15:33 nicky File Deleted: op_test_math_std


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker