frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:51:35Zhttps://git.frama-c.com/pub/frama-c/-/issues/961contract completely ignored if preceeded by initial comment2021-02-22T13:51:35ZJochen Burghardtcontract completely ignored if preceeded by initial commentID0001819:
**This issue was created automatically from Mantis Issue 1819. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001819:
**This issue was created automatically from Mantis Issue 1819. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001819 | Frama-Clang | Plug-in > clang | public | 2014-06-27 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 (64 bit) | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c -wp -wp-rte Fault2.cpp -wp-out Fault2_64" on the attached program produces the attached file "_Z3fooi_assert.ergo", corresponding to the "assert" in line 8, but no .ergo file for the (non-trivial) "ensures" in line 5. The proof obligation in file "_Z3fooi_assert.ergo" shows that the requires from line 4 has been ignored, too.
In the gui, no contract at all is shown in the (left-hand side) normalized-code window.
The problem disappears if
(1) the file is renamed to "Fault2.c", or
(2) the comment is moved after the "requires" clause (, or removed completely).
## Attachments
- [Fault2.cpp](/uploads/065e1a4fe5bef2a28e0fc7ffb524867c/Fault2.cpp)
- [_Z3fooi_assert.ergo](/uploads/17ae2b20f01db327a5a4b6eda758bfc4/_Z3fooi_assert.ergo)https://git.frama-c.com/pub/frama-c/-/issues/652syntax error in contract causes rest to be tacitly ignored2021-02-22T14:01:54ZJochen Burghardtsyntax error in contract causes rest to be tacitly ignoredID0001821:
**This issue was created automatically from Mantis Issue 1821. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001821:
**This issue was created automatically from Mantis Issue 1821. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001821 | Frama-Clang | Plug-in > clang | public | 2014-06-27 | 2015-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 (64 bit) | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c-gui -wp -wp-rte Fault2.cpp" on the attached program causes a message "Fault2.cpp:4:2: expecting function spec" on stderr (that's ok), but doesn't prevent the gui to appear (that's at least different to the behavior on a renamed version "Fault2.c").
More important, no error or warning message is visible in the gui (I checked the tabs "Information", "Messages", "Console", "Properties", "WP Goals"), and the contract rest after the error is tacitly ignored.
## Attachments
- [Fault2.cpp](/uploads/2ea7598b48027d199c2e89b9df46f36c/Fault2.cpp)https://git.frama-c.com/pub/frama-c/-/issues/963array-type parameter causes "Old style K&R" kernel warning with cxx plugin2021-02-22T13:27:57ZJochen Burghardtarray-type parameter causes "Old style K&R" kernel warning with cxx pluginID0001814:
**This issue was created automatically from Mantis Issue 1814. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001814:
**This issue was created automatically from Mantis Issue 1814. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001814 | Frama-Clang | Plug-in > clang | public | 2014-06-20 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
output:
Now output intermediate result
taint02.cpp:7:[kernel] warning: Calling undeclared function _Z3fooPi. Old style K&R code?
The warning disappears if the file is renamed to "taint02.c".
## Attachments
- [taint02.cpp](/uploads/0071ae679c085de2390e5212762dc45d/taint02.cpp)https://git.frama-c.com/pub/frama-c/-/issues/962Frama-clang has problems with "decreases" clauses2021-02-22T13:16:01ZJens GerlachFrama-clang has problems with "decreases" clausesID0001815:
**This issue was created automatically from Mantis Issue 1815. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001815:
**This issue was created automatically from Mantis Issue 1815. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001815 | Frama-Clang | Plug-in > clang | public | 2014-06-20 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Frama-Clang reports a "expecting function spec" when it
encounters a decreases-clause in a function contract.
The decrease-clause and all following clauses in the same contract
are then ignored and do not appear in the normalised representation.
### Steps To Reproduce :
The attached file is also available under acslplusplus/C++Examples/Problems.
## Attachments
- [problem300.cpp](/uploads/61244a27776b55985918c660ae29041f/problem300.cpp)https://git.frama-c.com/pub/frama-c/-/issues/1016clause "n<9-1" normalized to "n-1<9"2021-02-22T13:17:26ZJochen Burghardtclause "n<9-1" normalized to "n-1<9"ID0001810:
**This issue was created automatically from Mantis Issue 1810. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001810:
**This issue was created automatically from Mantis Issue 1810. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001810 | Frama-Clang | Plug-in > clang | public | 2014-06-16 | 2014-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c-gui -wp -wp-rte 108.cpp -wp-out wp-out" on the attached program shows in the gui's normalized-code window the clause "requires 0 <= n-1 && n-1 < 9;" as translation of source line 5 ("requires 0 <= n < 9-1;").
The same error is found in alt-ergo's input file "_Z4push_assert_rte_index_bound_2.ergo". As a consequence, alt-ergo can't prove the index bound for line 9.
The error disappears if
* the file is renamed to "108.c",
* "9-1" is replaced by "9" in line 5.
The error appears unchanged if "n" is made a procedure parameter of "push".
## Attachments
- [108.cpp](/uploads/f07695abe8c21809455ab3b47fd664b3/108.cpp)
- [_Z4push_assert_rte_index_bound_2.ergo](/uploads/e6b954a9726185b9f5ecdbb9bd90990d/_Z4push_assert_rte_index_bound_2.ergo)
- [109.cpp](/uploads/6aac1934cfc40814903aafd21efbc26b/109.cpp)https://git.frama-c.com/pub/frama-c/-/issues/964label argument of \at unrecognized2021-02-22T13:16:04ZJochen Burghardtlabel argument of \at unrecognizedID0001811:
**This issue was created automatically from Mantis Issue 1811. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001811:
**This issue was created automatically from Mantis Issue 1811. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001811 | Frama-Clang | Plug-in > clang | public | 2014-06-16 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
output:
110.cpp:4:33: expecting a label in the \at construct
Now output intermediate result
The problem remains when "entry" in line 4 is replaced by any of the FRAMA-C predefined labels "Old", "Pre", "Here", or "Post".
The problem disappears when the file is renamed to "110.c".
## Attachments
- [110.cpp](/uploads/d68acdaeb675d2bcc606417edcfed286/110.cpp)https://git.frama-c.com/pub/frama-c/-/issues/1017Frama-Clang fails to parse simple predicate2021-02-22T13:17:27ZJens GerlachFrama-Clang fails to parse simple predicateID0001808:
**This issue was created automatically from Mantis Issue 1808. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001808:
**This issue was created automatically from Mantis Issue 1808. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001808 | Frama-Clang | Plug-in > clang | public | 2014-06-13 | 2014-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
When Frama-Clang is called on the following code fragment
/*@
predicate IsValidRange(int* a, integer n) = (0 <= n) && \valid(a+(0.. n-1));
*/
void foo(int* a, int);
with the command line
frama-c -cpp-command 'gcc -C -E -nostdinc -I/opt/local/include -I/Users/jens/.opam/system/lib/frama-c/share/frama-c/libc' -cxx-clang-command="framaCIRGen" -cxx-demangling-full -wp -wp-rte -wp-out problem208.wp problem208.cpp
then the following error message occurs
Stack dump:
0. <eof> parser at end of file
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: skipping file "problem208.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
As far as I can see the problem is related to the predicate definition.
It is one of our simpler predicates in ACSL by Example.
### Steps To Reproduce :
The example is available also under acslplusplus/C++Examples/Problems/problem208.cpphttps://git.frama-c.com/pub/frama-c/-/issues/1021Frama-clang include problem with directory hierarchy2021-02-22T13:17:33ZJens GerlachFrama-clang include problem with directory hierarchyID0001797:
**This issue was created automatically from Mantis Issue 1797. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001797:
**This issue was created automatically from Mantis Issue 1797. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001797 | Frama-Clang | Plug-in > clang | public | 2014-06-04 | 2014-06-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached tar file contains a small directory hierarchy
problem206-dir
├── nonmutating
│ └── equal
│ ├── README
│ └── equal.c
└── typedefs.h
The file equal.c includes the file typedefs.h which is two layers up in the hierarchy.
When I call
frama-c.byte -cxx-clang-command="framaCIRGen -I../.." equal.c
then I receive the following error message
[kernel] preprocessing with "gcc -C -E -I. equal.c"
equal.c:2:20: fatal error: typedefs: No such file or directory
#include "typedefs"
^
compilation terminated.
[kernel] user error: failed to run: gcc -C -E -I. -o '/tmp/equal.c5f0bc4.i' 'equal.c'
you may set the CPP environment variable to select the proper preprocessor command or use the option "-cpp-command".
[kernel] user error: skipping file "equal.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
### Additional Information :
I am particularly baffled by the kernels message to "use -cpp-command" because I thought this option is not to be used with frama-clang.
Also, the problem disappears when the header typedefs.h is only one level above equal.c.
(Of course, the command line has to be changed accordingly.)
The example can also be found in
acslplusplus/C++Examples/Problems/problem206-dir
## Attachments
- [problem206-dir.tar](/uploads/cca3489eeafcb5be7e26e3fdcc9308bb/problem206-dir.tar)https://git.frama-c.com/pub/frama-c/-/issues/965"\nothing" unrecognized in assigns clause2021-02-22T13:28:14ZJochen Burghardt"\nothing" unrecognized in assigns clauseID0001793:
**This issue was created automatically from Mantis Issue 1793. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001793:
**This issue was created automatically from Mantis Issue 1793. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001793 | Frama-Clang | Plug-in > clang | public | 2014-06-02 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c from02.cpp" on the attached program yield the output:
from01.cpp:5:26: keyword 'keyword -> \nothing' encountered when parsing term or predicate
The error message disappears when the file is renamed to "from02.c"
## Attachments
- [from02.cpp](/uploads/cfe7e5a28737d3158b8d5f7d2f27fb1a/from02.cpp)https://git.frama-c.com/pub/frama-c/-/issues/808function called in initialization of a static/global variable2021-03-29T16:50:16ZFranck Vedrinefunction called in initialization of a static/global variableID0001728:
**This issue was created automatically from Mantis Issue 1728. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001728:
**This issue was created automatically from Mantis Issue 1728. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001728 | Frama-Clang | Plug-in > clang | public | 2014-04-01 | 2015-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | fvedrine | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | Frama-C GIT, precise the release id | **Fixed in Version** | - |
### Description :
C++ authorizes the call of function to initialize static variables.
In C this can only be done with __attribute__((constructor)).
It requires modification in Cabs to accept it.
initialization.cpp:7:[kernel] warning: CALL in constant
initialization.cpp:7:[kernel] user error: invalid global initializer tmp
{/*() <-
Calls:
tmp = _ZN1AE1f();
*/
tmp = _ZN1AE1f();}
## Attachments
- [initialization.cpp](/uploads/f74ef7ad9e674a067ea3b5b37f3fe0a5/initialization.cpp)Virgile PrevostoVirgile Prevosto