frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:26:56Zhttps://git.frama-c.com/pub/frama-c/-/issues/866"do"-loop with body interspersed with "case" labels of surrounding "switch" n...2021-02-22T13:26:56ZJochen Burghardt"do"-loop with body interspersed with "case" labels of surrounding "switch" not parsedID0001994:
**This issue was created automatically from Mantis Issue 1994. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001994:
**This issue was created automatically from Mantis Issue 1994. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001994 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Unsupported Statement:
DefaultStmt 0x2caf430 <158.cpp:6:2, col:15>
`-UnaryOperator 0x2c64b68 <col:12, col:15> 'int' postfix '++'
`-DeclRefExpr 0x2c64b40 <col:12> 'int' lvalue Var 0x2c649a0 'sum' 'int'
Aborting
The program has been boiled down from that an exercise in Stroustrup's C++ book, see attached file "stroustrup_06_06_15.cpp" for full example.
## Attachments
- [158.cpp](/uploads/7f019adb35c3e1fa16d757db41c9f50c/158.cpp)
- [stroustrup_06_06_15.cpp](/uploads/420758addbd603cbf270e95b7f67b154/stroustrup_06_06_15.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/865bitwise negation of uint introduces "-1" in Alt-Ergo obligation2021-02-22T13:41:06ZJochen Burghardtbitwise negation of uint introduces "-1" in Alt-Ergo obligationID0002023:
**This issue was created automatically from Mantis Issue 2023. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002023:
**This issue was created automatically from Mantis Issue 2023. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002023 | Frama-Clang | Documentation > ACSL | public | 2014-12-08 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
For the assertion in line 3 of the attached file "198.c", Frama-c generates the following proof obligation for Alt-Ergo: "goal foo_assert: forall i : int. is_uint32(i) -> ((-1) = i)". However, axiom "is_uint32_def" in line 430 of file "foo_assert_Alt-Ergo.mlw" says: "is_uint32(x) -> (0 <= x)", while "0 <= -1" is false (and unprovable as an own goal by Alt-Ergo).
As a consequence, there exists no (satisfiable) precondition "requires p(i)" that could be added as contract of "foo()" such that the assertion in line 3 becomes satisfiable, since "forall i : int. p(i) -> is_uint32(i) -> ((-1) = i)" implies "forall i : int. p(i) -> is_uint32(-1)". For example, requiring "i == 0xffffffffu" doesn't make line 3 provable, nor does any similar equation.
## Attachments
- [198.c](/uploads/43894779f84ecb85c5bbca9c5d4f60c5/198.c)
- [foo_assert_Alt-Ergo.mlw](/uploads/2d9028c59b5be767e57c7919eccb4d8b/foo_assert_Alt-Ergo.mlw)
- [198a.c](/uploads/387d28aa89210ab23bd7de97f80871b9/198a.c)
- [2compl.txt](/uploads/5886d302a5d8d0deae8deb56309ab3fe/2compl.txt)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/864non-predicate on right-hand size of "|" causes segmentation fault2021-03-29T16:34:53ZJochen Burghardtnon-predicate on right-hand size of "|" causes segmentation faultID0001991:
**This issue was created automatically from Mantis Issue 1991. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001991:
**This issue was created automatically from Mantis Issue 1991. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001991 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Same for "&".
In contrast, "i | (i==i)" is accepted, which might not be ok either, since "i" is not a predicate, and "i | ..." isn't either.
## Attachments
- [155.cpp](/uploads/97f44d774ea3375ac8795a16896f3136/155.cpp)
- [155a.cpp](/uploads/6028e94aafd01c070d1470bd32b6a00c/155a.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/863how to specify equality of references, rather than of values, in contract?2021-02-22T13:13:38ZJochen Burghardthow to specify equality of references, rather than of values, in contract?ID0001990:
**This issue was created automatically from Mantis Issue 1990. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001990:
**This issue was created automatically from Mantis Issue 1990. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001990 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The contract of the function "fst" in line 4 of the attached program intends to specify that "fst(ppp)" returns a reference to "ppp.xxx".
However, it is interpreted by Frama-C as specifying that "fst(ppp)" and "ppp.xxx" have the same value. As a consequence, the assertion in line 10 cannot be proven; the generated obligation essentially amounts to "t_2[a_1] = t_2[a] -> 222 = t_2[a_1 <- 222][a]"; cf. the attached .mlw file. If the precondition would state reference equality (i.e. "a_1 = a") instead of value equality (i.e. "t_2[a_1] = t_2[a]"), the goal would follow trivially.
Frama-C's interpretation is not a bug, but is perfectly valid.
However, the question arises how the intended meaning (i.e. reference equality) could be formalized in the contract. Maybe another equality operator ( named e.g. "===") should be introduced into ACSL++ for this purpose.
## Attachments
- [152.cpp](/uploads/ae9fb734c8266aae29f014361aee8f4f/152.cpp)
- [_Z3bar_assert_Alt-Ergo.mlw](/uploads/f53057cf4583330c0dba0cd5ac99de4f/_Z3bar_assert_Alt-Ergo.mlw)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/861scope resolution operator not recognized in assertion2021-02-22T13:26:43ZJochen Burghardtscope resolution operator not recognized in assertionID0001984:
**This issue was created automatically from Mantis Issue 1984. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001984:
**This issue was created automatically from Mantis Issue 1984. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001984 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
146.cpp:9:14: unexpected token 'operator -> ::' when starting to parse a term
Now output intermediate result
(Lines 5-8 aren't really needed to produce the error message.)
## Attachments
- [146.cpp](/uploads/73158ee47b3e3b872d5c8187cf72008b/146.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/860identifier unknown after leaving inner scope that declared same name2022-04-02T21:12:27ZJochen Burghardtidentifier unknown after leaving inner scope that declared same nameID0001983:
**This issue was created automatically from Mantis Issue 1983. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001983:
**This issue was created automatically from Mantis Issue 1983. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001983 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
145.cpp:7:16: unknown identifier 'x'
Now output intermediate result
...
[wp] Proved goals: 0 / 0
The error message disappears and a proof obligation is generated (and proven by Qed) if "x" is changed to "y" in the inner scope (line 5).
## Attachments
- [145.cpp](/uploads/73be9f397b0fdbf37c7e518259c9bf24/145.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/859enum types in contract cause syntax error2021-02-22T13:26:57ZJochen Burghardtenum types in contract cause syntax errorID0001982:
**This issue was created automatically from Mantis Issue 1982. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001982:
**This issue was created automatically from Mantis Issue 1982. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001982 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
144.cpp:4:22: keyword 'keyword -> enum' encountered when parsing a type
Now output intermediate result
The message disappears if the file is renamed to "144.c".
## Attachments
- [144.cpp](/uploads/cfc01750842b55273e7a3094dc5cba83/144.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/857Liskov substitution principle not checked for methods of same name and signat...2021-02-22T13:13:33ZJochen BurghardtLiskov substitution principle not checked for methods of same name and signature in super- and subclassID0001978:
**This issue was created automatically from Mantis Issue 1978. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001978:
**This issue was created automatically from Mantis Issue 1978. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001978 | Frama-Clang | Plug-in > clang | public | 2014-11-20 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is not a bug report but merely a suggestion for discussion. According to the "Liskov substitution principle" (see the English wikipedia article of that name for references) a method in a subclass should have a stronger (or equivalent) contract that the corresponding method in the superclass. It could make sense to provide a corresponding check within Frama-Cxx, which could be enabled or disabled by an appropriate command-line option.
This check would be negative (i.e. unprovable) for the attached program "140.cpp"; however, it would be positive if "==" in line 3 was changed to ">=". So this program can be used as a simple test case for such a check, if and when it is implemented.
## Attachments
- [140.cpp](/uploads/1bc224ee781810c444a06c34ee30f3e8/140.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/855insufficient preconditions given to Alt-Ergo to prove assigns clause for muta...2021-02-22T14:02:13ZJochen Burghardtinsufficient preconditions given to Alt-Ergo to prove assigns clause for mutable variable in contract of const methodID0002000:
**This issue was created automatically from Mantis Issue 2000. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002000:
**This issue was created automatically from Mantis Issue 2000. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002000 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte 171.cpp" on the attached program produces an obligation "typed__ZNK2clE3foo_assert_rte_mem_access" which is unprovable by Alt-Ergo. When the "const" is deleted in line 6, all obligations are provable.
The goal in the .mlw file is "... -> valid_rd(t, a, 1) -> valid_rw(t, shiftfield_F__Z2cl_x(a), 1)" with the "const", see attached file "_ZNK2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw", and "... -> valid_rw(t, a, 1) -> valid_rw(t, shiftfield_F__Z2cl_x(a), 1)" without it, see file "_ZN2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw". Since "shiftfield_F__Z2cl_x(p)" is defined as "shift(p,0)", the latter goal is trivially true.
Probably, the possibility that a "const" function well may modify a "mutable" variable has not been considered in proof goal generation.
## Attachments
- [171.cpp](/uploads/e0bcb05cd42e24bf1af6dd3309c3fc13/171.cpp)
- [_ZNK2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/0bb4d0ab67362ba0f4c5cf4c232c3e8d/_ZNK2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw)
- [_ZN2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/c120e77b9b17d4f7e08d80aebc0cd6b6/_ZN2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/853placement new causes crash2021-02-22T13:13:28ZJochen Burghardtplacement new causes crashID0001960:
**This issue was created automatically from Mantis Issue 1960. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001960:
**This issue was created automatically from Mantis Issue 1960. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001960 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
124.cpp:5:[fclang] failure: Wrong number of arguments in function call (expected 2, got 0)
[kernel] Current source was: 124.cpp:5
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert.ml", line 601, characters 19-79
Called from file "src/frama-clang/convert.ml", line 875, characters 31-57
Called from file "src/frama-clang/convert.ml", line 1132, characters 20-53
Called from file "src/frama-clang/convert.ml", line 1275, characters 20-46
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1265, characters 17-40
Called from file "src/frama-clang/convert.ml", line 2151, characters 21-44
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
## Attachments
- [124.cpp](/uploads/71566326db9e49039b74bf124e12fee7/124.cpp)Virgile PrevostoVirgile Prevostohttps://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/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/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/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/841Wp can't prove validity of access to public variable from superclass2021-02-22T14:02:09ZJochen BurghardtWp can't prove validity of access to public variable from superclassID0001963:
**This issue was created automatically from Mantis Issue 1963. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001963:
**This issue was created automatically from Mantis Issue 1963. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001963 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running Wp (with rte) on the attached file "128.cpp" results in one obligation unproven by Alt-Ergo, see the attached file "_ZN1BEC1_assert_rte_mem_access_Alt-Ergo.mlw".
In the latter file, the name "valid_rw" appears only in the goal (line 566-573), in the definition (l.464-466), and in 2 axioms (l.468-470, 477-480).
None of these axioms can be used to prove a goal of the form "... -> valid_rw(...,...,...)", since they contain "valid_rw" only at negated positions.
However, using the definition would require to establish a relations between "t" and "t1", in order to show "... & ...<=t[...] -> ...<=t1[...]". Probably, something like e.g. "t=t1" is missing amount the preconditions of the goal.
The .mlw file remains literally the same if a call ":A()" is inserted in the B() constructor definition in line 8.
BTW: I wonder why "valid_rw" can be applied to "t" which has type "int farray", while the definition says the first argument should have the type "(int,int) farray". However, Alt-Ergo doesn't complain about ill-typedness.
## Attachments
- [128.cpp](/uploads/d8a9595d7860e5dc446d1919753f1185/128.cpp)
- [_ZN1BEC1_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/70cb7046724b12759e6fc1d6ce188318/_ZN1BEC1_assert_rte_mem_access_Alt-Ergo.mlw)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/833error message "unknown identifier 'xxx'" causes Frama-C to forget previous mo...2021-02-22T14:01:54ZJochen Burghardterror message "unknown identifier 'xxx'" causes Frama-C to forget previous more severe errorsID0002033:
**This issue was created automatically from Mantis Issue 2033. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002033:
**This issue was created automatically from Mantis Issue 2033. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002033 | Frama-Clang | Plug-in > clang | public | 2014-12-15 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In its current form (cf. issue #2032), the complete output of "frama-c -wp 405.cpp" looks like:
Now output intermediate result
405.cpp:6:[kernel] user error: Cannot find field salary
[kernel] user error: skipping file "405.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
However, if a non-declared variable (e.g. "xxx") is added to the "assigns" clause in line 5, the subsequent call to the wp plugin is no longer suppressed; the complete output then looks:
405.cpp:5:26: unknown identifier 'xxx'
Now output intermediate result
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
If there is some Frama-C-internal variable holding the severity of
errors detected so far, the "Cannot find field salary" error seems to
set it to a high level (thus suppressing the wp call), which is ok;
however the "unknown identifier 'xxx'" seems to lower that level again
(thus re-enabling the wp call), which is probably not ok.
## Attachments
- [405.cpp](/uploads/fe7b7b538990b1a71e7de87d63e0922a/405.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/832illegal keyword in contract causes rest to be tacitly ignored2021-02-22T14:01:54ZJochen Burghardtillegal keyword in contract causes rest to be tacitly ignoredID0001989:
**This issue was created automatically from Mantis Issue 1989. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001989:
**This issue was created automatically from Mantis Issue 1989. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001989 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output of "frama-c -wp 153.cpp":
Now output intermediate result
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
An error message should be issued about the unrecognized keyword "wssigns" in line 3, and possibly also about the unknown identifier "w" in line 4.
## Attachments
- [153.cpp](/uploads/da24568d4d9fe766b319043c7187e2b6/153.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/831missing ";" after clause causes its tacit omission2021-02-22T14:01:54ZJochen Burghardtmissing ";" after clause causes its tacit omissionID0001976:
**This issue was created automatically from Mantis Issue 1976. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001976:
**This issue was created automatically from Mantis Issue 1976. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001976 | Frama-Clang | Plug-in > clang | public | 2014-11-20 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The goal "typed_main_assert" generated from the file "141.cpp" can't be proven; the corresponding .mlw file contains the goal formula "goal main_assert: forall i : int. is_sint32(i) -> (111 = i)"; that is, the "ensures" clause from line 2 isn't used there.
If the missing ";" at the end of line 2 is appended, the generated goal reads "goal main_assert: forall i : int. (222 = (2 * i)) -> is_sint32(i) -> (111 = i)", and is proven by Alt-Ergo.
No warning or error message about the missing ";" is issued. When the file is renamed to "141.c", frama-c prints an error message "141.c:2:[kernel] user error: expecting ';' before end of annotation".
## Attachments
- [141.cpp](/uploads/a78879845eac9a5610cf9c89525d755d/141.cpp)Virgile PrevostoVirgile Prevosto