frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:13:26Zhttps://git.frama-c.com/pub/frama-c/-/issues/851Declaration order of static class member2021-02-22T13:13:26ZJens GerlachDeclaration order of static class memberID0001950:
**This issue was created automatically from Mantis Issue 1950. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001950:
**This issue was created automatically from Mantis Issue 1950. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001950 | Frama-Clang | Plug-in > clang | public | 2014-11-02 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | high | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following file contains two classes A and B that contain a single static variable count.
A::count is declared at the beginning of class A. Everything is fine.
B::count, however, is defined at the end of class B. Here Frama-Clang complains.
problem209.cpp:26:[fclang] failure: Unknown global variable B::count
### Additional Information :
Note, the problem does not occur, when B::count is a non-static member.
## Attachments
- [problem209.cpp](/uploads/12b2d0b16ba9d25bf52bd8af599cf33c/problem209.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/844reference typedef causes conversion error in contract2021-02-22T14:02:14ZJochen Burghardtreference typedef causes conversion error in contractID0001948:
**This issue was created automatically from Mantis Issue 1948. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001948:
**This issue was created automatically from Mantis Issue 1948. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001948 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
114.cpp:7:37: invalid implicit conversion
Now output intermediate result
The error disappears if "reference" is changed to "int&" in line 8.
## Attachments
- [114.cpp](/uploads/47dd1e60cc1a1a5d2510ce3ad1ed608f/114.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/843"operator==" not recognized as predicate name2021-02-22T14:02:14ZJochen Burghardt"operator==" not recognized as predicate nameID0001949:
**This issue was created automatically from Mantis Issue 1949. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001949:
**This issue was created automatically from Mantis Issue 1949. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001949 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
115.cpp:4:16: expecting an identifier after 'predicate'
Now output intermediate result
It should be easy to accept "operator==" also as an ACSL predicate name, similar as in C++ code.
## Attachments
- [115.cpp](/uploads/3af4fa9c279e598a1fa8f5271ba24e16/115.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/839use of "new" causes warning2021-02-22T14:01:43ZJochen Burghardtuse of "new" causes warningID0001945:
**This issue was created automatically from Mantis Issue 1945. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001945:
**This issue was created automatically from Mantis Issue 1945. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001945 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
running file 050.cpp (from the resolved issue #1569) generates the output:
Now output intermediate result
[kernel] warning: Assuming declared function malloc can't throw any exception
In the long run, this warning should be avoided, since it is confusing to novel users. All methods (such as malloc) that don't originate from C++ user input should be handled as known to Frama-C.
According to Stroustrup's "The C++ programming language" (3rd ed.), sect.14.10, "new" may throw the exception "bad_alloc". Frama-C should be aware of this, without telling it to the user every time.
## Attachments
- [050.cpp](/uploads/97a9ab005c7cfc03376cf9c34ddbe052/050.cpp)
- [050a.cpp](/uploads/b501e75adabb33b35c888c830a08b0ee/050a.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/660CLASSNAME::PREDICATENAME not recognized as predicate (or even as term)2021-02-22T13:39:56ZJochen BurghardtCLASSNAME::PREDICATENAME not recognized as predicate (or even as term)ID0001944:
**This issue was created automatically from Mantis Issue 1944. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001944:
**This issue was created automatically from Mantis Issue 1944. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001944 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-04-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
113.cpp:13:28: expecting a term or predicate
113.cpp:13:28: the term is not a predicate
Now output intermediate result
Note that the 2nd message claims a term while the 1st denies a term; no message should appear.
If the prefix "Queue::" is omitted in line 10 before "IsValid", no message is issued, while "unknown identifier 'IsValid'" should be reported.
If the definition of Queue() and its contract are moved inside the class, no message is issued, which is ok.
Probably related to issue #1606.
## Attachments
- [113.cpp](/uploads/4926913e5616dc5c301dabd76eac5c74/113.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/845Frama-C-clang does not unfold typedef2021-02-22T14:02:14ZJens GerlachFrama-C-clang does not unfold typedefID0001805:
**This issue was created automatically from Mantis Issue 1805. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001805:
**This issue was created automatically from Mantis Issue 1805. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001805 | Frama-Clang | Kernel | public | 2014-06-12 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When Frama-Clang analyses the following code example
struct A
{
int n;
};
typedef struct A B;
/*@
requires \valid(b);
assigns \nothing;
ensures \result == b->n;
*/
int foo(B* b)
{
return b->n;
}
then it complains
problem207.cpp:12:29: expecting a struct with field
problem207.cpp:12:29: type is not a pointer type
### Steps To Reproduce :
The source code of the example is available under acslplusplus/C++Examples/Problems/problem207.cpp
It was analysed with the following command line:
frama-c.byte -cxx-clang-command="framaCIRGen" -wp problem207.cppVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/850Frama-Clang does allow access to private fields within annotations2021-02-22T13:13:24ZJens GerlachFrama-Clang does allow access to private fields within annotationsID0001791:
**This issue was created automatically from Mantis Issue 1791. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001791:
**This issue was created automatically from Mantis Issue 1791. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001791 | Frama-Clang | Kernel | public | 2014-05-30 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following example shows that the private field A::i can be accessed in an annotation.
In my opinion the access rules in annotations should be the same as for code.
struct A
{
private:
int i;
public:
explicit A(int k) : i(k) {}
/*@
assigns \nothing;
ensures \result == i;
*/
int get() const
{
return i;
}
};
int foo(const A& a)
{
int b = a.get();
//@ assert b == a.i;
// Frama-Clang allows access to private field of A
// a.i cannot be accessed here because it is private
// this is recognized by Frama-Clang
// int c = a.i;
return b;
}Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/290How to use the "Callers ..." context menu item2021-02-22T12:58:22Zmantis-gitlab-migrationHow to use the "Callers ..." context menu itemID0001431:
**This issue was created automatically from Mantis Issue 1431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001431:
**This issue was created automatically from Mantis Issue 1431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001431 | Frama-C | Graphical User Interface | public | 2013-05-27 | 2018-01-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dhekir | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Pardon the ignorance, but I couldn't find this on the manual...
I have a program where, after parsing, some warnings of this form are emitted:
"Calling undeclared function __builtin_swap32. Old style K&R code?"
I know there is a missing source file somewhere in my project, but I'd like to know who is calling these functions (since they are never directly called in my code). So I right-click on the function prototype on the GUI, and the last button in the context menu is "Callers ...". If I click on it, the "Launching analysis" window is displayed, with no indication of which analysis to choose.
I suppose the analysis I'd like is "Syntactic callgraph". So I choose it, without customizing any options, click Execute, but nothing changes. The "Callers ..." button is always visible when right-clicking the function declaration.
I noticed that if I choose the "Users" analysis, when right-clicking afterwards there is no more "Callers ..." button on the context menu, but I fail to see how any of the new options (e.g. Dependencies) could help me identify the function callers.
Is there a simpler way, other than by manually parsing the DOT file (the produced graph is too large for me to visually inspect it), to obtain information about function callers?Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2347Parse error when using a wide string literal to initialize uint16 array2021-02-22T13:56:58Zmantis-gitlab-migrationParse error when using a wide string literal to initialize uint16 arrayID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000593 | Frama-C | Kernel | public | 2010-09-30 | 2010-10-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Maria | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm trying to analyze Brew with Frama-C. OS - windows XP.
I've created simple Brew project(see attach), preprocessed it with Visual Studio and after it try to analyze with Frama-C:
C:\Frama-C\bin>frama-c.exe "\Program Files\BREW 3.1.5\sdk\examples\helloworld"\*.i
Also, I've tried to add files to project, using user interface, but nothing happened.
## Attachments
- [helloworld.zip](/uploads/e1faf5861730eaa7d75da589b90c18c6/helloworld.zip)Virgile PrevostoVirgile Prevosto