frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T14:02:14Zhttps://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/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/668path to non-existing directory given to framaCIRGen2021-02-22T13:26:29ZJochen Burghardtpath to non-existing directory given to framaCIRGenID0001954:
**This issue was created automatically from Mantis Issue 1954. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001954:
**This issue was created automatically from Mantis Issue 1954. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001954 | Frama-Clang | Plug-in > clang | public | 2014-11-06 | 2015-04-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe131.1 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When investigating issue #1953, in order to find out the appropriate command-line arguments for framaCIRGen, I called "frama-c -cxx-clang-command=echo 000.cpp" and got the output
-target i386-unknown-linux-gnu -I /usr/local/share/libc++ -I /usr/local/share/frama-c/libc -I /usr/local/share/frama-c --stop-annot-error 000a.cpp -o /tmp/clang_astb9af51ast
(before frama-c crashed due to lack of stdin input).
However, the first include path, "/usr/local/share/libc++", points to a non-existing directory. This need not be a problem, but it could be. In particular, some include files could be missing that are expected to reside in /usr/local/share/libc++.
### Additional Information :
No need to attach the trivial file 000.cpp here; any file will do.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/880public variables of superclass not visible in subclass invariant2021-02-22T14:02:19ZJochen Burghardtpublic variables of superclass not visible in subclass invariantID0001959:
**This issue was created automatically from Mantis Issue 1959. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001959:
**This issue was created automatically from Mantis Issue 1959. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001959 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **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
120.cpp:9:[kernel] user error: Cannot find field a
If "a ==" is deleted from line 9, the error message disappears.
Note that "a" is visible in the code in line 11.
## Attachments
- [120.cpp](/uploads/64602eaf38dd440ae1fe439ce89706fd/120.cpp)
- [127.cpp](/uploads/cd8fe9eacdedaad20a6a8966f6923c25/127.cpp)
- [120a.cpp](/uploads/00f63c1e84fb84a81269bc2d3301d26d/120a.cpp)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/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/667"=" in contract causes abort rather than syntax error message2021-02-22T13:08:31ZJochen Burghardt"=" in contract causes abort rather than syntax error messageID0001964:
**This issue was created automatically from Mantis Issue 1964. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001964:
**This issue was created automatically from Mantis Issue 1964. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001964 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-04-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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:
framaCIRGen: src/frama-clang/ACSLTermOrPredicate.cpp:7053: Parser::ReadResult Acsl::TermOrPredicate::readToken(Parser::State &, Parser::Arguments &): Assertion `false' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
## Attachments
- [130.cpp](/uploads/e09ffb81bdc68a67486b3af38d8eddc9/130.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/889use of template class in default template argument in namespace causes crash2021-02-22T13:14:16ZJochen Burghardtuse of template class in default template argument in namespace causes crashID0001970:
**This issue was created automatically from Mantis Issue 1970. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001970:
**This issue was created automatically from Mantis Issue 1970. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001970 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
135.cpp:6:[fclang] failure: Unknown aggregate type std::vector<...,...>
[kernel] Current source was: 135.cpp:6
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_env.ml", line 269, characters 43-71
Called from file "src/frama-clang/convert.ml", line 162, characters 17-69
Called from file "src/frama-clang/convert.ml", line 170, characters 17-52
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1283, characters 13-45
Called from file "src/frama-clang/convert.ml", line 1910, characters 8-66
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1998, characters 19-78
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.
The problem remains if the "std::" prefix is removed in line 5.
However, the problem disappears if no namespaces are used at all, i.e. if line 2 and 7 are deleted, and the "std::" prefixes are removed in line 5 and 9.
(Importance: this code is used via #include <vector>.)
## Attachments
- [135.cpp](/uploads/ea988c45a4d3e96baf392b9da299f9f7/135.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/650template parameter type can't used in typedef2021-02-22T13:08:05ZJochen Burghardttemplate parameter type can't used in typedefID0001972:
**This issue was created automatically from Mantis Issue 1972. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001972:
**This issue was created automatically from Mantis Issue 1972. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001972 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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:
Now output intermediate result
136.cpp:6:[kernel] failure: Cannot find type _ZN6traitsIiE2stE2tp (kind:type)
The problem disappears if the surrounding "struct st {" and "};" is deleted in line 3, and "st::" is deleted in line 6.
BTW: A call of "c++filt -n _ZN6traitsIiE2stE2tp" yields "traits<int>::st(tp)", while I would have expected "traits<int>::st::tp".
(Importance: this code is used via #include <vector>.)
Other issues that involve both typedef and templates were/are #1705, #1580, #1531. One of them might be related to the problem here.
## Attachments
- [136.cpp](/uploads/7681db01d5299465de8a20e5ebe39490/136.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/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 Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/804false assertion apparently undetected in the presence of overloaded virtual f...2021-02-22T13:12:20ZJochen Burghardtfalse assertion apparently undetected in the presence of overloaded virtual functionsID0001975:
**This issue was created automatically from Mantis Issue 1975. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001975:
**This issue was created automatically from Mantis Issue 1975. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001975 | Frama-Clang | Plug-in > clang | public | 2014-11-20 | 2015-02-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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" on the attached file generates 117 proof obligations of which 43 can be proven. I suppose that the obligation for the false assertion from line 19 is also proven, by qed; probably it has the name "typed_main_assert".
My reasons are:
If the assertion wasn't proven, an .mlw file for Alt-Ergo should appear in the wp-out directory which should contain the string "333"; however, no that string couldn't be found there, nor could "111"; while "222" occurs (in many/all .mlw files) only as value of the global variable "G__ZN6SquareE12_frama_c_vmt_221" which, in turn, is used only as index to an int array "t" and as an argument to "region" in global variables axioms, i.e. "222" doesn't occur in a goal.
If the value "333" in line 19 of file 139.cpp is changed to "222", i.e. if the assertion is made true, then the very same proof goal names and Valid/Unknown/Timeout results appear in the verification log. Similarly, if the value is changed to "111". All three log differ only in prover timings and obligation order, as can be seen by applying the shell-script "normalizeVerificationLog.sh" to the 117 obligation log lines in each of the log files "139_111orig.txt", "139_222orig.txt", and "139_333orig.txt" (all files attached).
Possibly, some precondition equivalent to \false is given to qed together with the goal for the line 19 assertion.
## Attachments
- [139.cpp](/uploads/ef54ab397fe24e7f040155064b4cbe62/139.cpp)
- [normalizeVerificationLog.sh](/uploads/dcc5ba9bf493c9ed7dd9a93ff699baa9/normalizeVerificationLog.sh)
- [139_111orig.txt](/uploads/d46a11670a724511c9293096ea0f790b/139_111orig.txt)
- [139_222orig.txt](/uploads/b31db051941cf23713b5f74417a79750/139_222orig.txt)
- [139_333orig.txt](/uploads/62f230fcf7b7523510583b46e105480c/139_333orig.txt)
- [139a.cpp](/uploads/8d62c589f4a19d553396ee705e4ef581/139a.cpp)
- [139a.fc_log](/uploads/fe53caffaae1a7cbdec8f3b76dfc4889/139a.fc_log)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/887use of initialized array causes crash2021-02-22T13:27:04ZJochen Burghardtuse of initialized array causes crashID0001986:
**This issue was created automatically from Mantis Issue 1986. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001986:
**This issue was created automatically from Mantis Issue 1986. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001986 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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:
Now output intermediate result
149.cpp:4:[fclang] failure: Unknown local variable a
[kernel] Current source was: 149.cpp:4
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 210, characters 8-39
Called from file "src/frama-clang/convert.ml", line 387, characters 33-55
Called from file "src/frama-clang/convert.ml", line 434, characters 29-52
Called from file "src/frama-clang/convert.ml", line 567, characters 29-52
Called from file "src/frama-clang/convert.ml", line 421, characters 29-52
Called from file "src/frama-clang/convert.ml", line 1082, characters 25-48
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.
The problem disappears if "a" isn't initialized in line 3, i.e. if "= {11,22,33}" is removed there.
## Attachments
- [149.cpp](/uploads/51ab1c38b8c7d36f3e7e7306fef9b130/149.cpp)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 Prevosto