frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:39:53Z
https://git.frama-c.com/pub/frama-c/-/issues/638
access to static struct fields unsupported in annotation
2021-02-22T13:39:53Z
Jochen Burghardt
access to static struct fields unsupported in annotation
ID0002116:
**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 Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/896
ACSL comment rejected in function template
2021-02-22T13:27:13Z
Jochen Burghardt
ACSL comment rejected in function template
ID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002048 | Frama-Clang | Plug-in > clang | public | 2015-01-12 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 430.cpp (external front-end)
inadequate comment at 430.cpp:5:2
If line 2 is commented-in and line 3 is commented-out, the error message disappears.
## Attachments
- [430.cpp](/uploads/fb7c1b9a2c7e740eb0e5c7200661ce99/430.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/838
ACSL parsing of greater-than relation with references
2021-02-22T13:13:04Z
Virgile Prevosto
ACSL parsing of greater-than relation with references
ID0001921:
**This issue was created automatically from Mantis Issue 1921. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001921:
**This issue was created automatically from Mantis Issue 1921. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001921 | Frama-Clang | Plug-in > clang | public | 2014-09-12 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | fixed |
| **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 :
On the following code:
/*@
ensures \result >= x;
*/
int f(int& x) { return ++x; }
/*@
ensures \result == x;
*/
int g(int& x) { return x; }
/*@
ensures \result >= x;
*/
int h(int x) { return x; }
contracts for g and h are correctly parsed, while contract of f produces the following error messages:
tests/specs/ref_spec.cpp:2:23: comparison of incompatible array types
tests/specs/ref_spec.cpp:2:23: expecting a term or predicate
tests/specs/ref_spec.cpp:2:23: the term is not a predicate
https://git.frama-c.com/pub/frama-c/-/issues/280
Alt-Ergo reports about " bool and int cannot be unified"
2021-02-22T14:01:05Z
Jens Gerlach
Alt-Ergo reports about " bool and int cannot be unified"
ID0002355:
**This issue was created automatically from Mantis Issue 2355. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002355:
**This issue was created automatically from Mantis Issue 2355. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002355 | Frama-C | Plug-in > clang | public | 2018-02-05 | 2018-02-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
If the attached simple C++ file is processed with the command line
frama-c -wp -wp-rte -warn-unsigned-downcast -wp-out equal.wp++ equal.cpp
then the following error message occurs:
[wp] [Alt-Ergo] Goal typed__Z5equali_assert_rte_unsigned_downcast : Failed
characters 4-22:typing error: bool and int cannot be unified
Could it be that Frama-Clang (or WP?) treats the return value of operator == as int instead of bool?
### Additional Information :
The error message disappears when the option "-warn-unsigned-downcast" is omitted.
## Attachments
- [equal.cpp](/uploads/cce7e3046290d9c1834fbf000d996488/equal.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/963
array-type parameter causes "Old style K&R" kernel warning with cxx plugin
2021-02-22T13:27:57Z
Jochen Burghardt
array-type parameter causes "Old style K&R" kernel warning with cxx plugin
ID0001814:
**This issue was created automatically from Mantis Issue 1814. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001814:
**This issue was created automatically from Mantis Issue 1814. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001814 | Frama-Clang | Plug-in > clang | public | 2014-06-20 | 2014-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
output:
Now output intermediate result
taint02.cpp:7:[kernel] warning: Calling undeclared function _Z3fooPi. Old style K&R code?
The warning disappears if the file is renamed to "taint02.c".
## Attachments
- [taint02.cpp](/uploads/0071ae679c085de2390e5212762dc45d/taint02.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/273
"assigns" in statement contract causes abort or crash
2021-02-22T12:58:03Z
Jochen Burghardt
"assigns" in statement contract causes abort or crash
ID0002361:
**This issue was created automatically from Mantis Issue 2361. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002361:
**This issue was created automatically from Mantis Issue 2361. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002361 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c remove_cpp.cpp" on the attached program outputs
"framaCIRGen: ACSLStatementAnnotation.cpp:248: Parser::Base::ReadResult Acsl::StatementAnnotation::readToken(Acsl::Parser::State&, Acsl::Parser::Arguments&): Assertion `false' failed."
and then aborts. If the "ensures" clause in line 5 is removed, Frama-C outputs instead:
"*** Error in `framaCIRGen': double free or corruption (out): 0x0000559f983d0160 ***"
and then aborts, too. If in addition "a[0..9]" is removed from the "assigns" claus in line 4, Frama-C crashes (Segmentation fault) without printing any error message before. For the latter reason, I've set the severity to "crash".
## Attachments
- [remove_cpp.cpp](/uploads/2af0af96279845d9332c5293876e6c3e/remove_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/904
"\at" doesn't accept predicate argument label
2021-02-22T13:14:33Z
Jochen Burghardt
"\at" doesn't accept predicate argument label
ID0002066:
**This issue was created automatically from Mantis Issue 2066. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002066:
**This issue was created automatically from Mantis Issue 2066. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002066 | Frama-Clang | Plug-in > clang | public | 2015-01-26 | 2015-02-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **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 444.cpp (external front-end)
444.cpp:2:44: expecting a label in the \at construct
Now output intermediate result
The message disappears when the file is renamed to "444.c".
## Attachments
- [444.cpp](/uploads/3f08cdd8c2d7381ec3a22c2725f249af/444.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/287
C++11 delegating constructor not supported
2021-02-22T12:58:18Z
Jens Gerlach
C++11 delegating constructor not supported
ID0002346:
**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 Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/903
can't compare pointer and reference for equality in contract
2021-02-22T13:14:31Z
Jochen Burghardt
can't compare pointer and reference for equality in contract
ID0002060:
**This issue was created automatically from Mantis Issue 2060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002060:
**This issue was created automatically from Mantis Issue 2060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002060 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 441.cpp (external front-end)
441.cpp:2:22: invalid implicit conversion
441.cpp:2:22: unknown type comparison for the operator ==
Now output intermediate result
When line 2 is commented out, the comparison in C++ code in line 3 is accepted.
## Attachments
- [441.cpp](/uploads/da2cc8f3623d5563d069827341da0b18/441.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/277
can't handle lemma with 3 labels
2021-02-22T12:58:06Z
Jochen Burghardt
can't handle lemma with 3 labels
ID0002357:
**This issue was created automatically from Mantis Issue 2357. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002357:
**This issue was created automatically from Mantis Issue 2357. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002357 | Frama-C | Plug-in > clang | public | 2018-02-08 | 2018-02-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp adjacent_difference_inv_cpp.cpp" on the attached program reports an error in line 6: "logic label `L' not found". The error message disappears when
(1) the file is renamed to "adjacent_difference_inv_cpp.c", and processed by plain Frama-C,
(2) the middle conjunct "foo{L}(1)" is removed in line 6, or
(3) label "M" is omitted in the header of "lem", and the rightmost conjunct is changed to "foo{L}(2)".
Consistently renaming the labels doesn't make the error message vanish.
## Attachments
- [adjacent_difference_inv_cpp.cpp](/uploads/e88a6c1225e59965e3a2ca825b8f7feb/adjacent_difference_inv_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/642
can't prove (trivial) validity of memory access of "p->a"
2021-02-22T13:07:57Z
Jochen Burghardt
can'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 Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/250
cast error with reference fields
2021-03-30T08:44:29Z
mantis-gitlab-migration
cast error with reference fields
ID0002396:
**This issue was created automatically from Mantis Issue 2396. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002396:
**This issue was created automatically from Mantis Issue 2396. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002396 | Frama-C | Plug-in > clang | public | 2018-08-24 | 2018-08-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abhishek.anand.iitg@gmail.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | manjaro | **OS Version** | 8/23/3018 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
```
class B {
};
template <typename T>
class A {
public:
T &x;
A(T &y): x(y) {}
};
int main()
{
B b;
B & y=b;
A<B> a(y);
}
```
I get the following error:
```
root@27db7a69b96a:/hostshare# frama-c -print refFieldBug.cpp
[kernel] Parsing refFieldBug.cpp (external front-end)
Now output intermediate result
[kernel] refFieldBug.cpp:8: Failure: castTo struct _Z1B -> struct _Z1B *
[kernel] User Error: stopping on file "refFieldBug.cpp" that has errors.
[kernel] Frama-C aborted: invalid user inp
```
I don't see what could be the problem because the following succeeds:
```
class A {
public:
T &x;
A(T &y): x(y) {}
};
int main()
{
int x=0;
int & y=x;
A<int> a(y);
}
```
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/940
"catch(...)" causes crash
2021-02-22T13:15:30Z
Jochen Burghardt
"catch(...)" causes crash
ID0001966:
**This issue was created automatically from Mantis Issue 1966. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001966:
**This issue was created automatically from Mantis Issue 1966. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001966 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2014-12-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **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** | Frama-C GIT, precise the release id |
### Description :
output:
Now output intermediate result
[kernel] Current source was: 133.cpp:3
The full backtrace is:
Raised at file "stack.ml", line 31, characters 20-25
Called from file "src/kernel/exn_flow.ml", line 120, characters 37-60
Called from file "list.ml", line 69, characters 12-15
Called from file "src/kernel/exn_flow.ml", line 112, characters 8-389
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2045, characters 15-31
Called from file "cil/src/cil.ml", line 3094, characters 5-86
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 3254, characters 16-40
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3483, characters 14-39
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 3445, characters 5-91
Called from file "cil/src/cil.ml", line 3537, characters 16-38
Called from file "cil/src/cil.ml", line 2084, characters 13-16
Called from file "cil/src/cil.ml", line 2129, characters 24-57
Called from file "cil/src/cil.ml", line 3531, characters 5-53
Called from file "cil/src/cil.ml", line 6156, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5746, characters 3-30
Called from file "cil/src/cil.ml", line 6157, characters 2-420
Called from file "cil/src/cil.ml", line 2060, characters 21-41
Called from file "cil/src/cil.ml", line 6190, characters 7-84
Called from file "src/kernel/visitor.ml", line 827, characters 2-45
Called from file "src/kernel/file.ml", line 1617, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1694, characters 2-36
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
Unexpected error (Stack.Empty).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
Could be related to issue #1957?
(Importance: this code is used via #include <vector>.)
## Attachments
- [133.cpp](/uploads/ec10c3fb4d765ca86e6de649c4277911/133.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/898
catching a superclass causes crash
2021-02-22T13:14:26Z
Jochen Burghardt
catching a superclass causes crash
ID0002051:
**This issue was created automatically from Mantis Issue 2051. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002051:
**This issue was created automatically from Mantis Issue 2051. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002051 | Frama-Clang | Plug-in > clang | public | 2015-01-15 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
[fclang] failure: Did not find struct for mangled class name _Z9Underflow
[kernel] Current source was: 432.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_link.ml", line 71, characters 36-53
Called from file "src/lib/FCSet.ml", line 332, characters 37-58
Called from file "src/frama-clang/convert_link.ml", line 86, characters 16-112
Called from file "src/frama-clang/convert_link.ml", line 104, characters 16-62
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert_link.ml", line 102, characters 12-142
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2046, characters 15-31
Called from file "cil/src/cil.ml", line 3095, characters 5-86
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 3255, characters 16-40
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3484, characters 14-39
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3446, characters 5-91
Called from file "cil/src/cil.ml", line 3538, characters 16-38
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 2130, characters 24-57
Called from file "cil/src/cil.ml", line 3532, characters 5-53
Called from file "cil/src/cil.ml", line 6151, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5741, characters 3-30
Called from file "cil/src/cil.ml", line 6152, characters 2-420
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 6185, characters 7-84
Called from file "src/kernel/file.ml", line 1803, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1880, characters 2-36
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 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 some member variable (e.g. "int x;") is added to the body of class "Matherr" in line 2 or/and the body of class "Underflow" in line 3.
The problem disappears if either:
(1) the definition of "Underflow" in line 3 is deleted,
(2) the definition of "foo" in line 5-10 is deleted,
(3) "Matherr" is changed to "Underflow" in the catch statement in line 8, or
(4) "public" is changed to "private" in line 3.
## Attachments
- [432.cpp](/uploads/c3a89685372790a4946ec88f8e54c293/432.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/267
C-function returning a struct causes warning on missing Ctor code/spec when i...
2021-03-30T08:24:10Z
Jochen Burghardt
C-function returning a struct causes warning on missing Ctor code/spec when inside 'extern "C" {...}'
ID0002367:
**This issue was created automatically from Mantis Issue 2367. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002367:
**This issue was created automatically from Mantis Issue 2367. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002367 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp equal_range_cpp.cpp" prints
[kernel] warning: Assuming declared function pair::Ctor can't throw any exception
equal_range_cpp.cpp:6:[kernel] warning: Neither code nor specification for function pair::Ctor, generating default assigns from the prototype
Both messages disappear when the file is renamed to "equal_range_cpp.c" and/or the leading 'extern "C" {' and the trailing '}' are removed.
## Attachments
- [equal_range_cpp.cpp](/uploads/345e6cc5ed90e78e5878e8d5736cbef8/equal_range_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/659
class expression causes abort in presence of user-defined destructor
2021-03-29T17:06:09Z
Jochen Burghardt
class expression causes abort in presence of user-defined destructor
ID0002004:
**This issue was created automatically from Mantis Issue 2004. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002004:
**This issue was created automatically from Mantis Issue 2004. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002004 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-04-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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:
Unsupported expressions:ExprWithCleanups 0x17e7dc0 <179.cpp:8:6, col:17> '_Bool'
`-CXXMemberCallExpr 0x17e7d98 <col:6, col:17> '_Bool'
`-MemberExpr 0x17e7d68 <col:6, col:12> '<bound member function type>' .test 0x1799820
`-CXXBindTemporaryExpr 0x17e7d48 <col:6, col:10> 'struct cls' (CXXTemporary 0x17e7d40)
`-CXXTemporaryObjectExpr 0x17e7d00 <col:6, col:10> 'struct cls' 'void (void)' zeroing
Aborting
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
The problem disappears if the destructor definition in line 3 is deleted.
## Attachments
- [179.cpp](/uploads/4356f9770e055afebc91022a33e22f7c/179.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/660
CLASSNAME::PREDICATENAME not recognized as predicate (or even as term)
2021-02-22T13:39:56Z
Jochen Burghardt
CLASSNAME::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 Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/874
clause labels not accepted by cxx plugin
2021-02-22T13:13:53Z
Jochen Burghardt
clause labels not accepted by cxx plugin
ID0002010:
**This issue was created automatically from Mantis Issue 2010. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002010:
**This issue was created automatically from Mantis Issue 2010. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002010 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **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:
187.cpp:2:27: expecting a term or predicate
187.cpp:2:27: expecting a predicate
Now output intermediate result
When the file is renamed to "187.c", Frama-C processes it without complaints, so I guess my syntax is correct. I failed to find this detail in the manual "acsl-implementation-Neon-20140301.pdf", cf. #2009.
## Attachments
- [187.cpp](/uploads/38bdf3aaabc360f9919bbc99cddd8bb1/187.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/1016
clause "n<9-1" normalized to "n-1<9"
2021-02-22T13:17:26Z
Jochen Burghardt
clause "n<9-1" normalized to "n-1<9"
ID0001810:
**This issue was created automatically from Mantis Issue 1810. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001810:
**This issue was created automatically from Mantis Issue 1810. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001810 | Frama-Clang | Plug-in > clang | public | 2014-06-16 | 2014-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C GIT, precise the release id |
### Description :
Running "frama-c-gui -wp -wp-rte 108.cpp -wp-out wp-out" on the attached program shows in the gui's normalized-code window the clause "requires 0 <= n-1 && n-1 < 9;" as translation of source line 5 ("requires 0 <= n < 9-1;").
The same error is found in alt-ergo's input file "_Z4push_assert_rte_index_bound_2.ergo". As a consequence, alt-ergo can't prove the index bound for line 9.
The error disappears if
* the file is renamed to "108.c",
* "9-1" is replaced by "9" in line 5.
The error appears unchanged if "n" is made a procedure parameter of "push".
## Attachments
- [108.cpp](/uploads/f07695abe8c21809455ab3b47fd664b3/108.cpp)
- [_Z4push_assert_rte_index_bound_2.ergo](/uploads/e6b954a9726185b9f5ecdbb9bd90990d/_Z4push_assert_rte_index_bound_2.ergo)
- [109.cpp](/uploads/6aac1934cfc40814903aafd21efbc26b/109.cpp)
https://git.frama-c.com/pub/frama-c/-/issues/837
Comparison of different types in acsl clause causes segmentation fault
2021-02-22T13:51:23Z
mantis-gitlab-migration
Comparison of different types in acsl clause causes segmentation fault
ID0001902:
**This issue was created automatically from Mantis Issue 1902. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001902:
**This issue was created automatically from Mantis Issue 1902. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001902 | Frama-Clang | Plug-in > clang | public | 2014-07-30 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lapawczykt | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | xubuntu 64 bit | **OS Version** | 14.04 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | - |
### Description :
A comparison between e.g. an int and a short is normaly translated to a cast and a following comparison in the normalised version. This works fine in C but in C++ a comparison of e.g. an int and a short in an acsl clause causes a segmentation fault.
## Attachments
- [problem311.cpp](/uploads/52700e19e5d6a83f949b1919c42187a1/problem311.cpp)