frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2023-05-05T02:36:31Z
https://git.frama-c.com/pub/frama-c/-/issues/1248
possible unsoundness bug
2023-05-05T02:36:31Z
John Regher
possible unsoundness bug
ID0000717:
**This issue was created automatically from Mantis Issue 717. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000717:
**This issue was created automatically from Mantis Issue 717. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000717 | Frama-C | Plug-in > Eva | public | 2011-02-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | regehr | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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 :
This is on Ubuntu 10.10 on x86.
Analyzing the attached program like this:
toplevel.opt -val -slevel 24 foo_pp.c
Gives output including:
*(unsigned char*)((unsigned char*)&g_8+30) == 0
However, running the program leaves the value 243 in this byte.
## Attachments
- [foo_pp.c](/uploads/d4618293170dad277408009f857c0c3d/foo_pp.c)
https://git.frama-c.com/pub/frama-c/-/issues/1249
Lexing of ACSL characters
2021-02-22T13:24:44Z
Patrick Baudin
Lexing of ACSL characters
ID0000714:
**This issue was created automatically from Mantis Issue 714. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000714:
**This issue was created automatically from Mantis Issue 714. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000714 | Frama-C | Kernel > ACSL implementation | public | 2011-02-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | patrick | **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 :
frama-c cannot parse the ACSL expression: '\\' + 'a'
The lexer considers, as a unique token, the expression: '\\' + '
https://git.frama-c.com/pub/frama-c/-/issues/1250
passing (C && c) as argument to a function that expects int (csmith)
2021-02-22T13:42:45Z
Pascal Cuoq
passing (C && c) as argument to a function that expects int (csmith)
ID0000725:
**This issue was created automatically from Mantis Issue 725. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000725:
**This issue was created automatically from Mantis Issue 725. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000725 | Frama-C | Kernel | public | 2011-02-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
$ frama-c -val char_ampamp.c
char_ampamp.c:7:[value] reading left-value x.
The contents is imprecise.
char_ampamp.c:7:[kernel] warning: accessing uninitialized left-value x: assert(Ook)
char_ampamp.c:7:[kernel] warning: accessing left-value x that contains escaping addresses; assert(Ook)
[value] Called Frama_C_show_each_x({{ ANYTHING }})
## Attachments
- [char_ampamp.c](/uploads/cb580ccef59ea48518ba110f8c027240/char_ampamp.c)
https://git.frama-c.com/pub/frama-c/-/issues/1251
r11920: Analyses -> Show callgraph requires a main function
2023-05-02T09:30:27Z
Pascal Cuoq
r11920: Analyses -> Show callgraph requires a main function
ID0000723:
**This issue was created automatically from Mantis Issue 723. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000723:
**This issue was created automatically from Mantis Issue 723. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000723 | Frama-C | Graphical User Interface | public | 2011-02-15 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **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** | Frama-C Nitrogen-20111001 |
### Description :
Launch the GUI on a C file without a main():
bin/viewer.opt tests/idct/idct.c
Select Analyses -> Show callgraph
Result:
[kernel] preprocessing with "gcc -C -E -I. tests/idct/idct.c"
[cg] beginning analysis
[gui] user error: cannot find entry point `main'.
Please use option `-main' for specifying a valid entry point.
Considering that the syntactic callgraph is most useful to find which function is the entry point, this is annoying.
https://git.frama-c.com/pub/frama-c/-/issues/1252
the input file should be the first argument to ptests
2023-04-21T13:20:33Z
Julien Signoles
the input file should be the first argument to ptests
ID0000736:
**This issue was created automatically from Mantis Issue 736. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000736:
**This issue was created automatically from Mantis Issue 736. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000736 | Frama-C | ptests | public | 2011-02-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | high | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
all in the title... Required in order to use -then* in tests.
https://git.frama-c.com/pub/frama-c/-/issues/1253
Incorrect states passed to value analysis callbacks in presence of slevel
2021-02-22T13:31:30Z
Boris Yakobowski
Incorrect states passed to value analysis callbacks in presence of slevel
ID0000732:
**This issue was created automatically from Mantis Issue 732. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000732:
**This issue was created automatically from Mantis Issue 732. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000732 | Frama-C | Plug-in > Eva | public | 2011-02-20 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Execute the following program with options '-val -slevel n' for n between 1 and 10001.
int p[20000];
void main () {
for (int j=0;j<10000;j++)
p[j]=1;
}
Inspecting the values of the variable j in the gui reveals ranges of the form [n..10000], which is clearly incorrect.
Also, there is a big gap in the execution time between a fully symbolic evaluation (-slevel 10001) and a partial one (eg. -slevel 10000). This seems to be related to superposing the states in the callbacks.
### Additional Information :
The bug appears between the svn revisions 11262 and 11385.
## Attachments
- ![5000](/uploads/815345649598c607d8e593513c99a542/5000.png)
https://git.frama-c.com/pub/frama-c/-/issues/1254
Function specification not exposed through vspec visitor method
2023-05-02T09:30:27Z
Boris Yakobowski
Function specification not exposed through vspec visitor method
ID0000727:
**This issue was created automatically from Mantis Issue 727. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000727:
**This issue was created automatically from Mantis Issue 727. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000727 | Frama-C | Kernel | public | 2011-02-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
The attached prints
Funspec of f is '' through visitor
It is 'behavior default:
assigns \nothing;' through get_spec
when called on this code
//@ assigns \nothing;
void f () {}
To the best of my understanding, it should print the same things in the two cases.
## Attachments
- [vis.ml](/uploads/5f84032e33971c4f38c0c566dc33152e/vis.ml)
https://git.frama-c.com/pub/frama-c/-/issues/1255
Incorrect handling of nearly-empty switch clauses with -simplify-cfg
2021-02-22T13:24:55Z
Boris Yakobowski
Incorrect handling of nearly-empty switch clauses with -simplify-cfg
ID0000720:
**This issue was created automatically from Mantis Issue 720. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000720:
**This issue was created automatically from Mantis Issue 720. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000720 | Frama-C | Kernel | public | 2011-02-13 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Frama-c chokes on the following code with option -simplify-cfg
void main()
{
switch(0) {
case 0:
break;
}
}
This can be seen either by starting the value analysis, or with -check.
https://git.frama-c.com/pub/frama-c/-/issues/1256
Unsoundness in value analysis when bitfield initializer exceeds range (csmith)
2021-02-22T13:24:58Z
John Regher
Unsoundness in value analysis when bitfield initializer exceeds range (csmith)
ID0000721:
**This issue was created automatically from Mantis Issue 721. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000721:
**This issue was created automatically from Mantis Issue 721. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000721 | Frama-C | Plug-in > Eva | public | 2011-02-13 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | regehr | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
The attached program, analyzed like this:
toplevel.opt -val -slevel 25 foo_pp.c
causes Frama-C to emit this assertion:
assert(*(unsigned int*)&g_115 == 9362872);
However, running the program gives the value of g_115 as 23992 at the end of execution.
This is on Ubuntu 10.10 on x86.
## Attachments
- [foo_pp.c](/uploads/3cf8926b10c608456b4537cd51e7b18f/foo_pp.c)
https://git.frama-c.com/pub/frama-c/-/issues/1258
Unexpected error (Ival.Float_abstract.Bottom)
2023-11-27T14:01:56Z
mantis-gitlab-migration
Unexpected error (Ival.Float_abstract.Bottom)
ID0000752:
**This issue was created automatically from Mantis Issue 752. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000752:
**This issue was created automatically from Mantis Issue 752. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000752 | Frama-C | Plug-in > Eva | public | 2011-03-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kerstin | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Crash if the 3 assertions are added to the program.
Unexpected error (Ival.Float_abstract.Bottom).
commandline: frama-c-gui -val -slevel 10 -main interp interp_bug.c
frama-c -val -slevel 10 -main interp interp_bug.c
## Attachments
- [interp_bug.c](/uploads/d959ec698d88e05db6586ff4c99a6246/interp_bug.c)
https://git.frama-c.com/pub/frama-c/-/issues/1259
wrong treatment for const arrays in lib-entry mode
2021-02-22T14:02:50Z
David Delmas
wrong treatment for const arrays in lib-entry mode
ID0000759:
**This issue was created automatically from Mantis Issue 759. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000759:
**This issue was created automatically from Mantis Issue 759. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000759 | Frama-C | Plug-in > Eva | public | 2011-03-21 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | Frama-C Oxygen-20120901 | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
With the attache source file,
frama-c fptr.c -lib-entry -main f -users
yields the below incorrect result:
[users] ====== DISPLAYING USERS ======
f: h0 h1
====== END OF USERS ==========
## Attachments
- [fptr.c](/uploads/076ddbe0115c99046256c2fb6f30d4c4/fptr.c)
https://git.frama-c.com/pub/frama-c/-/issues/1260
Dynamic plugin doc
2023-05-10T17:02:04Z
mantis-gitlab-migration
Dynamic plugin doc
ID0000754:
**This issue was created automatically from Mantis Issue 754. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000754:
**This issue was created automatically from Mantis Issue 754. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000754 | Frama-C | Kernel > Makefile | public | 2011-03-16 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Nitrogen-20111001 | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
The command : make xxx_DOC (where xxx is a dynamic plugin name) fails with the message :
Pas de règle pour fabriquer la cible « /kernel-doc.ocamldoc »
This is because $(DOC_DIR) is not defined, which seems normal (I far as I know, the compilation of dynamic plugin refers to the installed files, not to the source repository).
The easiest fix would probably be that a plugin internal documentation doesn't depend on the kernel documentation...
https://git.frama-c.com/pub/frama-c/-/issues/1263
Hex/octal signed constants can be represented in an unsigned extended integer...
2021-02-22T14:02:51Z
Pascal Cuoq
Hex/octal signed constants can be represented in an unsigned extended integer type (csmith)
ID0000775:
**This issue was created automatically from Mantis Issue 775. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000775:
**This issue was created automatically from Mantis Issue 775. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000775 | Frama-C | Kernel | public | 2011-03-31 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
main(){
int r = 0xE2DB80EBBD4856CDLL >= 1;
return r;
}
This program, when compiled with GCC, returns 1. This is in accordance to page 56 of the C99 standard, where octal/hexadecimal LL constants can be represented as unsigned long long int when they do not fit inside a long long int.
However the front-end types the program wrongly, leading the value analysis to believe the return value is 0:
~/ppc/bin/toplevel.opt -val u.c -print
[value] Values for function main:
r ? {0; }
/* Generated by Frama-C */
int main(void)
{
int r ;
r = 0xE2DB80EBBD4856CDLL >= (long long )1;
return (r);
}
https://git.frama-c.com/pub/frama-c/-/issues/1264
Slicing is sometimes not journalisable anymore
2021-02-22T13:44:59Z
Julien Signoles
Slicing is sometimes not journalisable anymore
ID0000774:
**This issue was created automatically from Mantis Issue 774. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000774:
**This issue was created automatically from Mantis Issue 774. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000774 | Frama-C | Plug-in > slicing | public | 2011-03-31 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | Frama-C Nitrogen-20111001 | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
See demo for dynamic typing.
Function internal_pretty_code on map is now required. Must be implemented.
https://git.frama-c.com/pub/frama-c/-/issues/1265
Value may be incorrect in presence of several ensures
2021-02-22T13:25:19Z
Julien Signoles
Value may be incorrect in presence of several ensures
ID0000689:
**This issue was created automatically from Mantis Issue 689. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000689:
**This issue was created automatically from Mantis Issue 689. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000689 | Frama-C | Plug-in > Eva | public | 2011-01-26 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
If a function has 1 valid ensure and 1 invalid ensure, the GUI says that both ensures are invalid.
### Steps To Reproduce :
==== a.c ====
/*@ ensures \result == 0;
@ ensures \false;
@ */
int f(void) { return 0; }
void main(void) { f(); }
==============
$ frama-c-gui a.c
Then check the property status of both ensures.
https://git.frama-c.com/pub/frama-c/-/issues/1266
r12430, some assertions are localized at Cabs2cil_start:0 (csmith)
2023-06-16T10:43:05Z
Pascal Cuoq
r12430, some assertions are localized at Cabs2cil_start:0 (csmith)
ID0000770:
**This issue was created automatically from Mantis Issue 770. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000770:
**This issue was created automatically from Mantis Issue 770. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000770 | Frama-C | Kernel | public | 2011-03-30 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
bin/toplevel.opt -val -slevel 70000 -unspecified-access dummy_loc.i
Result:
...
Cabs2cil_start:0:[kernel] warning: Unspecified sequence with side effect:
...
Cabs2cil_start:0:[kernel] warning: undefined multiple accesses in expression. assert \separated(l_934,& l_922);
...
The attached file is pre-processed but it was made from ordinary .c and .h files on a Linux system (computation server).
## Attachments
- [dummy_loc.i](/uploads/fdd12914c765bf9e2a12f0e7fd438798/dummy_loc.i)
https://git.frama-c.com/pub/frama-c/-/issues/1268
12816: Missing label in sliced program (csmith)
2021-02-22T14:02:52Z
Pascal Cuoq
12816: Missing label in sliced program (csmith)
ID0000786:
**This issue was created automatically from Mantis Issue 786. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000786:
**This issue was created automatically from Mantis Issue 786. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000786 | Frama-C | Plug-in > slicing | public | 2011-04-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Same conventions as usual, the slicing command was
~/ppc/bin/toplevel.opt -val-signed-overflow-alarms s.11215416.1.c -cpp-command "gcc -C -E -D__FRAMAC -I. -I$CSMITH/runtime " -machdep x86_64 -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-slice-force -no-val -print -ocode s.11215416.1.s.c
But when compiling the sliced program:
$ gcc s.11215416.1.s.c show_each.c
s.11215416.1.s.c: In function ‘func_10_slice_1’:
s.11215416.1.s.c:163: error: label ‘_LOR’ used but not defined
## Attachments
- [missing_label.tgz](/uploads/c96167e8377f46c437e19ec0babd22a6/missing_label.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1269
Generating metrics.html on demand
2021-02-22T13:31:42Z
Julien Signoles
Generating metrics.html on demand
ID0000784:
**This issue was created automatically from Mantis Issue 784. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000784:
**This issue was created automatically from Mantis Issue 784. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000784 | Frama-C | Plug-in > metrics | public | 2011-04-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
When computing metrics (via a command line option or the GUI), then file metrics.html is created in the current directory (or the plug-in crashes if there is a system error when opening, writing into, closing the file).
It would be nice:
- to generate the file only on demand (through a new command line option taking a filename as argument)
- to prevent crashes by catching exceptions.
https://git.frama-c.com/pub/frama-c/-/issues/1271
Sliced program computes value different from original (csmith)
2021-02-22T13:49:02Z
Pascal Cuoq
Sliced program computes value different from original (csmith)
ID0000781:
**This issue was created automatically from Mantis Issue 781. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000781:
**This issue was created automatically from Mantis Issue 781. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000781 | Frama-C | Plug-in > from | public | 2011-04-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
The program does not contain undefined behaviors in the sense of the value analysis, as checked by ~/ppc/bin/toplevel.opt -val -slevel 5000 -cpp-command "gcc -C -E -I runtime " s.11114014.1.c -no-results -machdep x86_64
But, when compiling and executing the sliced program, the number displayed is different from the number displayed by the original program.
cuoq@ns61143:~/csmith-2.0.0$ gcc -I runtime s.11114014.1.c -o s1
s.11114014.1.c: In function ‘func_59’:
s.11114014.1.c:448: warning: comparison of distinct pointer types lacks a cast
s.11114014.1.c: In function ‘func_93’:
s.11114014.1.c:895: warning: large integer implicitly truncated to unsigned type
cuoq@ns61143:~/csmith-2.0.0$ ./s1
[value] Called Frama_C_show_each({3932636802; })
cuoq@ns61143:~/csmith-2.0.0$ gcc -I runtime s.11114014.1.s.c -o s2
cuoq@ns61143:~/csmith-2.0.0$ ./s2
[value] Called Frama_C_show_each({1079028560; })
The sliced program was obtained using 12793+patch from bug report 780, with the command:
~/ppc/bin/toplevel.opt -val-signed-overflow-alarms s.11114014.1.c -cpp-command "gcc -C -E -I. -I runtime " -machdep x86_64 -slice-calls printf -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-slice-force -no-val -print -ocode s...s.c
### Additional Information :
I am in a good position to know that these big random programs can be a pain to debug. It is possible to wait for a smaller problematic program to come along.
I have quite thoroughly tested the value analysis on these random generated programs earlier. I would have liked to be more progressive and now check building blocks of the slicing, but I do not know what to use as oracle then. Only the slicing at the top of the pyramid offers a testable interface again.
Take it easy, it's only random programs.
I should replace the variadic printf by something less variadic, just in case.
## Attachments
- [incorrect_sliced_value.tgz](/uploads/55d0b17bc0d91c4f9fecc25249a823a2/incorrect_sliced_value.tgz)
- [small.tgz](/uploads/676e7c3158470fce017d924036662d7a/small.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1273
integrity problem of the AST on calls to functions with __attribute__ ((nor...
2021-02-22T13:49:10Z
Patrick Baudin
integrity problem of the AST on calls to functions with __attribute__ ((noreturn))
ID0000790:
**This issue was created automatically from Mantis Issue 790. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000790:
**This issue was created automatically from Mantis Issue 790. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000790 | Frama-C | Kernel > ACSL implementation | public | 2011-04-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Calls to function with __attribute__ ((noreturn)) have no successor.
If it is wright, that raises an ACSL problem on the specification of such functions. What are their specification?
### Additional Information :
The command:
> frama-c -check -print tests/slicing/loops.c
gives:
tests/slicing/loops.c:63:[kernel] failure: [AST Integrity Check] AST after normalization
statement stop();(35) in function stop_f1 has no successor.
https://git.frama-c.com/pub/frama-c/-/issues/1274
Plugin.is_invisible is not see-through enough
2021-02-22T13:42:38Z
Boris Yakobowski
Plugin.is_invisible is not see-through enough
ID0000729:
**This issue was created automatically from Mantis Issue 729. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000729:
**This issue was created automatically from Mantis Issue 729. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000729 | Frama-C | Kernel | public | 2011-02-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Although setting Plugin.is_invisible before creating a parameter prevents it from being displayed in the "Run analyses" menue of the Gui, this is not the case in the help messages displayed on the console. Hiding the parameter at both places would be great.
https://git.frama-c.com/pub/frama-c/-/issues/1275
Serial conversions in function result (csmith)
2021-02-22T13:25:42Z
Pascal Cuoq
Serial conversions in function result (csmith)
ID0000798:
**This issue was created automatically from Mantis Issue 798. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000798:
**This issue was created automatically from Mantis Issue 798. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000798 | Frama-C | Plug-in > Eva | public | 2011-04-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
short x = -10;
int y, z, t;
unsigned short f(void)
{
return x;
}
unsigned short g(void)
{
unsigned short l = *(unsigned short*)&x;
return l;
}
main(){
y = *(unsigned short*)&x;
z = f();
t = g();
}
y and z are computed correctly, but t is wrong:
[value] Values for function main:
y IN {65526; }
z IN {65526; }
t IN {-10; }
https://git.frama-c.com/pub/frama-c/-/issues/1276
12799, doubtful choice of promotion x86_64 mode (csmith)
2021-02-22T13:25:44Z
Pascal Cuoq
12799, doubtful choice of promotion x86_64 mode (csmith)
ID0000785:
**This issue was created automatically from Mantis Issue 785. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000785:
**This issue was created automatically from Mantis Issue 785. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000785 | Frama-C | Kernel | public | 2011-04-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
int x;
long x2;
unsigned long x9[6][2];
#if 0
#define d(n, v) Frama_C_show_each##n(v);
#else
#define d(n, v)
#endif
main(){
x2 = 2793414595;
for (int i = 0; i < 6; i++)
{
for (int j = 0; j < 2; j++)
x9[i][j] = 1U;
}
d(102, (0x090E7AF82577C8A6LL | x9[1][0]) )
d(103, (~(x2 || x9[1][0])) )
d(95, ((0x090E7AF82577C8A6LL | x9[0][1]) <= (~(x2 || x9[0][1]))))
x = ((0x090E7AF82577C8A6LL | x9[0][1]) <= (~(x2 || x9[0][1])));
return x;
}
~/ppc/bin/toplevel.opt -val -machdep x86_64 r.c -slevel 5000
...
[value] Values for function main:
x ? {0; }
BUT:
gcc -std=c99 r.c ; ./a.out ; echo $?
1
NOTE THAT:
~/ppc/bin/toplevel.opt -print -machdep x86_64 r.c [kernel] preprocessing with "gcc -C -E -I. r.c"
...
x = (0x090E7AF82577C8A6LL | (long long )x9[0][1]) <= (long long )(~ tmp);
}
return (x);
}
gcc is the computation server's, supposed to match x86_64.
x9[0][1] is an unsigned long. The promotion of the arguments of | seems to be wrong in Frama-C's front-end according to 6.3.1.8 (p 45), where the very last case of §1 seems to apply.
### Additional Information :
In addition to the computation server's GCC (version 4.4.3 (Ubuntu 4.4.3-4ubuntu5)), this one also predicts the result 1 for x when compiling with -m64:
gcc -m64 -v
Using built-in specs.
Target: powerpc-apple-darwin9
Configured with: /var/tmp/gcc/gcc-5493~1/src/configure --disable-checking -enable-werror --prefix=/usr --mandir=/share/man --enable-languages=c,objc,c++,obj-c++ --program-transform-name=/^[cg][^.-]*$/s/$/-4.0/ --with-gxx-include-dir=/include/c++/4.0.0 --with-slibdir=/usr/lib --build=i686-apple-darwin9 --program-prefix= --host=powerpc-apple-darwin9 --target=powerpc-apple-darwin9
Thread model: posix
gcc version 4.0.1 (Apple Inc. build 5493)
https://git.frama-c.com/pub/frama-c/-/issues/1277
typing rule of \old(tab) or tab[index] construct
2023-06-26T07:11:16Z
Patrick Baudin
typing rule of \old(tab) or tab[index] construct
ID0000761:
**This issue was created automatically from Mantis Issue 761. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000761:
**This issue was created automatically from Mantis Issue 761. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000761 | Frama-C | Kernel > ACSL implementation | public | 2011-03-22 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
\old(t)[0] is interpreted as \old((int*)t)[0] when t is a C variable declared as follow:
int t[10];
That raises a problem when using such constructs combined with \let constructs.
It is mainly accepted that
\old(\let x = t ; x)
is equivalent to
\let x = \old(t) ; x
That propagation rule implies the type of t should be the same than the type of \old(t).
That isn't the case with the current ACSL implementation:
\old(\let x = t ; x) has type int[10] and
\let x = \old(t) ; x has type int*
The issue is more significant on theses expressions
\old(\let x = t ; x)[0] and
(\let x = \old(t) ; x)[0].
So, is the problem with a typing rule or with the propagation rule.
https://git.frama-c.com/pub/frama-c/-/issues/1278
sliced program does not terminate (csmith)
2023-07-12T07:55:12Z
Pascal Cuoq
sliced program does not terminate (csmith)
ID0000807:
**This issue was created automatically from Mantis Issue 807. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000807:
**This issue was created automatically from Mantis Issue 807. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000807 | Frama-C | Plug-in > slicing | public | 2011-04-28 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
same conditions as bug 806.
Compile the original with gcc -m32 -D__FRAMAC -I runtime show_each.c noterm.c (executable terminates) and the sliced program with gcc -m32 show_each.c noterm.s.c
## Attachments
- [noterm.c](/uploads/ab1ab0534ff4c95890d574157583e87b/noterm.c)
https://git.frama-c.com/pub/frama-c/-/issues/1281
pretty-printed program rejected by GCC. Affects -print, slicing, scf (csmith)
2021-02-22T13:25:58Z
Pascal Cuoq
pretty-printed program rejected by GCC. Affects -print, slicing, scf (csmith)
ID0000810:
**This issue was created automatically from Mantis Issue 810. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000810:
**This issue was created automatically from Mantis Issue 810. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000810 | Frama-C | Kernel | public | 2011-05-02 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
$ cat const_field_return_struct.c
struct S {
const int f0;
int f1; } T, U;
struct S f(int c)
{
if (c) return T;
return U;
}
$ frama-c -quiet -print const_field_return_struct.c > t.c
$ cat t.c
/* Generated by Frama-C */
struct S {
int const f0 ;
int f1 ;
};
struct S T ;
struct S U ;
struct S f(int c )
{
struct S __retres ;
if (c) { __retres = T; goto return_label; }
__retres = U;
return_label: /* internal */
return (__retres);
}
$ gcc t.ct.c: In function 'f':
t.c:11: error: assignment of read-only variable '__retres'
t.c:12: error: assignment of read-only variable '__retres'
https://git.frama-c.com/pub/frama-c/-/issues/1282
unsoundness due to packed structs
2021-02-22T13:31:56Z
John Regher
unsoundness due to packed structs
ID0000719:
**This issue was created automatically from Mantis Issue 719. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000719:
**This issue was created automatically from Mantis Issue 719. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000719 | Frama-C | Kernel | public | 2011-02-13 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | regehr | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Analyzing the attached program like this:
toplevel.opt -val -slevel 14 foo_pp.c
Gives output including this:
g_113.f0 ? {2240865284; }
.f1 ? {-540177875780372926; }
.f2 ? {-1; }
.f3 ? {0; }
.f4 ? {-1; }
.[bits 184 to 191] ? UNINITIALIZED
.f5 ? {-1; }
.f6 ? {-5796648127719171460; }
g_113 is of type S0 which is declared using the pack(1) pragma, which makes all fields 1-byte aligned, so there should be no padding.
Not packing the struct properly causes Frama-C to have an incorrect impression about its layout.
Perhaps a very strongly-worded warning should appear in the output if the pack pragma is encountered in a program, but not honored.
## Attachments
- [foo_pp.c](/uploads/2fd6cb0469a80ccfba34bd381e921237/foo_pp.c)
https://git.frama-c.com/pub/frama-c/-/issues/1284
Comments parsing not always work
2021-02-22T14:04:22Z
mantis-gitlab-migration
Comments parsing not always work
ID0000691:
**This issue was created automatically from Mantis Issue 691. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000691:
**This issue was created automatically from Mantis Issue 691. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000691 | Frama-C | Kernel > ACSL implementation | public | 2011-01-27 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
/*@ lemma fib_3: fib(3) == 2; // proved automatically */
/*@ lemma fib_46: fib(46) == 1836311903; */
generates only one verification condition in jessie, i.e. for fig_46. However,
/*@ lemma fib_3: fib(3) == 2; */ /* proved automaticall */
/*@ lemma fib_46: fib(46) == 1836311903; */
works properly generating 2 VC, i.e. fib_3 and fib_46
https://git.frama-c.com/pub/frama-c/-/issues/1286
r13378, assertion failed with bit-fields
2021-02-22T14:04:22Z
Pascal Cuoq
r13378, assertion failed with bit-fields
ID0000817:
**This issue was created automatically from Mantis Issue 817. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000817:
**This issue was created automatically from Mantis Issue 817. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000817 | Frama-C | Kernel | public | 2011-05-10 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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 :
~/ppc/bin/toplevel.opt -cpp-command "gcc -C -E -I runtime" -machdep x86_64 noresult.10212234.10.c
[kernel] preprocessing with "gcc -C -E -I runtime noresult.10212234.10.c"
[kernel] error occurring when exiting Frama-C: stopping exit procedure.
The full backtrace is:
Called from file "cil/src/cil.ml", line 8478, characters 16-36
Called from file "cil/src/frontc/cabs2cil.ml", line 5565, characters 26-54
Called from file "cil/src/frontc/cabs2cil.ml", line 4923, characters 34-64
Called from file "cil/src/frontc/cabs2cil.ml", line 5843, characters 20-48
Called from file "cil/src/frontc/cabs2cil.ml", line 7477, characters 28-61
Called from file "cil/src/frontc/cabs2cil.ml", line 7382, characters 25-48
Called from file "list.ml", line 74, characters 24-34
Called from file "cil/src/frontc/cabs2cil.ml", line 7371, characters 9-1023
Called from file "cil/src/frontc/cabs2cil.ml", line 7495, characters 16-34
Called from file "cil/src/frontc/cabs2cil.ml", line 7557, characters 17-40
Called from file "cil/src/frontc/cabs2cil.ml", line 7382, characters 25-48
Called from file "list.ml", line 74, characters 24-34
Called from file "cil/src/frontc/cabs2cil.ml", line 7371, characters 9-1023
Called from file "cil/src/frontc/cabs2cil.ml", line 7052, characters 14-321
Called from file "cil/src/frontc/cabs2cil.ml", line 7930, characters 12-31
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/frontc/cabs2cil.ml", line 7962, characters 2-26
Called from file "cil/src/frontc/frontc.ml", line 171, characters 14-36
Called from file "src/kernel/file.ml", line 747, characters 27-46
Called from file "src/kernel/file.ml", line 796, characters 16-23
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 793, characters 6-318
Called from file "src/kernel/file.ml", line 1276, characters 12-30
Called from file "src/kernel/file.ml", line 1361, characters 4-27
Called from file "src/kernel/ast.ml", line 60, characters 2-28
Called from file "src/kernel/ast.ml", line 67, characters 53-71
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/cmdline.ml", line 174, characters 6-23
Unexpected error (File "cil/src/cil.ml", line 8462, characters 16-22: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Carbon-20110201+dev.
## Attachments
- [bitf.tgz](/uploads/6dc6db431037e3d03a34161b89af350f/bitf.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1287
using real function ( \max, \min, \abs ) instead of integer one in function c...
2023-09-06T14:10:43Z
mantis-gitlab-migration
using real function ( \max, \min, \abs ) instead of integer one in function contract
ID0000655:
**This issue was created automatically from Mantis Issue 655. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000655:
**This issue was created automatically from Mantis Issue 655. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000655 | Frama-C | Kernel > ACSL implementation | public | 2010-12-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
/*@
@ ensures \result == \max( a, b );
@ ensures \result != \min( a, b );
@ ensures a == \abs( a );
@*/
unsigned int
max( unsigned int a, unsigned int b )
{
int i = a > b ? a : b;
//@ assert i == \max( a, b );
return i;
}
Jessie output:
uint32 max(uint32 a, uint32 b)
behavior default:
ensures (C_8 : ((C_9 : (\result == \real_max(a, b))) &&
((C_11 : (\result != \real_min(a, b))) &&
(C_12 : (a == \real_abs(a))))));
I don't know exactly is it a bug or a feature.
## Attachments
- [max.c](/uploads/f369fbe09713900271c3103971ae67b4/max.c)
https://git.frama-c.com/pub/frama-c/-/issues/1288
r13417 unsigned bit-fields of width 32 should be promoted to unsigned int (cs...
2021-02-22T13:26:13Z
Pascal Cuoq
r13417 unsigned bit-fields of width 32 should be promoted to unsigned int (csmith)
ID0000823:
**This issue was created automatically from Mantis Issue 823. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000823:
**This issue was created automatically from Mantis Issue 823. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000823 | Frama-C | Kernel | public | 2011-05-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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 :
#include <stdio.h>
struct S { unsigned f:32; } x = { 28349};
unsigned short us = 0xDC23L;
main(){
int r = (x.f ^ ((short)-87)) >= us;
printf("%d\n", r);
return r;
}
gcc w.c && ./a.out
1
But:
~/ppc/bin/toplevel.opt -print w.c | grep -v preprocessing > w2.c && gcc w2.c && ./a.out
0
The front-end is correct in typing unsigned bit-fields as int most of the time, but there should be an exception for unsigned bit-fields of size 32. See http://stackoverflow.com/q/5977456/139746
https://git.frama-c.com/pub/frama-c/-/issues/1289
wrong interpretation when a bit-field receives the result of a function (csmith)
2021-02-22T13:26:14Z
Pascal Cuoq
wrong interpretation when a bit-field receives the result of a function (csmith)
ID0000819:
**This issue was created automatically from Mantis Issue 819. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000819:
**This issue was created automatically from Mantis Issue 819. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000819 | Frama-C | Plug-in > Eva | public | 2011-05-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
struct S { int b:31; } s;
int f(void)
{
return -1;
}
main(){
s.b = f();
Frama_C_dump_each();
}
[value] DUMPING STATE of file bitfield_receives_result.c line 10
s.b# ? {-1} misaligned 0%32
.[bits 31 to 31] ? {0}
=END OF DUMP==
https://git.frama-c.com/pub/frama-c/-/issues/1290
r13089 sliced program computes differently from original (csmith)
2021-02-22T13:32:04Z
Pascal Cuoq
r13089 sliced program computes differently from original (csmith)
ID0000808:
**This issue was created automatically from Mantis Issue 808. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000808:
**This issue was created automatically from Mantis Issue 808. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000808 | Frama-C | Plug-in > slicing | public | 2011-04-29 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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 :
~/ppc/bin/toplevel.opt -val-signed-overflow-alarms s.29114540.2.c -cpp-command "gcc -m32 -C -E -D__FRAMAC -I. -I$CSMITH/runtime " -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -print -ocode s.29114540.2.s.c
original compiled as 32-bit produces:
each: 1877464688
each: 923383238
each: 3118711398
each: 2770598846
each: 3750958151
each: 1873579612
each: 1348507732
each: 1348507732
sliced program produces:
each: 1877464688
each: 923383238
each: 3118711398
each: 2770598846
each: 130171288
each: 3207316278
each: 3201788839
each: 3201788839
It seems that the sliced program does not preserve the value of g_14 (see sequence of calls to transparent_crc() in main()).
## Attachments
- [di.tgz](/uploads/3bd5ec85502cf3eeeaa6791eeb439216/di.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1292
r13465, crash in slicing (csmith)
2023-09-29T10:40:22Z
Pascal Cuoq
r13465, crash in slicing (csmith)
ID0000825:
**This issue was created automatically from Mantis Issue 825. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000825:
**This issue was created automatically from Mantis Issue 825. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000825 | Frama-C | Plug-in > slicing | public | 2011-05-14 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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 :
Command: ~/ppc/bin/toplevel.opt -val-signed-overflow-alarms s.14013538.2.c -cpp-command "gcc -m32 -I runtime -D__FRAMAC -C -E " -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -print -ocode test.i
...
[slicing] exporting project to 'Slicing export'...
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[kernel] The full backtrace is:
Called from file "src/misc/filter.ml", line 406, characters 13-62
Called from file "src/kernel/visitor.ml", line 155, characters 17-23
Called from file "cil/src/cil.ml", line 7395, characters 5-86
Called from file "cil/src/cil.ml", line 6481, characters 13-16
Called from file "cil/src/cil.ml", line 7529, characters 16-40
Called from file "cil/src/cil.ml", line 6458, characters 21-41
Called from file "src/misc/filter.ml", line 404, characters 25-71
Called from file "src/kernel/visitor.ml", line 155, characters 17-23
Called from file "cil/src/cil.ml", line 7395, characters 5-86
Called from file "cil/src/cil.ml", line 6481, characters 13-16
Called from file "cil/src/cil.ml", line 7529, characters 16-40
Called from file "cil/src/cil.ml", line 6458, characters 21-41
Called from file "src/misc/filter.ml", line 512, characters 21-69
Called from file "src/misc/filter.ml", line 701, characters 13-25
Called from file "list.ml", line 57, characters 20-23
Called from file "src/misc/filter.ml", line 718, characters 23-59
Called from file "src/kernel/visitor.ml", line 186, characters 14-30
Called from file "cil/src/cil.ml", line 6512, characters 15-31
Called from file "cil/src/cil.ml", line 7787, characters 5-63
Called from file "cil/src/cil.ml", line 8125, characters 17-37
Called from file "cil/src/cil.ml", line 8132, characters 3-20
Called from file "cil/src/cil.ml", line 6458, characters 21-41
Called from file "src/kernel/file.ml", line 1294, characters 14-47
Called from file "src/kernel/file.ml", line 1326, characters 2-34
Called from file "src/misc/filter.ml", line 741, characters 14-71
Called from file "src/slicing/slicingTransform.ml", line 431, characters 4-69
Called from file "src/slicing/register.ml", line 1171, characters 6-61
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Unexpected error (File "src/misc/filter.ml", line 204, characters 15-21: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Carbon-20110201+dev.
Note that a version and a backtrace alone often does not have information
to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [c.tgz](/uploads/161af11e41b331cb433d14ff5a5b2365/c.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1295
r13586 Spurious "assert \separated(...)" (csmith)
2024-03-05T16:33:49Z
Pascal Cuoq
r13586 Spurious "assert \separated(...)" (csmith)
ID0000832:
**This issue was created automatically from Mantis Issue 832. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000832:
**This issue was created automatically from Mantis Issue 832. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000832 | Frama-C | Kernel | public | 2011-05-24 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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 :
file t.c:
int a, *G;
int g(int x, int y)
{
return x + y;
}
main(int c, char **v){
G = &a;
*G =
(a < (g((0U ||
(((a ^ a) <= a) < ((*G) || a))), 5)));
return a;
}
$ ~/ppc/bin/toplevel.byte -val -unspecified-access t.c
t.c:13:[kernel] warning: Unspecified sequence with side effect:
/* <- a G *G */
if (*G) { tmp = 1; } else { if (a) { tmp = 1; } else { tmp = 0; } }
/* <- a a a */
/* <- */
tmp_0 = g((((a ^ a) <= a) < tmp) != 0,5);
/* *G <- G a */
*G = a < tmp_0;
...
t.c:13:[kernel] warning: undefined multiple accesses in expression. assert \separated(G,& a);
t.c:13:[kernel] warning: undefined multiple accesses in expression. assert \separated(G,G);
...
The program is completely defined, g has no side-effects.
https://git.frama-c.com/pub/frama-c/-/issues/1296
r12436, unnecessary warning for side-effects (csmith)
2021-02-22T14:02:55Z
Pascal Cuoq
r12436, unnecessary warning for side-effects (csmith)
ID0000771:
**This issue was created automatically from Mantis Issue 771. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000771:
**This issue was created automatically from Mantis Issue 771. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000771 | Frama-C | Kernel | public | 2011-03-30 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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 :
The command below leads the value analysis to check whether *g_19 can be in alias with g_20. They can be, so the value analysis emits an alarm, but I fail to see why this should be checked. The functions called have no side-effects. In fact, there are no side-effects in the whole assignment, except the side-effect of the assignment.
This is likely to be related to 676: the display below is very strange, with some statements displayed as empty lines (and still having inputs !!).
__
bin/toplevel.opt -unspecified-access se.i
____
assert.30103607.7.c:632:[kernel] warning: Unspecified sequence with side effect:
/* <- */
tmp = safe_add_func_uint16_t_u_u(p_69.f2,(unsigned short )l_80);
/* <-
*/
tmp_0 = safe_lshift_func_uint8_t_u_u((unsigned char )p_70.f0,
(unsigned int )l_85);
/* <- p_70.f3 */
/* <-
*/
tmp_1 = safe_sub_func_uint32_t_u_u((unsigned int )l_90[0][0][1],
(unsigned int )*g_19);
/* <- */
tmp_2 = safe_sub_func_uint32_t_u_u(tmp_1,(unsigned int )p_70.f3);
/* <- l_80 g_14 */
/* <- */
tmp_3 = safe_rshift_func_int8_t_s_s((signed char )p_70.f3,g_20);
/* <- g_20 */
/* <-
*/
tmp_4 = safe_add_func_int8_t_s_s((signed char )((int )tmp_3 >= g_20),
(signed char )((long )(l_80 < (int32_t )g_14) <= 0xC7L));
/* <-
*/
tmp_5 = safe_add_func_int8_t_s_s(tmp_4,
(signed char )((uint32_t )((int )tmp != (int )tmp_0) <= tmp_2));
/* <- g_14 */
/* *g_19 <-
*/
*g_19 = (int32_t )safe_mul_func_int8_t_s_s((signed char )g_14,
(signed char )(1U != (unsigned int )tmp_5));
______
## Attachments
- [se.i](/uploads/7b3e9708421a0440524a591ed89764fd/se.i)
https://git.frama-c.com/pub/frama-c/-/issues/1303
Incorrect loop unrolling in presence of switch
2023-11-21T14:40:58Z
Boris Yakobowski
Incorrect loop unrolling in presence of switch
ID0000861:
**This issue was created automatically from Mantis Issue 861. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000861:
**This issue was created automatically from Mantis Issue 861. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000861 | Frama-C | Kernel | public | 2011-06-09 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | high | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Syntactic loop unrolling of loops containing while is completely wrong.
Can be checked with -print or -check on the code below.
void main () {
/*@ loop pragma UNROLL_LOOP 4; */
for (int i=0;i<4;i++) {
switch (i) {
case 1: break;
case 2: break;
case 3: break;
case 4: break;
default:
}
}
}
https://git.frama-c.com/pub/frama-c/-/issues/1304
emitted program computes differently from original (csmith)
2023-09-25T07:54:10Z
Pascal Cuoq
emitted program computes differently from original (csmith)
ID0000858:
**This issue was created automatically from Mantis Issue 858. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000858:
**This issue was created automatically from Mantis Issue 858. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000858 | Frama-C | Plug-in > semantic constant folding | public | 2011-06-08 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
cuoq@ns61143:~/csmith$ cat scf.08000752.exec
[value] Called Frama_C_show_each({8413297})
[value] Called Frama_C_show_each({3974178539})
[value] Called Frama_C_show_each({3974178539})
cuoq@ns61143:~/csmith$ ~/ppc/bin/toplevel.opt -val -cpp-command "gcc -C -E -I $CSMITH/runtime -D__FRAMAC " -slevel 50 -no-results-function crc32_gentab -semantic-const-folding -quiet -machdep x86_64 scf.08000752.c | ./selin.pl > scf.i
cuoq@ns61143:~/csmith$ gcc scf.i show_each-x86_64.o
cuoq@ns61143:~/csmith$ ./a.out
[value] Called Frama_C_show_each({8413297})
[value] Called Frama_C_show_each({844760584})
[value] Called Frama_C_show_each({844760584})
## Attachments
- [scf858.tgz](/uploads/c3c4881ae5ebdf358cd4154ca853f61e/scf858.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1305
Ocaml 32 bits version 3.11.0
2023-10-09T13:44:37Z
Patrick Baudin
Ocaml 32 bits version 3.11.0
ID0000857:
**This issue was created automatically from Mantis Issue 857. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000857:
**This issue was created automatically from Mantis Issue 857. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000857 | Frama-C | Kernel | public | 2011-06-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | patrick | **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 :
Problem with C enum value with the most significant bit set:
enum { KO=0x99996666u } v ;
This occurs on 32 bits platform and Ocaml 3.11.0
https://git.frama-c.com/pub/frama-c/-/issues/1307
sliced program computes differently from original (csmith)
2023-10-15T02:46:03Z
Pascal Cuoq
sliced program computes differently from original (csmith)
ID0000827:
**This issue was created automatically from Mantis Issue 827. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000827:
**This issue was created automatically from Mantis Issue 827. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000827 | Frama-C | Plug-in > slicing | public | 2011-05-18 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | high | **Severity** | minor | **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 :
The commands used and results obtained are in the included testslicing.sh
## Attachments
- [s.tgz](/uploads/d800ecc206e23ab4dc4eabc0c7747fb5/s.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1310
ACSL pretty-printer
2023-11-21T14:40:58Z
mantis-gitlab-migration
ACSL pretty-printer
ID0000859:
**This issue was created automatically from Mantis Issue 859. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000859:
**This issue was created automatically from Mantis Issue 859. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000859 | Frama-C | Kernel > ACSL implementation | public | 2011-06-09 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ckunz | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Inductive predicates are not printed correctly:
predicates of the form:
inductive .... ( ... ) {
case ...;
case ...;
}
are printed as:
predicate .... ( ... ) {
case ...;
case ...;
}
### Additional Information :
A quick fix consists of modifying cil/src/cil.ml as follows:
*** 5676,5682 ****
fprintf fmt "@[<hov 2>logic %a"
(self#pLogic_type None) rt
| None ->
! fprintf fmt "@[<hov 2>predicate"
end;
fprintf fmt " %a%a%a%a"
self#pLogic_var li.l_var_info
--- 5676,5688 ----
fprintf fmt "@[<hov 2>logic %a"
(self#pLogic_type None) rt
| None ->
! begin
! match li.l_body with
! | LBinductive _ ->
! fprintf fmt "@[<hov 2>inductive"
! | _ ->
! fprintf fmt "@[<hov 2>predicate"
! end
end;
fprintf fmt " %a%a%a%a"
self#pLogic_var li.l_var_info
https://git.frama-c.com/pub/frama-c/-/issues/1311
Cil generates incorrect switch (with missing cases)
2021-02-22T13:26:59Z
Boris Yakobowski
Cil generates incorrect switch (with missing cases)
ID0000882:
**This issue was created automatically from Mantis Issue 882. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000882:
**This issue was created automatically from Mantis Issue 882. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000882 | Frama-C | Kernel | public | 2011-07-06 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
frama-c -check crashes on the following code. This is a regression from Boron.
void main () {
int r;
switch(1) {
case 2:
r = (int) f(1);
break;
default:
break;
}
}
https://git.frama-c.com/pub/frama-c/-/issues/1312
Promotion from integer to boolean
2023-10-17T07:46:40Z
Julien Signoles
Promotion from integer to boolean
ID0000751:
**This issue was created automatically from Mantis Issue 751. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000751:
**This issue was created automatically from Mantis Issue 751. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000751 | Frama-C | Kernel > ACSL implementation | public | 2011-03-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
At this day, in the predicate or term "0 == !1", 0 is an integer while !1 is a boolean. Both members of the equality should have the same type (boolean). Thus a solution could be that the normalization translates "0 == !1" to "(0 == 0) == (0 == !1)".
https://git.frama-c.com/pub/frama-c/-/issues/1313
Crash du builtin memcpy, par une exception non rattrapable
2023-11-27T14:01:56Z
Boris Yakobowski
Crash du builtin memcpy, par une exception non rattrapable
ID0000883:
**This issue was created automatically from Mantis Issue 883. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000883:
**This issue was created automatically from Mantis Issue 883. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000883 | Frama-C | Plug-in > Eva | public | 2011-07-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **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 :
À analyser avec -val
extern unsigned int i;
char src[20];
char dst[10];
void main () {
if (i <= 10)
Frama_C_memcpy(dst+1, src, i);
}
### Additional Information :
svn 14142
https://git.frama-c.com/pub/frama-c/-/issues/1316
Results differ between value analysis and GCC on bitfields
2024-03-15T09:13:18Z
Benjamin Monate
Results differ between value analysis and GCC on bitfields
ID0000890:
**This issue was created automatically from Mantis Issue 890. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000890:
**This issue was created automatically from Mantis Issue 890. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000890 | Frama-C | Plug-in > Eva | public | 2011-07-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | pascal | **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 :
On the program
==bug.i==============
union U0 {
unsigned short f0 ;
int f1 ;
int f2 : 5 ;
unsigned char const f3 ;
};
unsigned short G0 ;
int G1 ;
int G2;
unsigned char G3 ;
union U0 G={(unsigned short)65532U};
int main() {
G0=G.f0;
G1=G.f1;
G2=G.f2;
G3=G.f3;
printf("%d %d %d %d : %d\n",G0,G1,G2,G3,G2==-4);
return (G2==-4);
}
=========================
frama-c -val bug.i
returns:
===
[value] Values for function main:
G0 ? {65532}
G1[bits 0 to 15] ? {65532}
[bits 16 to 31] ? {0}
G2 ? {28}
G3# ? {65532} misaligned 0%16
__retres ? {0}
===
but gcc bug.i && ./a.out ; echo $?
displays :
===
65532 65532 -4 252 : 1
1
===
They do not agree on the result nor on the value of G2.
https://git.frama-c.com/pub/frama-c/-/issues/1317
Typing error on expression array == pointer
2021-02-22T13:27:10Z
Patrick Baudin
Typing error on expression array == pointer
ID0000885:
**This issue was created automatically from Mantis Issue 885. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000885:
**This issue was created automatically from Mantis Issue 885. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000885 | Frama-C | Kernel > ACSL implementation | public | 2011-07-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
File:
extern int t1[10];
//@ requires t1 == \null;
void main(void) { ; }
is interpreted as:
extern int t1[10];
//@ requires (int *)t1 == (int []) \null;
void main(void) { ; }
Both operands of the equality have not the same type!
https://git.frama-c.com/pub/frama-c/-/issues/1318
error: label ‘__invalid_label’ used but not defined (csmith)
2021-02-22T13:43:06Z
Pascal Cuoq
error: label ‘__invalid_label’ used but not defined (csmith)
ID0000897:
**This issue was created automatically from Mantis Issue 897. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000897:
**This issue was created automatically from Mantis Issue 897. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000897 | Frama-C | Plug-in > slicing | public | 2011-07-28 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Je rapporte au plus vite pendant que c'est encore frais. Ça semble bien être un petit bug lié aux changements récents.
La commande de slicing était :
~/ppc/bin/toplevel.opt -val-signed-overflow-alarms -no-val-show-progress s.28172412.1.i -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -print -ocode s.28172412.1.s.c
Il y en a un deuxième qui est sorti pendant que je faisais l'archive et qui s'est glissé dedans. Le deuxième semble être un autre problème mais est trop gros pour être regardé, j'en trouverai un plus petit.
## Attachments
- [invalid_label.tgz](/uploads/e8999cfd4cef8cef37061908b9655b97/invalid_label.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1319
Warning for Axiom: From wp: Overloaded operator User defined axiom
2021-02-22T13:27:13Z
Patrick Baudin
Warning for Axiom: From wp: Overloaded operator User defined axiom
ID0000896:
**This issue was created automatically from Mantis Issue 896. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000896:
**This issue was created automatically from Mantis Issue 896. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000896 | Frama-C | Plug-in > wp | public | 2011-07-28 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Since there is no overloading is the source, the warning message has no sense!
### Additional Information :
> cat file.c
extern int tab[], x;
//@ axiomatic A { axiom ax: 10 < \block_length(tab); }
//@ assigns x;
extern void h(void);
//@ requires r2: x==0; assigns x;
void g() { h(); }
//@ requires r1: x==0;
void f(void) { g(); }
> frama-c -wp
...
file.c:8:[wp] warning: Warning for Axiom ax:
From wp: Overloaded operator User defined axiom ax{L} and User defined axiom ax
{L} not yet implemented
Effect: Ignored user-defined axiom 'ax'
https://git.frama-c.com/pub/frama-c/-/issues/1320
File "src/memory_state/lmap.ml", line 931, characters 22-28: Assertion failed
2021-02-22T13:42:52Z
Benjamin Monate
File "src/memory_state/lmap.ml", line 931, characters 22-28: Assertion failed
ID0000889:
**This issue was created automatically from Mantis Issue 889. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000889:
**This issue was created automatically from Mantis Issue 889. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000889 | Frama-C | Plug-in > Eva | public | 2011-07-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **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 :
frama-c /usr/local/share/frama-c/libc/fc_runtime.c main.i protocol.i util.i -val -quiet
crashes the value analysis.
## Attachments
- [main.i](/uploads/f310746c6649373aefea3edc9602f483/main.i)
- [util.i](/uploads/15ac5f03bcc13cfed5c759fbc47a64fc/util.i)
- [protocol.i](/uploads/9753b8a9322f329b2774dc0429fc793b/protocol.i)
https://git.frama-c.com/pub/frama-c/-/issues/1329
incorrect AST generated
2021-02-22T13:44:14Z
Pascal Cuoq
incorrect AST generated
ID0000911:
**This issue was created automatically from Mantis Issue 911. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000911:
**This issue was created automatically from Mantis Issue 911. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000911 | Frama-C | Kernel | public | 2011-08-04 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
short S;
int f(int x, int y)
{
return x+y;
}
int main (void) {
return f(1, S++);
}
Mini:~/ppc $ bin/toplevel.opt t.c -check
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:11:[kernel] failure: [AST Integrity Check] initial AST
in call tmp_0 = f(1,tmp);, arg tmp has type short instead of int
[kernel] error occurring when exiting Frama-C: stopping exit procedure.
The full backtrace is:
Raised at file "src/kernel/log.ml", line 509, characters 30-31
Called from file "src/kernel/log.ml", line 503, characters 9-16
Re-raised at file "src/kernel/log.ml", line 506, characters 15-16
Called from file "src/kernel/file.ml", line 639, characters 16-240
Called from file "cil/src/cil.ml", line 1410, characters 15-31
Called from file "cil/src/cil.ml", line 2258, characters 5-62
Called from file "cil/src/cil.ml", line 2384, characters 14-21
Called from file "cil/src/cil.ml", line 1356, characters 21-41
Called from file "cil/src/cil.ml", line 2302, characters 5-86
Called from file "cil/src/cil.ml", line 2331, characters 14-35
Called from file "cil/src/cil.ml", line 1379, characters 13-16
Called from file "cil/src/cil.ml", line 2329, characters 4-844
Called from file "cil/src/cil.ml", line 1356, characters 21-41
Called from file "cil/src/cil.ml", line 2302, characters 5-86
Called from file "cil/src/cil.ml", line 1379, characters 13-16
Called from file "cil/src/cil.ml", line 2436, characters 16-40
Called from file "cil/src/cil.ml", line 1356, characters 21-41
Called from file "cil/src/cil.ml", line 2649, characters 14-39
Called from file "cil/src/cil.ml", line 1356, characters 21-41
Called from file "cil/src/cil.ml", line 2624, characters 5-101
Called from file "cil/src/cil.ml", line 2700, characters 16-38
Called from file "cil/src/cil.ml", line 1379, characters 13-16
Called from file "cil/src/cil.ml", line 1424, characters 24-57
Called from file "cil/src/cil.ml", line 2694, characters 5-63
Called from file "cil/src/cil.ml", line 8221, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 8178, characters 3-30
Called from file "cil/src/cil.ml", line 8222, characters 2-368
Called from file "cil/src/cil.ml", line 1356, characters 21-41
Called from file "cil/src/cil.ml", line 8253, characters 7-84
Called from file "src/kernel/file.ml", line 1159, characters 35-147
Called from file "src/kernel/file.ml", line 1380, characters 4-27
Called from file "src/kernel/ast.ml", line 60, characters 2-28
Called from file "src/kernel/ast.ml", line 67, characters 53-71
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/cmdline.ml", line 174, characters 6-23
Frama-C aborted because of internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Carbon-20110201+dev.
Note that a version and a backtrace alone often does not have information
to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
Mini:~/ppc $
### Tags :
csmith
https://git.frama-c.com/pub/frama-c/-/issues/1330
Cil wrongly authorizes references to local variables in static arrays
2023-11-30T10:48:06Z
Boris Yakobowski
Cil wrongly authorizes references to local variables in static arrays
ID0000892:
**This issue was created automatically from Mantis Issue 892. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000892:
**This issue was created automatically from Mantis Issue 892. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000892 | Frama-C | Kernel | public | 2011-07-26 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
frama-c -check crashes on the following code.
int tab[16];
void* main(void)
{
int i;
static const int* t[] = {
&tab[1],
&tab[3],
&tab[4],
&i
};
return &t;
}
Declaring t as static causes Cil to lift the array to the global scope of the module, but this is incorrect because of &i. I think the program is incorrect in the first place, but Cil should reject it, instead of silently producing a wrong AST.
https://git.frama-c.com/pub/frama-c/-/issues/1334
Aggregate logic types containing only C types
2024-03-16T08:11:35Z
mantis-gitlab-migration
Aggregate logic types containing only C types
ID0000835:
**This issue was created automatically from Mantis Issue 835. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000835:
**This issue was created automatically from Mantis Issue 835. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000835 | Frama-C | Kernel > ACSL implementation | public | 2011-05-24 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | proux | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
According to section 2.2.7 of current ACSL implementation
documentation
http://frama-c.com/download/acsl-implementation-Carbon-20110201.pdf
it would be possible to use for example arrays of integers:
"Aggregate types can be declared in logic, and their contents may be any logic types themselves."
but when trying so, we got an error "not a C type".
Looking at type logic_type in cil/src/cil_types.mli
I understand that actually implementing what the documentation
says may require a non negligible amount of work
and I don't expect it anytime soon.
But putting a "not yet implemented" warning or something like that
in the implementation documentation would be nice.
https://git.frama-c.com/pub/frama-c/-/issues/1335
-sparecode-analysis option should have -sparecode alias
2021-02-22T13:27:47Z
Pascal Cuoq
-sparecode-analysis option should have -sparecode alias
ID0000947:
**This issue was created automatically from Mantis Issue 947. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000947:
**This issue was created automatically from Mantis Issue 947. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000947 | Frama-C | Plug-in > sparecode | public | 2011-09-02 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
This would be consistent with -value (for value analysis), -deps (for dependencies analysis), ...
https://git.frama-c.com/pub/frama-c/-/issues/1339
-semantic-const-folding should have a -semantic-constant-folding alias
2021-02-22T13:27:53Z
Pascal Cuoq
-semantic-const-folding should have a -semantic-constant-folding alias
ID0000946:
**This issue was created automatically from Mantis Issue 946. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000946:
**This issue was created automatically from Mantis Issue 946. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000946 | Frama-C | Plug-in > semantic constant folding | public | 2011-09-02 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | monate | **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 :
Thanks for saving the user from typing the 4 letters, but why not -sem-constant-folding or -semantic-constant-fold?
https://git.frama-c.com/pub/frama-c/-/issues/1341
Sliced program computes differently from original (csmith)
2021-02-22T13:28:01Z
Pascal Cuoq
Sliced program computes differently from original (csmith)
ID0000963:
**This issue was created automatically from Mantis Issue 963. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000963:
**This issue was created automatically from Mantis Issue 963. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000963 | Frama-C | Plug-in > slicing | public | 2011-09-14 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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 :
Bon, j'ai peut-être un peu perdu la main, alors il faudra m'excuser si je rapporte un non-problème, ou si j'oublie des détails au début.
L'architecture cible est maintenant -machdep x86_64 (on a maintenant confiance dans l'analyse de valeurs sur cette architecture).
La commande de slicing utilisée est dans le script slice_src_dest.sh
Pour compiler l'original ou le programme slicé:
gcc -Iruntime s.14134425.9.c show_each.c -o orig
gcc -Iruntime s.14134425.9.s.c show_each.c -o slice
(c'est un gcc 64-bit)
J'obtiens les fichiers .exec et .execs, qui sont différents.
## Attachments
- [s.tgz](/uploads/8dc2871ac9a879a06b4b6efacd7a8fe6/s.tgz)
- [s.c](/uploads/0cf5e56fd9b3ae9cfd85b89dfb29e7d7/s.c)
https://git.frama-c.com/pub/frama-c/-/issues/1342
Wrong AST (csmith)
2021-02-22T14:03:00Z
Pascal Cuoq
Wrong AST (csmith)
ID0000933:
**This issue was created automatically from Mantis Issue 933. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000933:
**This issue was created automatically from Mantis Issue 933. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000933 | Frama-C | Kernel | public | 2011-08-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **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 :
Mini:~/d $ cat r.c
int g_18;
typedef unsigned int uint32_t;
typedef int int32_t;
typedef short int16_t;
typedef long long int64_t;
struct S0 {
uint32_t f0;
int16_t f1;
signed f2 : 26;
int64_t f3;
};
union U3 {
signed f0 : 7;
int32_t f1;
int32_t f2;
struct S0 f3;
};
static union U3 g_7[1] = {{0x00868BB4L}};
int g_5;
int g_2;
void Frama_C_show_each(unsigned);
main(){
unsigned short l_8 = 1UL;
unsigned int l_16 = 0xBD4AA41AL;
g_2 |= (g_7[g_5].f3.f2 = l_16);
Frama_C_show_each(g_2);
}
Mini:~/d $ ~/ppc/bin/toplevel.opt -val -slevel 99 r.c | grep each
[value] Called Frama_C_show_each({3175785498})
Mini:~/d $ clang -m32 r.c show_each.c && ./a.out
r.c:29:1: warning: type specifier missing, defaults to 'int' [-Wimplicit-int]
main(){
^
1 warning generated.
[value] Called Frama_C_show_each({21668890})
Mini:~/d $ ~/ppc/bin/toplevel.opt -print r.c
[kernel] preprocessing with "gcc -C -E -I. r.c"
r.c:34:[kernel] warning: Body of function main falls-through. Adding a return statement
/* Generated by Frama-C */
typedef unsigned int uint32_t;
typedef int int32_t;
typedef short int16_t;
typedef long long int64_t;
struct S0 {
uint32_t f0 ;
int16_t f1 ;
int f2 : 26 ;
int64_t f3 ;
};
union U3 {
int f0 : 7 ;
int32_t f1 ;
int32_t f2 ;
struct S0 f3 ;
};
int g_18;
static union U3 g_7[1] = {{(int)0x00868BB4L}};
int g_5;
int g_2;
extern void Frama_C_show_each(unsigned int);
int main(void)
{
int __retres;
unsigned short l_8;
unsigned int l_16;
int __attribute__((__FRAMA_C_BITFIELD_SIZE__(26))) tmp;
l_8 = (unsigned short)1UL;
l_16 = (unsigned int)0xBD4AA41AL;
{ /*undefined sequence*/
tmp = (int)l_16;
g_7[g_5].f3.f2 = tmp;
g_2 |= tmp;
}
Frama_C_show_each((unsigned int)g_2);
__retres = 0;
return (__retres);
}
The program displayed with -print is not equivalent to the original because __attribute__((__FRAMA_C_BITFIELD_SIZE__(26))) in the declaration of tmp does not have any semantics.
https://git.frama-c.com/pub/frama-c/-/issues/1349
failure: bad initialisation: Too many initializations of the AST
2021-02-22T13:45:13Z
Patrick Baudin
failure: bad initialisation: Too many initializations of the AST
ID0000954:
**This issue was created automatically from Mantis Issue 954. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000954:
**This issue was created automatically from Mantis Issue 954. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000954 | Frama-C | Plug-in > metrics | public | 2011-09-09 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Crash with option -metrics -metrics-ast cabs when applied on project built by another (i.e. volatile and slicing) plug-in.
### Additional Information :
Revision: 15055
> cat file.c
int v;
int main(int x) {
v=x;
return v;
}
>frama-c -slice-return main file.c -then-on "Slicing export" -metrics -metrics-ast cabs
[kernel] failure: bad initialisation: Too many initializations of the AST
[kernel] The full backtrace is:
...
Called from file "src/metrics/metrics_cabs.ml", line 557, characters 21-44
...
https://git.frama-c.com/pub/frama-c/-/issues/1350
Unexpected label Old in pre : ignored annotation
2021-02-22T13:32:30Z
mantis-gitlab-migration
Unexpected label Old in pre : ignored annotation
ID0000979:
**This issue was created automatically from Mantis Issue 979. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000979:
**This issue was created automatically from Mantis Issue 979. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000979 | Frama-C | Plug-in > wp | public | 2011-10-05 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
A precondition using a user predicate is ignored by wp because of an Old label, but there isn't any label in it :
int bound = 0;
//@ predicate Bok{L} (integer n) = 0 <= bound < n;
/*@ behavior ok:
assumes x > 0;
requires Bok (3);
ensures Bok (5);
assigns bound;
*/
int f (int x);
void g (void) {
int x = f(3);
//@ assert P: bound < 20;
}
The command is : frama-c -wp-fct g -wp-prop P bug.c
The precondition : requires Bok{Pre} (3); gives the same error.
https://git.frama-c.com/pub/frama-c/-/issues/1353
Some functions lose their formals after File.create_project_from_visitor
2021-02-22T13:28:27Z
mantis-gitlab-migration
Some functions lose their formals after File.create_project_from_visitor
ID0001073:
**This issue was created automatically from Mantis Issue 1073. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001073:
**This issue was created automatically from Mantis Issue 1073. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001073 | Frama-C | Kernel | public | 2012-01-27 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
When a function is defined but not declared, it loses its formal arguments when creating a new project with [File.create_project_from_visitor].
The problem is that [Cil.setFormalsDecl] is not called for these functions in the generated project.
### Additional Information :
A simple way to experiment is to use Filter with a parameter that makes everything visible (I have sent such a mini-plug-in to Virgile and Boris).
In the generated project, we can see with [-then-on newproj -print] that these functions have lost their formals.
Moreover, [Cil.getFormalsDecl fundec.svar] raises Not_found on these [fundec].
I haven't found where this should be fixed (File ? Globals.Functions ? ...), but a workaround is to call [Cil.setFormalsDecl] afterward on such functions (ugly, but working !).
https://git.frama-c.com/pub/frama-c/-/issues/1354
Loop unrolling sub-optimal in presence of some labels
2021-02-22T13:28:29Z
Boris Yakobowski
Loop unrolling sub-optimal in presence of some labels
ID0001100:
**This issue was created automatically from Mantis Issue 1100. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001100:
**This issue was created automatically from Mantis Issue 1100. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001100 | Frama-C | Kernel | public | 2012-02-18 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Repro case :
-------------------p.c---------------
void main () {
int x = 0;
L:
while(x < 4) { x++; }
}
-------------------------------------
frama-c -ulevel 2 -print p.c results in
void main(void)
{
int x;
x = 0;
if (! (x < 4)) { goto unrolling_2_loop; }
x ++;
unrolling_4_loop: /* internal */ ;
if (! (x < 4)) { goto unrolling_2_loop; }
x ++;
unrolling_3_loop: /* internal */ ;
L:
while (x < 4) { x ++; }
unrolling_2_loop: /* internal */ ;
return;
}
The loop is unrolled before the label L. This is not incorrect per se, and even seems to be ok inside 'switch'. However, this will rarely be what the user expects and needs.
https://git.frama-c.com/pub/frama-c/-/issues/1355
Crash when parsing an incorrect program with pointer to arrays
2021-02-22T13:32:49Z
Boris Yakobowski
Crash when parsing an incorrect program with pointer to arrays
ID0001099:
**This issue was created automatically from Mantis Issue 1099. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001099:
**This issue was created automatically from Mantis Issue 1099. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001099 | Frama-C | Kernel | public | 2012-02-18 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | low | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
frama-c crashes on the following program
typedef int t[10];
typedef int u[4];
void main () {
int tab1[4];
u* p = &tab1;
t* p2 = (t) p;
}
https://git.frama-c.com/pub/frama-c/-/issues/1356
Handling error in external plug-in through --enable-external
2021-02-22T13:28:33Z
Julien Signoles
Handling error in external plug-in through --enable-external
ID0001069:
**This issue was created automatically from Mantis Issue 1069. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001069:
**This issue was created automatically from Mantis Issue 1069. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001069 | Frama-C | Kernel > configure | public | 2012-01-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Running './configure --enable-external=my_plugin_path' does not fail if the configure of the external plug-in fails. Worse the detection of this plug-in succeeds, so 'make' will try to compile it.
https://git.frama-c.com/pub/frama-c/-/issues/1357
Crash with multiple incompatible declarations
2021-02-22T13:32:35Z
Pascal Cuoq
Crash with multiple incompatible declarations
ID0000990:
**This issue was created automatically from Mantis Issue 990. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000990:
**This issue was created automatically from Mantis Issue 990. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000990 | Frama-C | Kernel | public | 2011-10-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
~/ppc/bzip2-1.0.6 $ cat f1.c
char s[100];
void perror(const char *);
void f(void){
perror(s);
}
~/ppc/bzip2-1.0.6 $ cat f2.c
char *s;
void perror(const char *);
void g(void){
perror(s);
}
~/ppc/bzip2-1.0.6 $ ~/ppc/bin/toplevel.opt f2.c f1.c
[kernel] warning: cannot load 4 plug-ins (incompatible with Nitrogen-20111001+dev).
Aorai; Obfuscator; Security_slicing;
Wp
[kernel] preprocessing with "gcc -C -E -I. f2.c"
[kernel] preprocessing with "gcc -C -E -I. f1.c"
f2.c:1:[kernel] warning: Incompatible declaration for s (included from f2.c). Previous was at f1.c:1
(include from f1.c) (different type constructors: char [100] vs. char *)]
f1.c:6:[kernel] failure: typeOf: StartOf on a non-array
[kernel] error occurring when exiting Frama-C: stopping exit procedure.
The full backtrace is:
Raised at file "src/kernel/log.ml", line 509, characters 30-31
Called from file "src/kernel/log.ml", line 503, characters 9-16
Re-raised at file "src/kernel/log.ml", line 506, characters 15-16
Called from file "cil/src/mergecil.ml", line 1643, characters 36-48
Called from file "cil/src/cil.ml", line 2256, characters 12-53
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2395, characters 38-57
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 1534, characters 24-57
Called from file "cil/src/cil.ml", line 2380, characters 5-52
Called from file "cil/src/cil.ml", line 2506, characters 14-21
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2424, characters 5-86
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 2558, characters 16-40
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2771, characters 14-39
Called from file "cil/src/cil.ml", line 1466, characters 21-41
Called from file "cil/src/cil.ml", line 2746, characters 5-91
Called from file "cil/src/cil.ml", line 2822, characters 16-38
Called from file "cil/src/cil.ml", line 1489, characters 13-16
Called from file "cil/src/cil.ml", line 1534, characters 24-57
Called from file "cil/src/cil.ml", line 2816, characters 5-53
Called from file "cil/src/mergecil.ml", line 2181, characters 11-41
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/mergecil.ml", line 2465, characters 2-38
Called from file "cil/src/mergecil.ml", line 2612, characters 22-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/mergecil.ml", line 2612, characters 2-61
Called from file "src/kernel/file.ml", line 830, characters 20-56
Called from file "src/kernel/file.ml", line 1327, characters 12-30
Called from file "src/kernel/file.ml", line 1412, characters 4-27
Called from file "src/kernel/ast.ml", line 64, characters 2-28
Called from file "src/kernel/ast.ml", line 71, characters 53-71
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/cmdline.ml", line 174, characters 6-23
Frama-C aborted because of internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Nitrogen-20111001+dev.
Note that a version and a backtrace alone often does not have information
to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
~/ppc/bzip2-1.0.6 $
### Additional Information :
I think it would be ok just to be stricter for multiple incompatible declarations.
https://git.frama-c.com/pub/frama-c/-/issues/1358
Wrong [\valid(p)] outside the pointed variable scope
2021-02-22T13:32:33Z
mantis-gitlab-migration
Wrong [\valid(p)] outside the pointed variable scope
ID0000986:
**This issue was created automatically from Mantis Issue 986. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000986:
**This issue was created automatically from Mantis Issue 986. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000986 | Frama-C | Plug-in > wp | public | 2011-10-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
The following assertion is said to be true, but it shouldn't :
void main (void) {
int * p;
{ int x;
p = &x;
}
/*@ assert \valid(p); */
}
https://git.frama-c.com/pub/frama-c/-/issues/1359
\valid_range not mentioned in Acsl manual
2021-02-22T13:33:03Z
Jochen Burghardt
\valid_range not mentioned in Acsl manual
ID0001023:
**This issue was created automatically from Mantis Issue 1023. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001023:
**This issue was created automatically from Mantis Issue 1023. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001023 | Frama-C | Documentation > ACSL | public | 2011-11-18 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
In the manual "ACSL: ANSI/ISO C Specification Language Version 1.5", \valid_range is not mentioned.
On p.70, it says " the ACSL built-in predicate \valid (p) is now equivalent to \validrange (p,0,0)." where the "_" seems to be missing.
No other occurrences of "\valid" followed by "range" could be found using my pdf search button.
https://git.frama-c.com/pub/frama-c/-/issues/1360
Missing or misleading warnings when merging two functions
2021-02-22T13:32:39Z
Boris Yakobowski
Missing or misleading warnings when merging two functions
ID0000999:
**This issue was created automatically from Mantis Issue 999. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000999:
**This issue was created automatically from Mantis Issue 999. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000999 | Frama-C | Kernel | public | 2011-10-24 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **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 complain in the right way when parsing the following code:
- there is no warning for the types, even though the return types are not compatible
- the warning "found two default behaviors, merging them" is not really intuitive for the user, as he has not written "behavior" anywhere.
//@ assigns \nothing;
int foo(int* p);
//@ ensures 0 <= \result < 25;
unsigned short foo()
{
return 0;
}
https://git.frama-c.com/pub/frama-c/-/issues/1361
Incorrect dependencies in presence of declared functions
2021-02-22T13:28:42Z
Boris Yakobowski
Incorrect dependencies in presence of declared functions
ID0000993:
**This issue was created automatically from Mantis Issue 993. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000993:
**This issue was created automatically from Mantis Issue 993. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000993 | Frama-C | Plug-in > from | public | 2011-10-20 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **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 :
Consider the following code
//@ assigns *p \from \nothing;
void f(int *p);
void main () {
int x = 0;
int y = 0;
f(&x);
f(&y);
}
Slicing the program on x results on keeping only y and the call f(&y), instead of the instructions related to x. (However, the result is correct with -calldeps.)
https://git.frama-c.com/pub/frama-c/-/issues/1362
code annotation placed above a local declaration are not correctly handled
2021-02-22T13:28:44Z
Virgile Prevosto
code annotation placed above a local declaration are not correctly handled
ID0001009:
**This issue was created automatically from Mantis Issue 1009. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001009:
**This issue was created automatically from Mantis Issue 1009. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001009 | Frama-C | Kernel > ACSL implementation | public | 2011-11-04 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
with the attached file.i, frama-c -check file.i crashes. Apparently local x is not put in the appropriate block.
### Additional Information :
If you replace the assert with an ensures (arguably a function contract in this place does not mean anything), it is silently discarded.
## Attachments
- [file.i](/uploads/a88c569413cf827b5c301aa038732516/file.i)
https://git.frama-c.com/pub/frama-c/-/issues/1363
Kernel should desugar "complete behaviors"
2021-02-22T14:03:02Z
Boris Yakobowski
Kernel should desugar "complete behaviors"
ID0001006:
**This issue was created automatically from Mantis Issue 1006. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001006:
**This issue was created automatically from Mantis Issue 1006. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001006 | Frama-C | Kernel | public | 2011-11-02 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Currently, the kernel does not transform "complete behaviors;" clauses into "complete behaviors b1 ... bn;" when it sees one. However, this would be worthwhile:
- it makes life simpler for all the plugins, that have one less case to handle
- if someone adds some named behaviors programmatically, the "complete behaviors;" clause becomes less precise.
https://git.frama-c.com/pub/frama-c/-/issues/1364
-cpp-extra-args option should be a list
2021-02-22T13:42:57Z
mantis-gitlab-migration
-cpp-extra-args option should be a list
ID0001132:
**This issue was created automatically from Mantis Issue 1132. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001132:
**This issue was created automatically from Mantis Issue 1132. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001132 | Frama-C | Kernel | public | 2012-03-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
The "-cpp-extra-args" option is a StringSet option. It seems to me that is should better be a list since the order might be important...
### Additional Information :
With the following script:
=============================================
let main () =
Kernel.CppExtraArgs.add "-Ilib1";
Kernel.CppExtraArgs.add "-Ilib2";
Kernel.Files.set [ "tests/test.c" ];
()
let main : unit -> unit =
Dynamic.register ~plugin:"Frama_c_journal" "main"
(Datatype.func Datatype.unit Datatype.unit)
~journalize:false main
let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()
=============================================
You always get :
[kernel] preprocessing with "gcc -C -E -I. -Ilib2 -Ilib1 tests/test.c"
whatever the order of the [Kernel.CppExtraArgs.add] commands is.
https://git.frama-c.com/pub/frama-c/-/issues/1367
unrolling loop statements with labels into there annotations are not handled ...
2021-02-22T13:28:52Z
Patrick Baudin
unrolling loop statements with labels into there annotations are not handled correctly (in conjunction with -ulevel)
ID0001135:
**This issue was created automatically from Mantis Issue 1135. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001135:
**This issue was created automatically from Mantis Issue 1135. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001135 | Frama-C | Kernel | public | 2012-03-27 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Fresh labels and correct gotos are introduced when unrolling loop statements,
but labels into code annotations are not handled correctly.
Into the given example, the assertion is not unrolled correctly.
### Additional Information :
> cat file.c
int X ;
void main (int c) {
for (int i = 0 ; i < 10 ;) {
if (c) goto there ;
X++;
there: i++;
//@ assert c==0 ==> \at(X,there)==i+1;
}
}
> frama-c file.c -ulevel 1 -print
int X;
void main(int c)
{
int i;
i = 0;
if (! (i < 10)) { goto unrolling_2_loop; }
if (c) { goto there_unrolling_4_loop; }
X ++;
there_unrolling_4_loop: /* internal */ i ++;
/*@ assert c ? 0 ? \at(X,there) ? i+1; */ ;
unrolling_3_loop: /* internal */ ;
while (i < 10) {
if (c) { goto there; }
X ++;
there: i ++;
/*@ assert c ? 0 ? \at(X,there) ? i+1; */ ;
}
unrolling_2_loop: /* internal */ ;
return;
}
https://git.frama-c.com/pub/frama-c/-/issues/1368
17514, -unspecified-access and if (*p = (*p < 3)) (csmith)
2024-03-12T17:06:13Z
Pascal Cuoq
17514, -unspecified-access and if (*p = (*p < 3)) (csmith)
ID0001114:
**This issue was created automatically from Mantis Issue 1114. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001114:
**This issue was created automatically from Mantis Issue 1114. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001114 | Frama-C | Kernel | public | 2012-03-10 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
In the program below, line 6 is as innocuous as line 5, but:
$ bin/toplevel.opt -val -unspecified-access t.c
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:6:[kernel] warning: Unspecified sequence with side effect:
/* <- *p p */
tmp = *p < 3;
/* *p <- tmp p */
*p = tmp;
...
t.c:6:[kernel] warning: undefined multiple accesses in expression. assert \separated(p, p);;
int x, *p;
main(){
p = &x;
*p = (*p < 3);
if (*p = (*p < 3))
x = 4;
}
https://git.frama-c.com/pub/frama-c/-/issues/1369
Preprocessing code may yield expanded code with undeclared variables
2021-02-22T13:28:55Z
mantis-gitlab-migration
Preprocessing code may yield expanded code with undeclared variables
ID0001113:
**This issue was created automatically from Mantis Issue 1113. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001113:
**This issue was created automatically from Mantis Issue 1113. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001113 | Frama-C | Kernel | public | 2012-03-08 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pkarpman | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Some variables introduced by Frama-C during the preprocessing phase (i.e. the result of "frama-c -print") may not be declared (thus yielding incorrect code).
A simple example where this occurs is when declaring arrays with variable size, e.g.:
int k[2*rounds];
is transformed as
int *k;
__lengthofk = (unsigned int)(2 * rounds);
k = (int *)__builtin_alloca(sizeof(*k) * __lengthofk);
with __lengthofk being left undeclared.
See attached file for a (complete) simple example.
HOW TO REPRODUCE:
Preprocess code with e.g. a variable-sized array declaration. This is however not the only case where this seem to happen.
EXPECTED BEHAVIOUR:
In this example, declaration of __lengthofk as unsigned int.
### Additional Information :
Might be a regression from Carbon.
I have scripts (that I didn't write myself, though, so I may not use them properly) that first preprocess C programs with Frama-C before using again Frama-C on the `expanded' code.
I don't think the previous user of those scripts had any problems with missing declarations when using them on Frama-C B & C, and yet they pretty much always fail for me when using Frama-C N (but succeed when I manually add the missing declarations).
## Attachments
- [nodec.c](/uploads/26238ce53b703d51dd4c366e32c7cfee/nodec.c)
https://git.frama-c.com/pub/frama-c/-/issues/1370
[Globals.Vars.get_astinfo] doesn't work
2021-02-22T13:32:37Z
mantis-gitlab-migration
[Globals.Vars.get_astinfo] doesn't work
ID0001136:
**This issue was created automatically from Mantis Issue 1136. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001136:
**This issue was created automatically from Mantis Issue 1136. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001136 | Frama-C | Kernel | public | 2012-03-27 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
[Globals.Vars.get_astinfo] compares variable names instead of using [Varinfo.equal], so it gives erroneous results.
### Additional Information :
int f (int x) { return x; }
int g (int x) { return x; }
int h (int x) { return x; }
$ frama-c -load-script script.ml toto.c
found variable vid:363 formal in f
found variable vid:367 formal in g
found variable vid:371 formal in h
[do_v] vid:371 formal in f
[do_v] vid:367 formal in f
[do_v] vid:363 formal in f
## Attachments
- [script.ml](/uploads/ad5f431aef42b958a0c6518d3f383f25/script.ml)
https://git.frama-c.com/pub/frama-c/-/issues/1371
AST check failure : problem with generated block-local variables
2021-02-22T13:28:59Z
mantis-gitlab-migration
AST check failure : problem with generated block-local variables
ID0001126:
**This issue was created automatically from Mantis Issue 1126. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001126:
**This issue was created automatically from Mantis Issue 1126. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001126 | Frama-C | Kernel | public | 2012-03-20 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pherrmann | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
On submitted file :
frama-c -check failchek.c
produces
failcheck.c:40:[kernel] failure: [AST Integrity Check] initial AST
In function _gnutls_epoch_set_cipher_suite, variable tmp_0 is supposed to be local to a block but not mentioned in function's locals.
[kernel] error occurring when exiting Frama-C: stopping exit procedure.
Also, use of
frama-c failcheck -print -then -check
does not produce the problem, while
frama-c failcheck.c -then -check
does, thus -print seems to have an unintended side-effect.
## Attachments
- [failcheck.c](/uploads/6866395d6e59393e99b62901bc0f8881/failcheck.c)
https://git.frama-c.com/pub/frama-c/-/issues/1372
unrolling labeled loops
2021-02-22T13:29:01Z
Patrick Baudin
unrolling labeled loops
ID0001139:
**This issue was created automatically from Mantis Issue 1139. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001139:
**This issue was created automatically from Mantis Issue 1139. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001139 | Frama-C | Kernel | public | 2012-04-02 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
foward gotos to unrolled loop are transformed into goto to undefined labels.
### Additional Information :
> cat file
void g (int j) {
if (j==0) goto zero;
return;
zero:
//@ loop pragma UNROLL_LOOP 3;
while (j<5) {j++;}
}
> frama-c -print file.c
https://git.frama-c.com/pub/frama-c/-/issues/1373
axiom outside axiomatic tacitly ignored in presence of struct
2021-02-22T13:29:03Z
Jochen Burghardt
axiom outside axiomatic tacitly ignored in presence of struct
ID0001116:
**This issue was created automatically from Mantis Issue 1116. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001116:
**This issue was created automatically from Mantis Issue 1116. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001116 | Frama-C | Kernel | public | 2012-03-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Running frama-c -wp on the attached program doesn't produce a syntax error message, although using "axiom" outside "axiomatic" is incorrect.
However, the axiom is not given to the provers: alt-ergo can't verify the program, but it will verify it if "axiom" is changed to "lemma" (in that case, the lemma is given to alt-ergo).
If the struct in line 6-8 is removed, a syntax error is reported as expected (however at EOF position, which seems too late).
## Attachments
- [ftest.c](/uploads/4bad9fc2f463ca90b2897af3885d3f34/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1374
Bad AST generation ?
2021-02-22T13:29:05Z
mantis-gitlab-migration
Bad AST generation ?
ID0001142:
**This issue was created automatically from Mantis Issue 1142. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001142:
**This issue was created automatically from Mantis Issue 1142. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001142 | Frama-C | Plug-in > Eva | public | 2012-04-04 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pherrmann | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
See program attached: it is accepted as correct (-check passes) but rejected later on (cf. value analysis crashes on it).
## Attachments
- [e.c](/uploads/3efaa42532fa642b0a57d167949b412f/e.c)
https://git.frama-c.com/pub/frama-c/-/issues/1376
17944 using option -unspecified-access, no alarm for x + (x=0)
2021-02-22T13:29:09Z
Pascal Cuoq
17944 using option -unspecified-access, no alarm for x + (x=0)
ID0001144:
**This issue was created automatically from Mantis Issue 1144. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001144:
**This issue was created automatically from Mantis Issue 1144. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001144 | Frama-C | Kernel | public | 2012-04-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
On the program below, with bin/toplevel.opt -val -unspecified-access t.c, it would be desireable to have an alarm. Instead, the return value is computed as zero.
int main(void) { int d = 5; return d + (d=0);
}
https://git.frama-c.com/pub/frama-c/-/issues/1378
PLUGIN_LINK_GUI_OFLAGS not used ?
2021-02-22T13:29:13Z
mantis-gitlab-migration
PLUGIN_LINK_GUI_OFLAGS not used ?
ID0001145:
**This issue was created automatically from Mantis Issue 1145. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001145:
**This issue was created automatically from Mantis Issue 1145. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001145 | Frama-C | Kernel > Makefile | public | 2012-04-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
It seems that the variables PLUGIN_LINK_GUI_BFLAGS and PLUGIN_LINK_GUI_OFLAGS that can be defined in plug-ins Makefile are not used in Makefile.plugin.
In $(TARGET_GUI_CMXS) I managed to change :
$(OCAMLOPT) -o $@ -shared $^
into
$(OCAMLOPT) -o $@ -shared $($(basename $(notdir $@))_OFLAGS) \
$($(basename $(notdir $@))_gui_TARGET_GUI_OFLAGS) \
$^
to make it work in my plug-in,
but I guess that there are other modifications to do...
https://git.frama-c.com/pub/frama-c/-/issues/1379
Emitted assertion wrongly reduces to bottom (apparently) (csmith)
2021-02-22T13:29:18Z
Pascal Cuoq
Emitted assertion wrongly reduces to bottom (apparently) (csmith)
ID0001024:
**This issue was created automatically from Mantis Issue 1024. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001024:
**This issue was created automatically from Mantis Issue 1024. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001024 | Frama-C | Plug-in > Eva | public | 2011-11-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | Frama-C Oxygen-20120901 | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Soundness bug, probably caused by wrong reduction on emitted assertions.
~/ppc/bin/toplevel.opt -slevel 5 -slevel-function main:0 -no-results -val-signed-overflow-alarms -cpp-command "gcc -C -E -Iruntime -m32 " a.c -precise-unions -val
...
a.c:236:[value] Assertion got status invalid (stopping propagation).
[value] Recording results for func_1
[value] Done for function func_1
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
L'analyse avec -slevel 5 dit que la fin du programme et le Frama_C_dump... n'est pas atteint. Pourtant, il l'est comme le montre l'analyse avec -slevel 5000000:
~/ppc/bin/toplevel.opt -slevel 5000000 -slevel-function main:0 -no-results -val-signed-overflow-alarms -cpp-command "gcc -C -E -Iruntime -m32 " a.c -precise-unions -val
...
&& *(unsigned short*)&g_1113 == 65535)
End of Frama_C_dump_assert_each output
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
## Attachments
- [emassert.tgz](/uploads/a75264748678243f7dd1e887608fb9bf/emassert.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1381
[libc] erreur: #endif sans #if
2021-02-22T13:29:21Z
mantis-gitlab-migration
[libc] erreur: #endif sans #if
ID0001165:
**This issue was created automatically from Mantis Issue 1165. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001165:
**This issue was created automatically from Mantis Issue 1165. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001165 | Frama-C | Kernel | public | 2012-04-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
This error is at least in:
/usr/local/share/frama-c/libc/fcntl.h
/usr/local/share/frama-c/libc/termios.h
/usr/local/share/frama-c/libc/unistd.h
(and maybe others... I didn't check)
### Additional Information :
I guess that it is because of the missing usual lines:
#ifndef __FC_XXX
#define __FC_XXX
at the beginning of these files.
https://git.frama-c.com/pub/frama-c/-/issues/1382
Using Filter without Value
2021-02-22T13:32:41Z
mantis-gitlab-migration
Using Filter without Value
ID0001110:
**This issue was created automatically from Mantis Issue 1110. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001110:
**This issue was created automatically from Mantis Issue 1110. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001110 | Frama-C | Kernel | public | 2012-03-02 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | Frama-C Oxygen-20120901 | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
When using Filter to build a new project, if the visited old project has a [code_annotation], and the value analysis is not computed, [vcode_annot] crashes on [Db.Value.is_reachable_stmt] because of the assert :
assert (is_computed ()); (* this assertion fails during value analysis *)
in [Db.Value.get_stmt_state].
Either [Db.Value.is_reachable] should return true when the value analysis is not computed, or at least, Filter should call it only if it has been computed.
https://git.frama-c.com/pub/frama-c/-/issues/1384
Sequence number generated by aorai is incorrect
2021-02-22T13:32:46Z
Mounir Assaf
Sequence number generated by aorai is incorrect
ID0001050:
**This issue was created automatically from Mantis Issue 1050. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001050:
**This issue was created automatically from Mantis Issue 1050. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001050 | Frama-C | Plug-in > aoraï | public | 2011-12-14 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Mounir | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
void f(){};
void g(){};
The aorai counter generated for the program and automata below is incorrect. It should be 0 <= aorai_counter <= 5 while it's defined as <=6.
frama-c loop.c -aorai-automata loop.ya
* file: loop.c
int main(int c){
if (c<0){ c = 0;}
if (c>0){ c = 5;}
while (c){
f();
g();
c--;
}
return 0;
}
* file loop.ya
%init : S0;
%accept : Sf;
S0 : {[ main( [ f(); g() ]{0,5} ) ]} -> Sf;
Sf: -> Sf;
https://git.frama-c.com/pub/frama-c/-/issues/1386
incompatible types for a correct spec
2021-02-22T13:29:30Z
Julien Signoles
incompatible types for a correct spec
ID0001027:
**This issue was created automatically from Mantis Issue 1027. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001027:
**This issue was created automatically from Mantis Issue 1027. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001027 | Frama-C | Kernel > ACSL implementation | public | 2011-11-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
On the attached file, we get:
$ frama-c -jessie max_ok.c
<snip>
File "max_ok.jc", line 53, characters 11-17: typing error: incompatible types: intP[..] and integer
Note that the WP plug-in proves this program correct wrt its spec.
## Attachments
- [max_ok.c](/uploads/6e0308bc9a71173bd3e8ca7fb989bc33/max_ok.c)
https://git.frama-c.com/pub/frama-c/-/issues/1388
Frama-c fails when Starting Jessie Translation
2021-02-22T13:29:33Z
mantis-gitlab-migration
Frama-c fails when Starting Jessie Translation
ID0001056:
**This issue was created automatically from Mantis Issue 1056. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001056:
**This issue was created automatically from Mantis Issue 1056. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001056 | Frama-C | Kernel > ACSL implementation | public | 2011-12-21 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Chitman | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Full Stacktrace:
tester@ubuntu-fm:~/Desktop/iteration1/task2$ frama-c -jessie multiset_diff.c
[kernel] preprocessing with "gcc -C -E -I. -dD multiset_diff.c"
[jessie] Starting Jessie translation
multiset_diff.h:45:[jessie] failure: Unexpected failure.
Please submit bug report (Ref. "cil/src/cil.ml:7780:2").
[kernel] The full backtrace is:
Raised at file "src/kernel/log.ml", line 507, characters 30-31
Called from file "src/kernel/log.ml", line 501, characters 2-9
Re-raised at file "src/kernel/log.ml", line 504, characters 8-9
Called from file "src/type/type.ml", line 600, characters 39-44
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 713, characters 2-9
Called from file "src/kernel/cmdline.ml", line 195, characters 4-8
Plug-in jessie aborted because of internal error.
Please report as 'crash' at http://bts.frama-c.com/
Note that a backtrace alone often does not have information to
understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
------------------------
Pls see .h file in attach.
### Additional Information :
Problem lines:
@ lemma test:
@ \forall integer c, int_multiset s;
@ (\forall integer i; (sizeof(Action) <= i < sizeof(c))
@ ==> (contains(s, i) == 0) );
## Attachments
- [multiset_diff.h](/uploads/322e2925efb7ce5176cc8811c2cdd0c8/multiset_diff.h)
- [multiset_diff.c](/uploads/fe21a0cf2500bba6e357f8566b7f2e18/multiset_diff.c)
https://git.frama-c.com/pub/frama-c/-/issues/1389
suggest to use "NULL" rather than "&NULL" for null pointer
2021-02-22T13:44:22Z
Jochen Burghardt
suggest to use "NULL" rather than "&NULL" for null pointer
ID0001066:
**This issue was created automatically from Mantis Issue 1066. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001066:
**This issue was created automatically from Mantis Issue 1066. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001066 | Frama-C | Plug-in > Eva | public | 2012-01-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Running "frama-c -val exm4.c -no-unicode" on the attached program produces an output "p IN {{ &NULL ; &n }}", which is unusual and confusing for a C-programmer. I'd prefer to get "p IN {{ NULL ; &n }}" instead, which also resembles the C code in line 4 of the program.
From p.26 of file "value-analysis-Nitrogen-20111001.pdf", I understand that (void*)0, which I consider an absolute address, handled in the 2nd item under "A set of addresses", should be denoted as "NULL+0". The notation "&NULL", on the other hand, could be subsumed only under the 1st item on p.26, which seems to indicate that "NULL" denotes some variable. So I consider the output on exm4.c to be inconsistent with the explanations on p.26. The same applies to the use of "&NULL" on p.51 and later in the manual.
## Attachments
- [exm4.c](/uploads/b1ce66eefcc2c74cab2007322c4be3f0/exm4.c)
https://git.frama-c.com/pub/frama-c/-/issues/1391
Bad links in generated documentation modules.svg
2021-02-22T13:29:37Z
mantis-gitlab-migration
Bad links in generated documentation modules.svg
ID0001082:
**This issue was created automatically from Mantis Issue 1082. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001082:
**This issue was created automatically from Mantis Issue 1082. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001082 | Frama-C | Kernel > Makefile | public | 2012-02-06 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
There is an error in [share/Makefile.common] in the rule .dot -> .svg
that makes the links incorrect in the generated SVG.
Solution in line 275:
$(ISED) -e "s/\(digraph .*\)/\1 node [href=\"\\N.html\"];/" $<
should be transformed into:
$(ISED) -e "s/\(digraph .*\)/\1 node [href=\"\\\\N.html\"];/" $<
in order to write "\N.html" instead of "N.html" in the dot file.
https://git.frama-c.com/pub/frama-c/-/issues/1392
Imprecision of 'Defs' when querying precise location
2021-02-22T13:29:39Z
Boris Yakobowski
Imprecision of 'Defs' when querying precise location
ID0001079:
**This issue was created automatically from Mantis Issue 1079. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001079:
**This issue was created automatically from Mantis Issue 1079. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001079 | Frama-C | Plug-in > scope | public | 2012-02-03 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
-------------------------
typedef struct {
int a;
int b;
} ts;
ts t[10];
void init() {
t[1].a = 1;
t[1].b = 2;
}
unsigned int main () {
init();
return t[1].a;
}
------------------------
Requiring the instructions that define t[1].a in main yields both lines of function init, which is a bit imprecise. Since slicing main on its return value removes the line 't[1].b = 2', the pdg is probably precise enough. Thus the imprecision lies somewhere in Scope.
https://git.frama-c.com/pub/frama-c/-/issues/1394
relation chains exploited incompletely
2021-02-22T13:29:43Z
Jochen Burghardt
relation chains exploited incompletely
ID0001071:
**This issue was created automatically from Mantis Issue 1071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001071:
**This issue was created automatically from Mantis Issue 1071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001071 | Frama-C | Plug-in > Eva | public | 2012-01-26 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Running "frama-c -val ftest.c" on the attached program yields
"Called Frama_C_show_each_m([0..2147483647])
Called Frama_C_show_each_n([0..9])".
When the precondition in line 1 is replaced by the equivalent version in line 2, we obtain
"Called Frama_C_show_each_m([0..9])
Called Frama_C_show_each_n([0..9])".
Seemingly, from the relation chain "0 <= m <= n <= 9", the information "m <= 9" is not used.
## Attachments
- [ftest.c](/uploads/6bd935ca5fd432edc92877b733d621ff/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1395
Cil.prepareCfg (or -simplify-cfg option) insert dummy locations in the ast
2021-02-22T13:29:49Z
mantis-gitlab-migration
Cil.prepareCfg (or -simplify-cfg option) insert dummy locations in the ast
ID0001025:
**This issue was created automatically from Mantis Issue 1025. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001025:
**This issue was created automatically from Mantis Issue 1025. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001025 | Frama-C | Kernel | public | 2011-11-21 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | fgarnier | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Hello,
I am developing some Frama-c plugin to extract some counter
automata based models of C programs, and I am currently developing
this plugin using the Carbon-20110201 release.
To generate our model, I am using some graph traversal algorithm on
the Control flow graph computed by Cil, and I do perform
some analysis on the the arguments of the instructions.
At some point, I do traverse a "Skip" type instruction, and the value
contained in the the Cil_types.location argument is :
"In file : Cabs2cil_start, from line 0 col -1 to line 0 col -1."
The file Cabs2cil_start appears to be some Framac file, issued in
the carbon version. This is strange, because others instruction that
contains location positions, used to contain value that deal with
the analyzed C source code -- And I was expecting to get such a value.
After some time spent on the Mantis BTS, I noticed that some issues
were the name "Cabs2cil_start" appeared, were solved, but I
can't figure out if this will solve the problem I get. Maybe I won't get
this problem anymore, when I will migrate from Carbon to the new
Nitrogen version, but I prefer to point this strange thing to you.
I have two extra questions : Concerning the Skip instruction, does it
mean that the control goes through the statement without performing
any operation ?
Is it still worth reporting bugs on the Carbon version of Frama-C ?
Best regards,
Florent Garnier.
### Additional Information :
The Skip "instruction" is defined in the file Cil_types.ml.
and stmtkind =
| Instr of instr
(** An instruction that does not contain control flow. Control
* implicitly falls through. *)
| Return of exp option * location
(** The return statement. This is a leaf in the CFG. *)
[...]
and instr =
Set of lval * exp * location (** An assignment. A cast is present
if the exp has different type
from lval *)
[...]
| Skip of location
| Code_annot of code_annotation * location
## Attachments
- [debug.tgz](/uploads/0d3edbfc568ae757a4853b5000513536/debug.tgz)
- [vis.ml](/uploads/21a01d1fd43ad568bd5147350bccc636/vis.ml)
- [Debug_plugin.tgz](/uploads/9fbfd031a588d3117ab4f0889c021663/Debug_plugin.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1396
Slicer: slicing preserving some undesired function calls
2021-02-22T14:03:05Z
Dillon Pariente
Slicer: slicing preserving some undesired function calls
ID0000107:
**This issue was created automatically from Mantis Issue 107. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000107:
**This issue was created automatically from Mantis Issue 107. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000107 | Frama-C | Plug-in > slicing | public | 2009-05-27 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | yakobowski | **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 Oxygen-20120901 |
### Description :
(This issue was previously discussed through private messages but not yet resolved. It was noticed that a solution would require some "work around"! It is now recorded into the BTS for traceability reasons.)
The following code is sliced w.r.t. its annotation.
typedef struct { int i; int j; } las;
las v1,v2,v3;
void g(las*p) { p->i = p->i * 2; }
void f()
{
g( &v1 );
g( &v2 );
g( &v3 );
//@ assert v2.i>=10;
}
Command line:
frama-c -slice-assert f -slice-print -lib-entry -main f foo.c
The sliced code got rid of the statement g(&v3) (with calldeps), but kept g(&v1).
A slicer improvement would be, of course, to be able to get also rid of the 1st call to g (i.e., "g(&v1);")!
https://git.frama-c.com/pub/frama-c/-/issues/1402
wrong origin displayed in the GUI
2021-02-22T13:30:08Z
Pascal Cuoq
wrong origin displayed in the GUI
ID0000251:
**This issue was created automatically from Mantis Issue 251. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000251:
**This issue was created automatically from Mantis Issue 251. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000251 | Frama-C | Plug-in > Eva | public | 2009-09-20 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | immediate | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
~/ppc/bin/viewer.opt -val imprecise.c
Inspect value of F at the last statement before return.
It shows Origin: Misaligned ..:19
This is correct (we are at line 19).
Inspect the value of "*p"
It shows Origin: Misaligned ..:20
This is incorrect. Line 20 has not even been analyzed yet.
Note: this is probably only a problem in display (since F is correct).
Unfortunately this happens in a demo I was planning to do soon for
someone that matters a lot. Quick fix very much appreciated if at all
possible (meanwhile I will try to hide the problem by adjusting
the demo).
## Attachments
- [imprecise.c](/uploads/d0430283fcaa57d47ff326e878716536/imprecise.c)
https://git.frama-c.com/pub/frama-c/-/issues/1413
Arguments are not checked when function call precedes function declaration
2021-02-22T14:03:07Z
Virgile Prevosto
Arguments are not checked when function call precedes function declaration
ID0000728:
**This issue was created automatically from Mantis Issue 728. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000728:
**This issue was created automatically from Mantis Issue 728. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000728 | Frama-C | Kernel | public | 2011-02-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Cil allows a function to be called before being defined but does not check that the number/types of argument correspond. See for instance
tests/misc/call_variadic.i, which fails with frama-c -check, while the error should be reported directly when type-checking.
https://git.frama-c.com/pub/frama-c/-/issues/1418
FRAMA_C_MALLOC_INFINITE not used in stdlib.c
2021-02-22T13:30:40Z
mantis-gitlab-migration
FRAMA_C_MALLOC_INFINITE not used in stdlib.c
ID0001214:
**This issue was created automatically from Mantis Issue 1214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001214:
**This issue was created automatically from Mantis Issue 1214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001214 | Frama-C | Plug-in > Eva | public | 2012-06-18 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
#define FRAMA_C_MALLOC_INFINITE
#include "stdlib.c"
doesn't do what is expected since stdlib.c begins with :
#ifndef FRAMA_C_MALLOC_HEAP
#ifndef FRAMA_C_MALLOC_CHUNKS
#ifndef FRAMA_C_MALLOC_INDIVIDUAL
#ifndef FRAMA_C_MALLOC_POSITION
#define FRAMA_C_MALLOC_HEAP
so it ends up with FRAMA_C_MALLOC_HEAP instead. Is this on purpose ?
PS. I select [Kernel] category because I don't know where else to put it...
https://git.frama-c.com/pub/frama-c/-/issues/1428
syntax error message refers to (true error line + 5 lines)
2021-02-22T13:31:01Z
Jochen Burghardt
syntax error message refers to (true error line + 5 lines)
ID0000840:
**This issue was created automatically from Mantis Issue 840. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000840:
**This issue was created automatically from Mantis Issue 840. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000840 | Frama-C | Kernel | public | 2011-05-27 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
In the attached program, I confused "ensures" and "assert" in the contract of p() in line 20. However, the syntax error message refers to 5 lines below (i.e. line 25). If the error is moved e.g. to line 10 the message refers to line 15.
Usually there is other C- or Acsl-code after the error; the message is rather confusing in that cases.
## Attachments
- [ftest.c](/uploads/004e3ba1ff3a1ca8964d03156d590cab/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1430
error with -pp-annot : eof while parsing C comment
2021-02-22T13:31:04Z
mantis-gitlab-migration
error with -pp-annot : eof while parsing C comment
ID0001226:
**This issue was created automatically from Mantis Issue 1226. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001226:
**This issue was created automatically from Mantis Issue 1226. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001226 | Frama-C | Kernel | public | 2012-07-02 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
With the following example:
void test (void) { char * str = "/*"; }
The command:
$ frama-c toto.c -pp-annot
gives:
[kernel] preprocessing with "gcc -C -E -I. -dD toto.c"
"toto.c":3:[kernel] user error: Can't preprocess annotation: eof while parsing C comment
Annotation will be kept as is
I guess that the string "/*" is considered by frama-c as the beginning of a comment...
### Additional Information :
With { char * str = "//@"; } it gives more errors...
https://git.frama-c.com/pub/frama-c/-/issues/1437
Opening consolidation graph crashes when 'dot' is missing
2021-02-22T14:03:08Z
Julien Signoles
Opening consolidation graph crashes when 'dot' is missing
ID0001122:
**This issue was created automatically from Mantis Issue 1122. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001122:
**This issue was created automatically from Mantis Issue 1122. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001122 | Frama-C | Graphical User Interface | public | 2012-03-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
All in the title. Was previously fixed for the callgraph.
https://git.frama-c.com/pub/frama-c/-/issues/1440
Journalisation of dynamic functions using abstract types does not work
2021-02-22T13:31:25Z
Julien Signoles
Journalisation of dynamic functions using abstract types does not work
ID0000932:
**This issue was created automatically from Mantis Issue 932. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000932:
**This issue was created automatically from Mantis Issue 932. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000932 | Frama-C | Kernel | public | 2011-08-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | low | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
All in the title...
### Additional Information :
For fixing this issue, the journal must generate "let module" in such cases.
### Steps To Reproduce :
With the attached files, run:
$ frama-c -load-script cpt.ml -load-script use.ml -journal-enable
Then read the generated journal.
## Attachments
- [use.ml](/uploads/aff64533c357a7177fc64d65c6d2678d/use.ml)
https://git.frama-c.com/pub/frama-c/-/issues/1444
Double version of program considerably slower to analyze than float version (...
2021-02-22T14:03:09Z
mantis-gitlab-migration
Double version of program considerably slower to analyze than float version (svn 19535)
ID0001260:
**This issue was created automatically from Mantis Issue 1260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001260:
**This issue was created automatically from Mantis Issue 1260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001260 | Frama-C | Plug-in > Eva | public | 2012-08-03 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sven | **Assigned To** | yakobowski | **Resolution** | fixed |
| **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 :
When analyzing the attached program, Value is much slower when analyzing a double version than when analyzing with floats.
### Additional Information :
Steps to reproduce:
time -v -- frama-c -val -slevel 1100 interp.c
change typedef
time -v -- frama-c -val -slevel 1100 interp.c
## Attachments
- [interp.c](/uploads/8bfbc504d93081e0a2a204f1fc22326e/interp.c)
- [prof-double](/uploads/2f2093a32183da4e374ef69e73da48fa/prof-double)