2021-01-18 18:55 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002491Frama-CPlug-in > clangpublic2020-01-23 15:35
Reporternicky 
Assigned Tofvedrine 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0002491: incompatibilité de libc/math.h ??
Descriptionl'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'
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 Files

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-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
+Issue History