frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T12:53:24Z
https://git.frama-c.com/pub/frama-c/-/issues/97
incompatibilité de libc/math.h ??
2021-02-22T12:53:24Z
Nicky Williams
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:
**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)
Franck Vedrine
Franck Vedrine
https://git.frama-c.com/pub/frama-c/-/issues/243
const fields in constructors
2021-02-22T12:57:11Z
mantis-gitlab-migration
const fields in constructors
ID0002395:
**This issue was created automatically from Mantis Issue 2395. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002395:
**This issue was created automatically from Mantis Issue 2395. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002395 | Frama-C | Plug-in > clang | public | 2018-08-24 | 2018-09-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abhishek.anand.iitg@gmail.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Manjaro | **OS Version** | 8/23/2018 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
Const fields in constructors are not handled properly.
Below is an example:
class A {
public:
const int x;
A(int y): x(y){}
};
int main()
{
A a(0);
}
I get the following error:
root@27db7a69b96a:/hostshare# frama-c -print constFieldBug.cpp
[kernel] Parsing constFieldBug.cpp (external front-end)
Now output intermediate result
[kernel] constFieldBug.cpp:4: User Error:
Cannot assign to non-modifiable lval this->x
[kernel] User Error: stopping on file "constFieldBug.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
Perhaps such constructors have to first initialize all fields using the {} notation and then do the rest of the construction of all fields and then do the rest of the constructor body.
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/256
Crash on attempt to start framaCIRGen when libs are linked statically and dyn...
2021-02-22T12:57:36Z
mantis-gitlab-migration
Crash on attempt to start framaCIRGen when libs are linked statically and dynamically.
ID0002368:
**This issue was created automatically from Mantis Issue 2368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002368:
**This issue was created automatically from Mantis Issue 2368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002368 | Frama-C | Plug-in > clang | public | 2018-02-15 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DeMaze | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | GNU/Linux | **OS** | Debian | **OS Version** | 9.3 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
On the attempt to install Frama-Clang regularly as described (see
attached file installation.txt), the executable framaCIRGen exits with
an error when executed. The error message points to a problem with
LLVM. In fact, it depicts one commandline option to be registered more
than once. This occurs on the attempt of using Frama-C to parse C++
source code and when the executable framaCIRGen is invoked manually on
the commandline. I get the following error:
<output nr="0" command="./frama-clang-0.0.4/bin/framaCIRGen">
: CommandLine Error: Option 'asm-macro-max-nesting-depth' registered more than once!
LLVM ERROR: inconsistency in registered CommandLine options
</output>
However, this has only been observed ith llvm-5.0 on Debian GNU/Linux
9.3 (my system, see lsb_release_3ffbf_2018-02-10000905) for now. With
llvm 3.9, no such errors happen. Presumably, versions of llvm > 5.0
could also be affected. This seems to be a problem many people have
experienced with llvm related programs [2][3][4][5]. In fact, it has
even been reported for frama-clang [6].
### Additional Information :
Root Cause
==========
As far as my investigations revealed, this problem occurs because of
the linking mechanism on Debian GNU/Linux. On this distribution,
libraries of LLVM are built two-fold:
Static archives (lib*.a):
clangFrontend, clangDriver, clangTooling, clanParse, clangSema,
clangAnalysis, clangEdit, clangAST, clangLex, clangSerialization,
clangBasic, LLVMTransformUtils, LLVMBitReader, LLVMMCParser,
LLVMOption
Shared object (lib*.so):
LLVM-5.0
Therefore, it is tried to link them according to their type (lines 74-77, 82-85):
<output nr="1" command="cat frama-clang-0.0.4/Makefile.clang -n | grep 'USEDLIBS' -A 5 -B 5 ">
69 CFLAGS+=-g
70 CLANG_LINKFLAGS+=-g
71 endif
72
73 #LINK_COMPONENTS := $(TARGETS_TO_BUILD) asmparser support mc
74 USEDLIBS = clangFrontend \
75 clangDriver clangTooling clangParse clangSema \
76 clangAnalysis clangEdit clangAST clangLex clangSerialization \
77 clangBasic LLVMTransformUtils LLVMBitReader LLVMMCParser LLVMOption
78
79 # for use in main Makefile
80 default: $(PLUGIN_DIR)/bin/$(TOOLNAME)
81
82 $(PLUGIN_DIR)/bin/$(TOOLNAME): $(OBJS) $(PLUGIN_DIR)/bin
83 $(PRINT_LINKING) $@
84 $(CXX) $(CLANG_LINKFLAGS) -o $@ \
85 $(OBJS) $(addprefix -l,$(USEDLIBS)) $(LLVM_LIBS) $(CLANG_SYSLIBS) $(CLANG_LINKFLAGS)
86
87 $(PLUGIN_DIR)/bin:
88 $(MKDIR) $@
89
90 clean:
</output>
This results in the following dependencies on dynamic libraries as follows:
<output n="2" command="ldd ./frama-clang-0.0.4/bin/framaCIRGen">
linux-vdso.so.1 (0x00007ffe31ff5000)
libLLVM-5.0.so.1 => /usr/lib/x86_64-linux-gnu/libLLVM-5.0.so.1 (0x00007fb4c4825000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fb4c44a3000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb4c419f000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fb4c3f88000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb4c3be9000)
libffi.so.6 => /usr/lib/x86_64-linux-gnu/libffi.so.6 (0x00007fb4c39e0000)
libedit.so.2 => /usr/lib/x86_64-linux-gnu/libedit.so.2 (0x00007fb4c37a8000)
librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007fb4c35a0000)
libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fb4c339c000)
libtinfo.so.5 => /lib/x86_64-linux-gnu/libtinfo.so.5 (0x00007fb4c3172000)
libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fb4c2f55000)
libz.so.1 => /lib/x86_64-linux-gnu/libz.so.1 (0x00007fb4c2d3b000)
/lib64/ld-linux-x86-64.so.2 (0x00007fb4c9431000)
libncurses.so.5 => /lib/x86_64-linux-gnu/libncurses.so.5 (0x00007fb4c2b18000)
libbsd.so.0 => /lib/x86_64-linux-gnu/libbsd.so.0 (0x00007fb4c2902000)
</output>
From this output, this assumption can be confirmed because
ligcc_s.so.1 as well as libLLVM-5.0.so.1 occurs. A response on a bug
report of LLVM considers this as rather bad practice
however. Moreover, this is mentioned as a classical problem of LLVM's
"global object-based commandline switch registration" [1]:
"The command line option error is the classical problem one gets due
to the LLVM's global object-based command line switch registration. If
you somehow link the same global object (that registers the command
line option) twice via dynamic loading of the LLVM library twice or
more to the same process, it registers the same command line object
again (when calling the global object initializer), resulting in this
error." [1]
The aforementioned symbol 'asm-macro-max-nesting-depth' occurs both in
libLLVMMCParser.a and libLLVM-5.0.so.1 . Hence, I conjecture these are
the files in conflict.
My Solution
===========
Just link without libLLVMMCParser.a or more precisely, remove
LLVMMCParser from USEDLIBS in Makefile.clang. This seems to work as
C++ code is analyzable again. Please find patches for Makefile.clang
attached which circumvent this problem according to my proposal
(Makefile.clang.patch / Makefile.clang.patch.better). Feel free to
contacting me in case of any further quesions / comments.
References
==========
[1] https://bugs.llvm.org/show_bug.cgi?id=30587#c6
[2] https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=768185
[3] https://bugs.llvm.org/show_bug.cgi?id=31571
[4] http://llvm.1065342.n5.nabble.com/llvm-dev-LLD-and-LLVM-LINK-LLVM-DYLIB-td104570.html
[5] https://github.com/zig-lang/zig/issues/67
[6] https://stackoverflow.com/questions/45647503/errors-when-using-the-frama-clang-plugin
### Steps To Reproduce :
1. Manually install llvm-5.0 as described on https://apt.llvm.org/
2. Download and build frama-clang as described officially with llvm-5.0
3. Execute ./bin/framaCIRGen
## Attachments
- [logs_and_more.tar.xz](/uploads/d2a4d0490b88cd4c21961e8a55ab0ca2/logs_and_more.tar.xz)
https://git.frama-c.com/pub/frama-c/-/issues/269
user-defined type not accepted after builtin type in quantifier chain
2021-02-22T12:58:00Z
Jochen Burghardt
user-defined type not accepted after builtin type in quantifier chain
ID0002365:
**This issue was created automatically from Mantis Issue 2365. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002365:
**This issue was created automatically from Mantis Issue 2365. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002365 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp partial_sort_cpp.cpp" on the attached program reports "partial_sort_cpp.cpp:4:43: unexpected token 'identifier -> v' after a binders construct". The message disappears when "v" is declared as "int" instead of "value_type", or when "int n" is removed.
## Attachments
- [partial_sort_cpp.cpp](/uploads/27af4a5cad254a4d4837fb9aae5e0732/partial_sort_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/271
variable declared in "for" init-part unrecognized in loop body assigns clause...
2021-02-22T12:58:01Z
Jochen Burghardt
variable declared in "for" init-part unrecognized in loop body assigns clause; 100% verification degree reported nevertheless
ID0002363:
**This issue was created automatically from Mantis Issue 2363. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002363:
**This issue was created automatically from Mantis Issue 2363. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002363 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp remove_copy_cpp.cpp" on the attached program prints an error message "remove_copy_cpp.cpp:4:17: unknown identifier 'i'". When "i" is declared outside the loop, the message disappears.
As a second, more severe issue, Frama-C subsequently ignores the assertion. It prints "[wp] Proved goals: 0 / 0", and terminates successfully with exit code 0. In a larger program, an error message like the above one is likely to be overlooked, and from a reported verification degree of 100%, the user will infer that his program has been fully verified.
## Attachments
- [remove_copy_cpp.cpp](/uploads/6f2ad5f898b23f26b2560dceafaa9ba7/remove_copy_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/272
"let" in predicate body unrecognized
2021-02-22T12:58:02Z
Jochen Burghardt
"let" in predicate body unrecognized
ID0002362:
**This issue was created automatically from Mantis Issue 2362. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002362:
**This issue was created automatically from Mantis Issue 2362. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002362 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp replace_copy_cpp.cpp" on the attached program issues two messages, the 2nd probably being a follow-up problem of the 1st:
replace_copy_cpp.cpp:2:47: unexpected token 'operator -> =' when starting to parse a term
replace_copy_cpp.cpp:4:21: unknown identifier 'Replace'
When the body of predicate definition of "Replace" is changed to "( \at(a[0],K) > 3 )", both message disappear.
## Attachments
- [replace_copy_cpp.cpp](/uploads/dfacff4304f7f33dc22b5bb80602202c/replace_copy_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/273
"assigns" in statement contract causes abort or crash
2021-02-22T12:58:03Z
Jochen Burghardt
"assigns" in statement contract causes abort or crash
ID0002361:
**This issue was created automatically from Mantis Issue 2361. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002361:
**This issue was created automatically from Mantis Issue 2361. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002361 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c remove_cpp.cpp" on the attached program outputs
"framaCIRGen: ACSLStatementAnnotation.cpp:248: Parser::Base::ReadResult Acsl::StatementAnnotation::readToken(Acsl::Parser::State&, Acsl::Parser::Arguments&): Assertion `false' failed."
and then aborts. If the "ensures" clause in line 5 is removed, Frama-C outputs instead:
"*** Error in `framaCIRGen': double free or corruption (out): 0x0000559f983d0160 ***"
and then aborts, too. If in addition "a[0..9]" is removed from the "assigns" claus in line 4, Frama-C crashes (Segmentation fault) without printing any error message before. For the latter reason, I've set the severity to "crash".
## Attachments
- [remove_cpp.cpp](/uploads/2af0af96279845d9332c5293876e6c3e/remove_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/274
"Here" as predicate label in statement contract causes Segmentation fault
2021-02-22T12:58:03Z
Jochen Burghardt
"Here" as predicate label in statement contract causes Segmentation fault
ID0002360:
**This issue was created automatically from Mantis Issue 2360. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002360:
**This issue was created automatically from Mantis Issue 2360. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002360 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp rotate_cpp.cpp" on the attached program outputs an error message "rotate_cpp.cpp:5:23: expecting a label argument", and then crashes due to a Segmentation fault. The problem disappears when the statement contract in line 5 is changed into an assertion.
## Attachments
- [rotate_cpp.cpp](/uploads/56cddcc4aad61f74882ab6f0a55106cf/rotate_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/275
Frama-clang complains when reserved keywords are used as property labels, whi...
2021-02-22T12:58:04Z
Jochen Burghardt
Frama-clang complains when reserved keywords are used as property labels, while Frama-C doesn't
ID0002359:
**This issue was created automatically from Mantis Issue 2359. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002359:
**This issue was created automatically from Mantis Issue 2359. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002359 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp st.cpp" on the attached program produces a (stderr) message "st.cpp:2:14: keyword 'keyword -> invariant' encountered when parsing term or predicate". When 'invariant' is changed e.g. to 'assert', a similar message is printed.
When the file is renamed to "st.c", the message disappears. Likewise, our use of a reserved keyword as procedure or parameter name didn't cause such a message.
## Attachments
- [st.cpp](/uploads/41260701caea5f2a98b989b4454b1fc1/st.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/277
can't handle lemma with 3 labels
2021-02-22T12:58:06Z
Jochen Burghardt
can't handle lemma with 3 labels
ID0002357:
**This issue was created automatically from Mantis Issue 2357. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002357:
**This issue was created automatically from Mantis Issue 2357. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002357 | Frama-C | Plug-in > clang | public | 2018-02-08 | 2018-02-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp adjacent_difference_inv_cpp.cpp" on the attached program reports an error in line 6: "logic label `L' not found". The error message disappears when
(1) the file is renamed to "adjacent_difference_inv_cpp.c", and processed by plain Frama-C,
(2) the middle conjunct "foo{L}(1)" is removed in line 6, or
(3) label "M" is omitted in the header of "lem", and the rightmost conjunct is changed to "foo{L}(2)".
Consistently renaming the labels doesn't make the error message vanish.
## Attachments
- [adjacent_difference_inv_cpp.cpp](/uploads/e88a6c1225e59965e3a2ca825b8f7feb/adjacent_difference_inv_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/283
warning from kernel about exceptions
2021-02-22T12:58:13Z
Jens Gerlach
warning from kernel about exceptions
ID0002349:
**This issue was created automatically from Mantis Issue 2349. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002349:
**This issue was created automatically from Mantis Issue 2349. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002349 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is more a question than a bug report...
In the attached example Frama-Clang issue the warning
frama-c -wp -wp-rte exception_warning.cpp
[kernel] Parsing exception_warning.cpp (external front-end)
Now output intermediate result
[kernel] warning: Assuming declared function bar can't throw any exception
This also occurs when I add "noexcept" to the declaration of "bar".
(see second file: exception_warning_noexcept.cpp)
Is there a way to declare in the contract that a function cannot throw?
Or what do I have to do to get rid of this warning?
## Attachments
- [exception_warning.cpp](/uploads/1c9349ade800a02746a00368ccb273fc/exception_warning.cpp)
- [exception_warning_noexcept.cpp](/uploads/de71f4c8b161448d91413e4af41e8b4d/exception_warning_noexcept.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/285
unknown variable in contract is not treated as an error
2021-02-22T12:58:15Z
Jens Gerlach
unknown variable in contract is not treated as an error
ID0002348:
**This issue was created automatically from Mantis Issue 2348. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002348:
**This issue was created automatically from Mantis Issue 2348. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002348 | Frama-C | Plug-in > clang | public | 2018-01-30 | 2018-01-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached C/C++ code is treated differently by Frama-C and Frama-Clang
The C file 'unknown_variable.c' is correctly rejected by Frama-C with wit the the message
frama-c -wp -wp-rte unknown_variable.c
[kernel] user error: stopping on file "unknown_variable.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
When processing this file as C++ code
frama-c -wp -wp-rte unknown_variable.cpp
Frama-Clang only emits a warning (by the kernel) and continues processing
Parsing unknown_variable.cpp (external front-end)
unknown_variable.cpp:6:18: unknown identifier 'c'
Now output intermediate result
In my opinion, the C++ contract should be rejected as well.
## Attachments
- [unknown_variable.c](/uploads/c5a054e84514556cecef576a58a99a77/unknown_variable.c)
- [unknown_variable.cpp](/uploads/1b1624f8c2b2da94da16a415596ba498/unknown_variable.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/287
C++11 delegating constructor not supported
2021-02-22T12:58:18Z
Jens Gerlach
C++11 delegating constructor not supported
ID0002346:
**This issue was created automatically from Mantis Issue 2346. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002346:
**This issue was created automatically from Mantis Issue 2346. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002346 | Frama-C | Plug-in > clang | public | 2018-01-19 | 2018-01-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **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 :
The attached two examples for with g++ in C++11 mode.
The first example is pure C++03. Fram-Clang can handle it.
The second version uses a delegation constructor.
Frama-Clang fails on this one with the error message:
frama-c -val object_construction2.cpp
[kernel] Parsing object_construction2.cpp (external front-end)
Unsupported constructor initializer:SomeType
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "object_construction2.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
### Additional Information :
frama-clang 0.0.4
## Attachments
- [object_construction1.cpp](/uploads/9470c7f8b2af8d771a6a8e48784a42c4/object_construction1.cpp)
- [object_construction2.cpp](/uploads/7f0b7bc342fb3b3b749aafd7bce30c70/object_construction2.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/288
range based for loop from C++11 not supported
2021-02-22T12:58:19Z
Jens Gerlach
range based for loop from C++11 not supported
ID0002345:
**This issue was created automatically from Mantis Issue 2345. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002345:
**This issue was created automatically from Mantis Issue 2345. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002345 | Frama-C | Plug-in > clang | public | 2018-01-19 | 2018-01-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **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 :
The attached example compiles without waring in C++11 mode
g++ --std=c++11 -Wall -c -o range_based_for_loop.o range_based_for_loop.cpp
but it fails with
frama-c -val range_based_for_loop.cpp
Error message says:
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "range_based_for_loop.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
## Attachments
- [range_based_for_loop.cpp](/uploads/06215bb4a9f91910a1a0bacff4ffa79f/range_based_for_loop.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/289
std::bad_alloc not supported
2021-02-22T12:58:19Z
Jens Gerlach
std::bad_alloc not supported
ID0002342:
**This issue was created automatically from Mantis Issue 2342. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002342:
**This issue was created automatically from Mantis Issue 2342. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002342 | Frama-C | Plug-in > clang | public | 2018-01-18 | 2018-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | linux | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Attached is a simple C++ (03) program that checks whether 'new' has thrown an exception.
I am not yet sure whether this is due to general lack of exceptions or just a library issue.
I report just for completeness.
### Steps To Reproduce :
Call 'frama-c -val new_bad_alloc.cpp'
## Attachments
- [new_bad_alloc.cpp](/uploads/d2abd5208e0f45238cee308e702b69b7/new_bad_alloc.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/642
can't prove (trivial) validity of memory access of "p->a"
2021-02-22T13:07:57Z
Jochen Burghardt
can't prove (trivial) validity of memory access of "p->a"
ID0002112:
**This issue was created automatically from Mantis Issue 2112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002112:
**This issue was created automatically from Mantis Issue 2112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002112 | Frama-Clang | Plug-in > clang | public | 2015-05-04 | 2015-05-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte 477.cpp" on the attached program leaves an obligation "typed_main_assert_rte_mem_access" unproven by Alt-Ergo. It goal formula in file "main_assert_rte_mem_access_Alt-Ergo.mlw" reads:
576 goal main_assert_rte_mem_access:
577 forall t_1,t : int farray.
578 linked(t) ->
579 valid_rw(t_1, shiftfield_F__Z1X_a(shift__Z1X(global(L_x_111), 0)), 1)
When "t" is changed to "t_1" in line 578, the formaula is proven. This looks as if an "assigns" clause is missing for some operator. However, there is no user-defined operator involved here, so the necessary "assigns" clause should be generated by Frama-C.
## Attachments
- [477.cpp](/uploads/cabf9f2eb5e5c7118db6400bf14d3275/477.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/649
declaration of local variable of class type results in unprovable assigns clause
2021-02-22T13:08:04Z
Jochen Burghardt
declaration of local variable of class type results in unprovable assigns clause
ID0002106:
**This issue was created automatically from Mantis Issue 2106. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002106:
**This issue was created automatically from Mantis Issue 2106. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002106 | Frama-Clang | Plug-in > clang | public | 2015-04-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The assigns clause in line 4 of the attached program results in two Alt-Ergo obligations (such as "goal _Z3foo_assign_normal: forall t : int farray. not linked(t)" in obligation file "_Z3foo_assign_normal_Alt-Ergo.mlw"), none of which is provable.
However, from a C++ programmer's point of view, the clause should be valid.
Probably, some Frama-Cxx-internal variables are assigned by the implicit constructor "A()", and hence by "foo()", but there is no clue how to refer to them. Maybe they should be added automatically by Frama-Cxx to the set of assigned locations.
## Attachments
- [469.cpp](/uploads/a03e4e3a40b48a76922e10de413446fb/469.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/650
template parameter type can't used in typedef
2021-02-22T13:08:05Z
Jochen Burghardt
template parameter type can't used in typedef
ID0001972:
**This issue was created automatically from Mantis Issue 1972. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001972:
**This issue was created automatically from Mantis Issue 1972. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001972 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
136.cpp:6:[kernel] failure: Cannot find type _ZN6traitsIiE2stE2tp (kind:type)
The problem disappears if the surrounding "struct st {" and "};" is deleted in line 3, and "st::" is deleted in line 6.
BTW: A call of "c++filt -n _ZN6traitsIiE2stE2tp" yields "traits<int>::st(tp)", while I would have expected "traits<int>::st::tp".
(Importance: this code is used via #include <vector>.)
Other issues that involve both typedef and templates were/are #1705, #1580, #1531. One of them might be related to the problem here.
## Attachments
- [136.cpp](/uploads/7681db01d5299465de8a20e5ebe39490/136.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/654
"__is_trivial" causes abort
2021-02-22T13:08:13Z
Jochen Burghardt
"__is_trivial" causes abort
ID0001967:
**This issue was created automatically from Mantis Issue 1967. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001967:
**This issue was created automatically from Mantis Issue 1967. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001967 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Unsupported expressions:UnaryTypeTraitExpr 0x253e888 <134.cpp:2:10, col:26> '_Bool'
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
(Importance: this code is used via #include <vector>.)
## Attachments
- [134.cpp](/uploads/fc0e0514a33ec9a94e33e11fd592e5b0/134.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/656
extra "//" comment within "//@" annotation causes abort
2021-02-22T13:08:15Z
Jochen Burghardt
extra "//" comment within "//@" annotation causes abort
ID0002013:
**This issue was created automatically from Mantis Issue 2013. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002013:
**This issue was created automatically from Mantis Issue 2013. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002013 | Frama-Clang | Plug-in > clang | public | 2014-12-04 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
framaCIRGen: src/frama-clang/ACSLToken.h:563: Acsl::DLexer::AbstractToken Acsl::DLexer::Token::getFullToken() const: Assertion `_type != 0' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem disappears if "// comment" is deleted in line 2, or if the file is renamed to "190.c".
## Attachments
- [190.cpp](/uploads/6e7ae2cf72d87f620e534fcf2c6a03dd/190.cpp)