frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:08:41Zhttps://git.frama-c.com/pub/frama-c/-/issues/673virtual base class causes error2021-02-22T13:08:41ZJochen Burghardtvirtual base class causes errorID0002075:
**This issue was created automatically from Mantis Issue 2075. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002075:
**This issue was created automatically from Mantis Issue 2075. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002075 | Frama-Clang | Plug-in > clang | public | 2015-02-05 | 2015-03-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 454.cpp (external front-end)
Now output intermediate result
454.cpp:7:[kernel] user error: Cannot find field _frama_c__Z1A
[kernel] user error: stopping on file "454.cpp" that has errors.
The error message disappears if the contructor definition in line 7 is deleted, or if the "virtual" is deleted in line 4.
## Attachments
- [454.cpp](/uploads/4a7365082cdfd5d01d0cea781a1c31b2/454.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/670value analysis assumes dynamic_cast between unrelated classes to succeed, rat...2021-02-22T13:08:36ZJochen Burghardtvalue analysis assumes dynamic_cast between unrelated classes to succeed, rather than to yield NULLID0002076:
**This issue was created automatically from Mantis Issue 2076. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002076:
**This issue was created automatically from Mantis Issue 2076. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002076 | Frama-Clang | Plug-in > clang | public | 2015-02-09 | 2015-04-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -val 461.cpp" on the attached program yields the output (excerpt):
461.cpp:10:[value] Assertion got status valid.
However, running "clang++ 461.cpp && ./a.out" reveals that the assertion in line 12 (identical to that in line 11) is in fact invalid:
a.out: 461.cpp:11: int main(): Assertion `bp!=0' failed.
Compiling "g++ 461.cpp" even yields a compile-time warning:
461.cpp: In function ‘int main()’:
461.cpp:9:37: warning: dynamic_cast of ‘A aaa’ to ‘struct B*’ can never succeed [enabled by default]
B* const bp = dynamic_cast<B*>(&aaa);
^
## Attachments
- [461.cpp](/uploads/20b05a3ffead132fae7718ee75d4dece/461.cpp)
- [461_bis.cpp](/uploads/07b4979e4c6b1bdf3d7b1eb9d20722fe/461_bis.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/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/666indexing of string literal apparently causes memory leak in framaCIRGen2021-02-22T13:40:05ZJochen Burghardtindexing of string literal apparently causes memory leak in framaCIRGenID0001988:
**This issue was created automatically from Mantis Issue 1988. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001988:
**This issue was created automatically from Mantis Issue 1988. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001988 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-04-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
When running "frama-c 151.cpp" on the attached program, about 1 minute of silence is observed on the terminal output, followed by:
Killed
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Running "top -d 1" produces the figures shown in file "151.typescript": framaCIRGen acquires about 90MB memory each second until it has 1.8GB after 18 seconds; then the memory remains constant for another 18 seconds; then the process appears to be killed by the Linux kernel due to memory exhaustion.
## Attachments
- [151.cpp](/uploads/22b5baf2a7db1b3084d4da78b008cbaf/151.cpp)
- [151.typescript](/uploads/b4a76f523493de4fe8ab69804480ce6b/151.typescript)
- [156.cpp](/uploads/fb17a0983991ed74ce7fe3d23ce44028/156.cpp)
- [156.typescript](/uploads/1dc0c1b0d4a1e83a9be18b27027d3979/156.typescript)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/664use of "CLASSNAME::VARIABLENAME" in assigns clase causes abort2021-02-22T13:08:27ZJochen Burghardtuse of "CLASSNAME::VARIABLENAME" in assigns clase causes abortID0002074:
**This issue was created automatically from Mantis Issue 2074. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002074:
**This issue was created automatically from Mantis Issue 2074. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002074 | Frama-Clang | Plug-in > clang | public | 2015-02-05 | 2015-04-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 455.cpp (external front-end)
framaCIRGen: SemaLookup.cpp:1622: bool clang::Sema::LookupQualifiedName(clang::LookupResult &, clang::DeclContext *, bool): Assertion `(!isa<TagDecl>(LookupCtx) || LookupCtx->isDependentContext() || cast<TagDecl>(LookupCtx)->isCompleteDefinition() || cast<TagDecl>(LookupCtx)->isBeingDefined()) && "Declaration context must already be complete!"' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Cf. #1944 for a similar problem in an "ensures" clause.
If the prefix "Employee::" is deleted in the assigns clause in line 11, a warning is issued instead:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 455.cpp (external front-end)
Now output intermediate result
455.cpp:12:[kernel] user error: Cannot find field dept
[kernel] user error: stopping on file "455.cpp" that has errors.
As a consequence of both behaviors, it is impossible to write an "assigns" clause for a subclass method that refers to a member of a superclass.
## Attachments
- [455.cpp](/uploads/2b4202f07be66f6e527f8c274d7e5300/455.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/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/649declaration of local variable of class type results in unprovable assigns clause2021-02-22T13:08:04ZJochen Burghardtdeclaration of local variable of class type results in unprovable assigns clauseID0002106:
**This issue was created automatically from Mantis Issue 2106. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002106:
**This issue was created automatically from Mantis Issue 2106. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002106 | Frama-Clang | Plug-in > clang | public | 2015-04-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The assigns clause in line 4 of the attached program results in two Alt-Ergo obligations (such as "goal _Z3foo_assign_normal: forall t : int farray. not linked(t)" in obligation file "_Z3foo_assign_normal_Alt-Ergo.mlw"), none of which is provable.
However, from a C++ programmer's point of view, the clause should be valid.
Probably, some Frama-Cxx-internal variables are assigned by the implicit constructor "A()", and hence by "foo()", but there is no clue how to refer to them. Maybe they should be added automatically by Frama-Cxx to the set of assigned locations.
## Attachments
- [469.cpp](/uploads/a03e4e3a40b48a76922e10de413446fb/469.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/648use of body-declared variable in loop annotation causes crash2021-02-22T14:01:53ZJochen Burghardtuse of body-declared variable in loop annotation causes crashID0001997:
**This issue was created automatically from Mantis Issue 1997. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001997:
**This issue was created automatically from Mantis Issue 1997. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001997 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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
161.cpp:3:[fclang] failure: Unknown local variable s
[kernel] Current source was: 161.cpp:3
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_acsl.ml", line 317, characters 18-77
Called from file "src/frama-clang/convert_acsl.ml", line 303, characters 13-52
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 272, characters 4-30
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 385, characters 13-38
Called from file "src/frama-clang/convert_acsl.ml", line 363, characters 11-42
Called from file "src/frama-clang/convert_acsl.ml", line 586, characters 14-40
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1179, characters 18-70
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 remains if line 3 is changed to "//@ loop assigns s;", and if "s" is declared "static int" (in which case a reference to "s" in a loop annotation makes sense).
## Attachments
- [161.cpp](/uploads/5bfc197761d406d5ad0e3f804e293cad/161.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/647variable declared in loop initializer is unknown in loop body "assert"2021-02-22T13:54:40ZJochen Burghardtvariable declared in loop initializer is unknown in loop body "assert"ID0002108:
**This issue was created automatically from Mantis Issue 2108. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002108:
**This issue was created automatically from Mantis Issue 2108. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002108 | Frama-Clang | Plug-in > clang | public | 2015-04-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 471.cpp (external front-end)
471.cpp:5:17: unknown identifier 'i'
Now output intermediate result
The error message disappears if
(1) the "assert" in line 5 is deleted (i.e. "i" is known in the "loop assigns" clause in line 3), or
(2) the declaration of "i" is moved before line 3.
### Additional Information :
Ubuntu clang version 3.4-1ubuntu3 (tags/RELEASE_34/final) (based on LLVM 3.4)
## Attachments
- [471.cpp](/uploads/e8841adebbb2c9c95ac3128188b487e6/471.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/646loop invariant referring to body-local variable causes crash, when body is en...2021-03-29T17:09:18ZJochen Burghardtloop invariant referring to body-local variable causes crash, when body is enclosed in curly braces "{...}"ID0002107:
**This issue was created automatically from Mantis Issue 2107. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002107:
**This issue was created automatically from Mantis Issue 2107. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002107 | Frama-Clang | Plug-in > clang | public | 2015-04-27 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 470.cpp (external front-end)
Now output intermediate result
470.cpp:3:[fclang] failure: Unknown local variable s
[kernel] Current source was: 470.cpp:3
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 "convert_acsl.ml", line 329, characters 18-77
Called from file "convert_acsl.ml", line 315, characters 13-52
Called from file "convert_acsl.ml", line 184, characters 38-72
Called from file "convert_acsl.ml", line 284, characters 4-30
Called from file "convert_acsl.ml", line 184, characters 38-72
Called from file "convert_acsl.ml", line 397, characters 13-38
Called from file "convert_acsl.ml", line 375, characters 11-42
Called from file "convert_acsl.ml", line 603, characters 14-40
Called from file "list.ml", line 55, characters 20-23
Called from file "convert.ml", line 1248, characters 18-70
Called from file "convert.ml", line 1344, characters 20-46
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 1334, characters 17-40
Called from file "convert.ml", line 2508, characters 21-44
Called from file "convert.ml", line 2642, characters 21-41
Called from file "list.ml", line 84, characters 24-34
Called from file "convert.ml", line 2645, characters 4-74
Called from file "frama_Clang_register.ml", line 120, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 84, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, 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 763, 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 Sodium-20150201.
The crash doesn't happen when
(1) the braces "{" and "}" in line 5 and 7 are deleted,
(2) "s" is replaced by "0" in the invariant in line 3,
(3) the declaration of "s" in line 6 is deleted,
(4) the file is renamed to "470.c".
In each of these cases, an appropriate error message is printed.
### Additional Information :
My output of "clang --version" is:
Ubuntu clang version 3.4-1ubuntu3 (tags/RELEASE_34/final) (based on LLVM 3.4)
Target: x86_64-pc-linux-gnu
Thread model: posix
## Attachments
- [470.cpp](/uploads/25f4766330a52880d319ebc21f807ac9/470.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/643insufficient preconditions given to verify constructor call from global varia...2021-02-22T14:02:18ZJochen Burghardtinsufficient preconditions given to verify constructor call from global variable initializationID0002003:
**This issue was created automatically from Mantis Issue 2003. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002003:
**This issue was created automatically from Mantis Issue 2003. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002003 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-05-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 predonditions of the cls() constructor aren't verified for the call originating from the declaration in line 9. The goal in the .mlw file is just "forall i : int. is_sint32(i) -> (0 <> i)", i.e. the fact that i (that is x in the C++ source) has the value 2 isn't given as precondition.
In contrast, when cls() is called explicitly in main(), the actual value of x is given - the .mlw file's goal for line 13 reads: "... -> (0 <> (safe_comp_div(1, 2)))". Note that here the effect of the line-9 cls()-call is ignored in x-value computation; in fact, already the cls()-call in line 12 will crash with zero-divide.
This issues is probably closely related to #2002.
## Attachments
- [178.cpp](/uploads/5a04d189eb4a14ee24fb23392f9ea5b5/178.cpp)
- [476.cpp](/uploads/383651d9a385b7199be6833e66e52491/476.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/642can't prove (trivial) validity of memory access of "p->a"2021-02-22T13:07:57ZJochen Burghardtcan't prove (trivial) validity of memory access of "p->a"ID0002112:
**This issue was created automatically from Mantis Issue 2112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002112:
**This issue was created automatically from Mantis Issue 2112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002112 | Frama-Clang | Plug-in > clang | public | 2015-05-04 | 2015-05-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte 477.cpp" on the attached program leaves an obligation "typed_main_assert_rte_mem_access" unproven by Alt-Ergo. It goal formula in file "main_assert_rte_mem_access_Alt-Ergo.mlw" reads:
576 goal main_assert_rte_mem_access:
577 forall t_1,t : int farray.
578 linked(t) ->
579 valid_rw(t_1, shiftfield_F__Z1X_a(shift__Z1X(global(L_x_111), 0)), 1)
When "t" is changed to "t_1" in line 578, the formaula is proven. This looks as if an "assigns" clause is missing for some operator. However, there is no user-defined operator involved here, so the necessary "assigns" clause should be generated by Frama-C.
## Attachments
- [477.cpp](/uploads/cabf9f2eb5e5c7118db6400bf14d3275/477.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/640declarations of static variable of class type in function body causes crash2021-03-29T17:24:55ZJochen Burghardtdeclarations of static variable of class type in function body causes crashID0002001:
**This issue was created automatically from Mantis Issue 2001. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002001:
**This issue was created automatically from Mantis Issue 2001. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002001 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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
161.cpp:3:[fclang] failure: Unknown local variable s
[kernel] Current source was: 161.cpp:3
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_acsl.ml", line 317, characters 18-77
Called from file "src/frama-clang/convert_acsl.ml", line 303, characters 13-52
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 272, characters 4-30
Called from file "src/frama-clang/convert_acsl.ml", line 172, characters 38-72
Called from file "src/frama-clang/convert_acsl.ml", line 385, characters 13-38
Called from file "src/frama-clang/convert_acsl.ml", line 363, characters 11-42
Called from file "src/frama-clang/convert_acsl.ml", line 586, characters 14-40
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1179, characters 18-70
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
(1) the "static" is deleted in line 5, or
(2) "cls" is changed to "int" in line 5.
Could be related to #1997, since the crash messages agree. I dind't check the full call stack, however.
## Attachments
- [173.cpp](/uploads/bc77682336214d038cb4267b460d0df8/173.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/638access to static struct fields unsupported in annotation2021-02-22T13:39:53ZJochen Burghardtaccess to static struct fields unsupported in annotationID0002116:
**This issue was created automatically from Mantis Issue 2116. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002116:
**This issue was created automatically from Mantis Issue 2116. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002116 | Frama-Clang | Plug-in > clang | public | 2015-05-07 | 2015-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 479.cpp (external front-end)
479.cpp:9:18: Unsupported Field Access to s in struct Cl
Now output intermediate result
(Despite the error message, provers are called, when command-line option "-wp" is used.)
The error disappears if (line 8 is activated and) line 9 is deactivated.
## Attachments
- [479.cpp](/uploads/abca3d8bf2819f8cdb4b49d9f829011c/479.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/588mixed virtual/nonvirtual base class causes error2021-02-22T13:39:25ZJochen Burghardtmixed virtual/nonvirtual base class causes errorID0002077:
**This issue was created automatically from Mantis Issue 2077. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002077:
**This issue was created automatically from Mantis Issue 2077. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002077 | Frama-Clang | Plug-in > clang | public | 2015-02-09 | 2015-10-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 462.cpp (external front-end)
Now output intermediate result
462.cpp:5:[kernel] failure: Cannot resolve variable __frama_c_arg_0
[kernel] user error: stopping on file "462.cpp" that has errors.
If "virtual" is deleted in line 4, the error disappears; similarly if "virtual" is inserted in line 3.
Since in Stroustrup's book no mixed virtual/nonvirtual base class is discussed, the example in file "462.cpp" may not be of any relevance. However, the clang++ compiler accepts that file without any problems.
## Attachments
- [462.cpp](/uploads/6c5857ed398e1a937d5fade5314a5a1e/462.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/289std::bad_alloc not supported2021-02-22T12:58:19ZJens Gerlachstd::bad_alloc not supportedID0002342:
**This issue was created automatically from Mantis Issue 2342. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002342:
**This issue was created automatically from Mantis Issue 2342. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002342 | Frama-C | Plug-in > clang | public | 2018-01-18 | 2018-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | linux | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Attached is a simple C++ (03) program that checks whether 'new' has thrown an exception.
I am not yet sure whether this is due to general lack of exceptions or just a library issue.
I report just for completeness.
### Steps To Reproduce :
Call 'frama-c -val new_bad_alloc.cpp'
## Attachments
- [new_bad_alloc.cpp](/uploads/d2abd5208e0f45238cee308e702b69b7/new_bad_alloc.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/288range based for loop from C++11 not supported2021-02-22T12:58:19ZJens Gerlachrange based for loop from C++11 not supportedID0002345:
**This issue was created automatically from Mantis Issue 2345. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002345:
**This issue was created automatically from Mantis Issue 2345. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002345 | Frama-C | Plug-in > clang | public | 2018-01-19 | 2018-01-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached example compiles without waring in C++11 mode
g++ --std=c++11 -Wall -c -o range_based_for_loop.o range_based_for_loop.cpp
but it fails with
frama-c -val range_based_for_loop.cpp
Error message says:
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "range_based_for_loop.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
## Attachments
- [range_based_for_loop.cpp](/uploads/06215bb4a9f91910a1a0bacff4ffa79f/range_based_for_loop.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/287C++11 delegating constructor not supported2021-02-22T12:58:18ZJens GerlachC++11 delegating constructor not supportedID0002346:
**This issue was created automatically from Mantis Issue 2346. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002346:
**This issue was created automatically from Mantis Issue 2346. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002346 | Frama-C | Plug-in > clang | public | 2018-01-19 | 2018-01-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached two examples for with g++ in C++11 mode.
The first example is pure C++03. Fram-Clang can handle it.
The second version uses a delegation constructor.
Frama-Clang fails on this one with the error message:
frama-c -val object_construction2.cpp
[kernel] Parsing object_construction2.cpp (external front-end)
Unsupported constructor initializer:SomeType
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "object_construction2.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
### Additional Information :
frama-clang 0.0.4
## Attachments
- [object_construction1.cpp](/uploads/9470c7f8b2af8d771a6a8e48784a42c4/object_construction1.cpp)
- [object_construction2.cpp](/uploads/7f0b7bc342fb3b3b749aafd7bce30c70/object_construction2.cpp)Virgile PrevostoVirgile Prevosto