frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:52:23Zhttps://git.frama-c.com/pub/frama-c/-/issues/2156wrong generation of assigns \nothing at function call2021-02-22T13:52:23ZPatrick Baudinwrong generation of assigns \nothing at function callID0000800:
**This issue was created automatically from Mantis Issue 800. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000800:
**This issue was created automatically from Mantis Issue 800. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000800 | Frama-C | Plug-in > RTE | public | 2011-04-18 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | pherrmann | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
RTE should not generate assigns \nothing; at the statement calling function f
### Additional Information :
> cat file.c:
int X, Y ;
//@ assigns \union(X, Y) ;
void f () ;
void g() {
f () ;
}
> frama-c -print -rte file.c
int X ;
int Y ;
/*@ assigns \union(X, Y); */
extern void f() ;
void g(void)
{
/*@ behavior pre_f_0:
assigns \nothing; */
f();
return;
}https://git.frama-c.com/pub/frama-c/-/issues/2050RTE does not generate assertions for non initialized arguments2021-02-22T13:49:48ZBoris YakobowskiRTE does not generate assertions for non initialized argumentsID0000877:
**This issue was created automatically from Mantis Issue 877. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000877:
**This issue was created automatically from Mantis Issue 877. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000877 | Frama-C | Plug-in > RTE | public | 2011-07-06 | 2012-05-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pherrmann | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Calling the WP (or Jessie for that matter) on the following code results in all goals being proven. Yet, there is a RTE on the call to max, because a is not initialized. I tend to think that -rte-precond should add \initialized(a) and \initialized(b) to the local contract for the call to max, but there is perhaps another better way. Anyway, either RTE or the WP are faulty here.
/*@ ensures \result == (a < b ? a : b); */
int max(int a, int b) {
return (a < b ? a : b);
}
int main () {
int a;
int b = 2;
return max (a, b);
}https://git.frama-c.com/pub/frama-c/-/issues/1997RTE does not check for downcast of unsigned integer2021-02-22T13:48:16Zmantis-gitlab-migrationRTE does not check for downcast of unsigned integerID0001083:
**This issue was created automatically from Mantis Issue 1083. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001083:
**This issue was created automatically from Mantis Issue 1083. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001083 | Frama-C | Plug-in > RTE | public | 2012-02-07 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sylvain nahas | **Assigned To** | pherrmann | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Frama-C does not behave as one could expect with the following code:
unsigned char main(unsigned char a, unsigned char b)
{
return (a + b);
}
$frama-c -rte -rte-unsigned-ov toto.c -rte-print -then -val -then -werror
...
unsigned char main(unsigned char a, unsigned char b)
{
unsigned char __retres;
/*@ assert
rte: (int)a+(int)b ? 2147483647 ? (int)a+(int)b ? (-0x7FFFFFFF-1);
*/
__retres = (unsigned char)((int)a + (int)b);
return (__retres);
}
The plug-in generates checks for the overflow of int, but not for the downcasting of int to unsigned char. One would expect:
0 ? (int)a+(int)b ? USCHR_MAX
In my opinion, this is not a bug, but rather a missing functionality. The RTE plugin should offer an option symmetrical to -rte-downcast for unsigned integers, which generates annotation for unsigned downcast.https://git.frama-c.com/pub/frama-c/-/issues/1857Missing index_bound2021-02-22T13:44:21Zmantis-gitlab-migrationMissing index_boundID0001429:
**This issue was created automatically from Mantis Issue 1429. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001429:
**This issue was created automatically from Mantis Issue 1429. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001429 | Frama-C | Plug-in > RTE | public | 2013-05-24 | 2013-05-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
No 'index_bound' annotation is generated in that case to check that 0 <= i < 10 :
typedef struct { int t[10]; } Tstr;
void main (int i) {
Tstr s;
Tstr * ps = &s;
f(& ps->t[i]);
}https://git.frama-c.com/pub/frama-c/-/issues/1045Unproven rte assertions for bit complement2023-10-09T13:44:38ZJens GerlachUnproven rte assertions for bit complementID0001769:
**This issue was created automatically from Mantis Issue 1769. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001769:
**This issue was created automatically from Mantis Issue 1769. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001769 | Frama-C | Plug-in > RTE | public | 2014-05-01 | 2014-05-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am struggling with unproven run time assertions in a some piece of code that heavily relies on bit operations.
In fact, I am not sure this an issue of the rte plug-in.
It is probably related to https://bts.frama-c.com/view.php?id=1750
which I submitted to the WP section.
However, I wonder if the rte plug-in could make the task of WP easier.
The attached file simply performs bitwise complement for various unsigned integer types.
For unsigned char and unsigned short the rte plugin generates unsigned_downcast assertion that
WP cannot discharge.
I understand that the promotion of the variable "a" to int is covered by the C standard.
On the other hand, the C standard says in 6.5.3.4 (4)
If the promoted type is an unsigned type, the expression ~E is equivalent to the maximum value
representable in that type minus E.
So, no overflow will occur.
### Steps To Reproduce :
I called the file with the following options
frama-c-gui.byte -cpp-command 'gcc -C -E -nostdinc -I/usr/local/share/frama-c/libc' -pp-annot -no-unicode -wp -warn-signed-downcast -warn-signed-overflow -warn-unsigned-downcast -warn-unsigned-overflow -wp-rte complement.c
## Attachments
- [complement.c](/uploads/5a515e096bc7eeb191a98c240d20e77e/complement.c)https://git.frama-c.com/pub/frama-c/-/issues/1044Missing rte guard when assigning an unsigned int to an int2021-02-22T13:23:19ZJens GerlachMissing rte guard when assigning an unsigned int to an intID0001766:
**This issue was created automatically from Mantis Issue 1766. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001766:
**This issue was created automatically from Mantis Issue 1766. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001766 | Frama-C | Plug-in > RTE | public | 2014-04-30 | 2014-05-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux | **OS Version** | ubuntu 3.13 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following function assigns the unsigned int variable "a" to the int variable "b".
I do not see any generated rte assertions to guard this operation.
The C standard says in 6.3.1.3.3 about this kind of operation
Otherwise, the new type is signed and the value cannot be represented in it; either the result is
implementation-defined or an implementation-defined signal is raised.
On the other hand, for the operation involving "a" and "x", proper rte guards are generated.
/*@
requires \valid(x);
assigns *x;
*/
int f(unsigned int a, unsigned int* x)
{
*x = a + a;
int b = a;
return b;
}https://git.frama-c.com/pub/frama-c/-/issues/401Annotation wrongly displayed as checked (green bullet) whereas it is false, w...2021-02-22T13:01:21Zmantis-gitlab-migrationAnnotation wrongly displayed as checked (green bullet) whereas it is false, when using the option -rte on command line.ID0002258:
**This issue was created automatically from Mantis Issue 2258. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002258:
**This issue was created automatically from Mantis Issue 2258. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002258 | Frama-C | Plug-in > RTE | public | 2016-11-24 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | julien-cohen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | PC | **OS** | Linux Ubuntu | **OS Version** | 16.04 LTS |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have a program with an incorrect acces outside an array. When lauching frama-c-gui with no options and value analysis, the out-of-bounds access is detected and the corresponding annotation is displayed with an orange bullet. When using the -rte option, two annotations are displayed (for the lower and upper bound of the array), and a green bullet is displayed for both (which is not correct).
/*@ assert rte: index_bound: 0 ≤ cpt; */
/*@ assert rte: index_bound: cpt < 5; */
The console says :
tableau_erreur.c:11:[value] Assertion 'rte,index_bound' got status valid.
### Additional Information :
Posted on http://stackoverflow.com/questions/40763614/unsound-behavior-with-rte-option-in-magnesium/40766174#40766174 .
There are two screen captures there. Someone (anol) replied and gave additional information (see the post).
### Steps To Reproduce :
Here is my program :
int main(){
int t[5] = {1,2,3,4,5};
int cpt =0 ;
int tmp ;
while (cpt<10){
tmp = getchar() ;
if ( t[cpt] > tmp )
{ return 1 ; }
cpt++ ;
}
return 10 ;
}
The problem occurs when launching frama-c-gui -rte and the calue analysis on this program.https://git.frama-c.com/pub/frama-c/-/issues/293Incorrect overflow and cast assertions for bitfields2021-02-22T13:36:38ZKostyantyn VorobyovIncorrect overflow and cast assertions for bitfieldsID0002314:
**This issue was created automatically from Mantis Issue 2314. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002314:
**This issue was created automatically from Mantis Issue 2314. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002314 | Frama-C | Plug-in > RTE | public | 2017-06-26 | 2017-12-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following snippet:
struct STR { int num : 7; };
void foo(int a, long b) {
struct STR s = { .num = 0 };
s.num = b;
s.num += a;
}
generates the following assertions
/*@ assert rte: signed_downcast: b ≤ 2147483647; */
/*@ assert rte: signed_downcast: -2147483648 ≤ b; */
s.num = (int)b;
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)s.num + a; */
/*@ assert rte: signed_overflow: (int)s.num + a ≤ 2147483647; */
s.num = (int)((int)s.num + a);
The limits for s.num are incorrect, since s.num is a bitfield of 7 bits its limits should be [-64, 63]
### Steps To Reproduce :
frama-c -machdep x86_64 file.c -rte -warn-signed-overflow -warn-signed-downcast -print
## Attachments
- [b.c](/uploads/40289826f17e8973d35c95cb375e1d60/b.c)
- [patch-downcast-rte](/uploads/f5123ced359a007c0de00ba52c7fc3cd/patch-downcast-rte)https://git.frama-c.com/pub/frama-c/-/issues/235RTE assertion for signed right shift is wrong2021-02-22T12:57:02Zmantis-gitlab-migrationRTE assertion for signed right shift is wrongID0002354:
**This issue was created automatically from Mantis Issue 2354. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002354:
**This issue was created automatically from Mantis Issue 2354. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002354 | Frama-C | Plug-in > RTE | public | 2018-02-03 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | xleroy | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
Consider:
/*@ ensures \result == arg >> 2; */
int toto(int arg) { return arg >> 2; }
"frama-c -wp -wp-rte" fails to verify this rather tautological spec because the RTE pass inserts the assertion
/*@ assert rte: shift: 0 ≤ arg; */
I think this is an incorrect reading of the ISO C 90 and C 99 specs: right-shift of a signed integer expression that has a negative value is implementation-defined, but is not an undefined behavior. (See ISO C 99 section 6.5.7 item 5.)
I would suggest that WP and RTE accept the spec above, so that I can actually reason about the right shift, probably by adding axioms specifying how right shifts of negative numbers work on the platforms I am (and everyone is) interested in.https://git.frama-c.com/pub/frama-c/-/issues/181Missing cast in code generated by RTE2021-04-20T07:27:57ZJulien SignolesMissing cast in code generated by RTEID0002419:
**This issue was created automatically from Mantis Issue 2419. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002419:
**This issue was created automatically from Mantis Issue 2419. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002419 | Frama-C | Plug-in > RTE | public | 2018-12-17 | 2018-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
==========
int main(void) {
int i = 2;
unsigned int j = i < 2;
return 0;
}
$ frama-c -check -rte -warn-unsigned-downcast -print -ocode res.c
[kernel] Parsing a.c (with preprocessing)
[rte] annotating function main
/* Generated by Frama-C */
int main(void)
{
int __retres;
int i = 2;
/*@ assert rte: unsigned_downcast: (i < 2) ≤ 4294967295; */
/*@ assert rte: unsigned_downcast: 0 ≤ (i < 2); */
unsigned int j = (unsigned int)(i < 2);
__retres = 0;
return __retres;
}
$ frama-c res.c
[kernel] Parsing res.c (with preprocessing)
[kernel:annot-error] res.c:6: Warning:
comparison of incompatible types: 𝔹 and ℤ. Ignoring code annotation
[kernel] User Error: warning annot-error treated as fatal error.
==========
The terms (i < 2) should be casted to int in the generated predicatesJulien SignolesJulien Signoles