frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T12:58:15Z
https://git.frama-c.com/pub/frama-c/-/issues/285
unknown variable in contract is not treated as an error
2021-02-22T12:58:15Z
Jens Gerlach
unknown variable in contract is not treated as an error
ID0002348:
**This issue was created automatically from Mantis Issue 2348. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002348:
**This issue was created automatically from Mantis Issue 2348. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002348 | Frama-C | Plug-in > clang | public | 2018-01-30 | 2018-01-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached C/C++ code is treated differently by Frama-C and Frama-Clang
The C file 'unknown_variable.c' is correctly rejected by Frama-C with wit the the message
frama-c -wp -wp-rte unknown_variable.c
[kernel] user error: stopping on file "unknown_variable.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
When processing this file as C++ code
frama-c -wp -wp-rte unknown_variable.cpp
Frama-Clang only emits a warning (by the kernel) and continues processing
Parsing unknown_variable.cpp (external front-end)
unknown_variable.cpp:6:18: unknown identifier 'c'
Now output intermediate result
In my opinion, the C++ contract should be rejected as well.
## Attachments
- [unknown_variable.c](/uploads/c5a054e84514556cecef576a58a99a77/unknown_variable.c)
- [unknown_variable.cpp](/uploads/1b1624f8c2b2da94da16a415596ba498/unknown_variable.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/284
BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version"
2021-02-22T12:58:14Z
Jens Gerlach
BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version"
ID0002343:
**This issue was created automatically from Mantis Issue 2343. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002343:
**This issue was created automatically from Mantis Issue 2343. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002343 | Frama-C | Documentation | public | 2018-01-18 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version" ...
https://git.frama-c.com/pub/frama-c/-/issues/283
warning from kernel about exceptions
2021-02-22T12:58:13Z
Jens Gerlach
warning from kernel about exceptions
ID0002349:
**This issue was created automatically from Mantis Issue 2349. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002349:
**This issue was created automatically from Mantis Issue 2349. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002349 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is more a question than a bug report...
In the attached example Frama-Clang issue the warning
frama-c -wp -wp-rte exception_warning.cpp
[kernel] Parsing exception_warning.cpp (external front-end)
Now output intermediate result
[kernel] warning: Assuming declared function bar can't throw any exception
This also occurs when I add "noexcept" to the declaration of "bar".
(see second file: exception_warning_noexcept.cpp)
Is there a way to declare in the contract that a function cannot throw?
Or what do I have to do to get rid of this warning?
## Attachments
- [exception_warning.cpp](/uploads/1c9349ade800a02746a00368ccb273fc/exception_warning.cpp)
- [exception_warning_noexcept.cpp](/uploads/de71f4c8b161448d91413e4af41e8b4d/exception_warning_noexcept.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/282
no diagnostics on wrong keyword
2021-03-30T07:48:10Z
Jens Gerlach
no diagnostics on wrong keyword
ID0002351:
**This issue was created automatically from Mantis Issue 2351. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002351:
**This issue was created automatically from Mantis Issue 2351. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002351 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
The attached ACSL/C code contains a typo in the assigns clause:
"assign" instead of "assigns".
Frama-Clang provides no diagnostic message on this
frama-c -wp -wp-rte wrong_keyword.cpp
[kernel] Parsing wrong_keyword.cpp (external front-end)
Now output intermediate result
[rte] annotating function foo
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
When processed as a normal C file by Frama-C/WP a more appropriated message is shown
frama-c -wp -wp-rte wrong_keyword.c
[kernel] Parsing wrong_keyword.c (with preprocessing)
wrong_keyword.c:5:[kernel] user error: unexpected token 'a'
[kernel] user error: stopping on file "wrong_keyword.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
## Attachments
- [wrong_keyword.cpp](/uploads/577364237c433e7a05c5ae2104548eda/wrong_keyword.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/281
Frama-Clang crashes on error in contract
2021-02-22T13:36:01Z
Jens Gerlach
Frama-Clang crashes on error in contract
ID0002352:
**This issue was created automatically from Mantis Issue 2352. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002352:
**This issue was created automatically from Mantis Issue 2352. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002352 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-01-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached example uses mistakenly the assignment operator = instead of == in the ensures clause.
Frama-Clang crashes on this example.
frama-c -wp -wp-rte assignment_in_contract.cpp
[kernel] Parsing assignment_in_contract.cpp (external front-end)
framaCIRGen: ACSLTermOrPredicate.cpp:7096: Parser::Base::ReadResult Acsl::TermOrPredicate::readToken(Acsl::Parser::State&, Acsl::Parser::Arguments&): Assertion `false' failed.
Aborted (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "assignment_in_contract.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
A message along the lines of normal Frama-C
"user error: Assignment operators not allowed in annotations."
would be more helpful.
## Attachments
- [assignment_in_contract.cpp](/uploads/f0d2dd6918d688ca68e2c4996617c929/assignment_in_contract.cpp)
Virgile Prevosto
Virgile Prevosto
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/279
kernel warns about invalid implicit conversion
2021-03-30T08:04:31Z
Jens Gerlach
kernel warns about invalid implicit conversion
ID0002350:
**This issue was created automatically from Mantis Issue 2350. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002350:
**This issue was created automatically from Mantis Issue 2350. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002350 | Frama-C | Plug-in > clang | public | 2018-01-31 | 2018-02-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
When processing the attached (C-)code with Fram-Clang the kernels sends a diagnostic as follows
frama-c -wp -wp-rte implicit_conversion.cpp
[kernel] Parsing implicit_conversion.cpp (external front-end)
implicit_conversion.cpp:16:44: invalid implicit conversion
Now output intermediate result
When processed as a ACSL/C file by WP no warning occurs.
## Attachments
- [implicit_conversion.cpp](/uploads/fe14759cabb542c2f83d85b61b0e28e9/implicit_conversion.cpp)
- [imcCnv2.cpp](/uploads/d6c96e86d9b3ff6a2032499013b2aac0/imcCnv2.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/278
predicate argument type "struct S" accepted by Frama-C, but not by Frama-clang
2021-03-30T08:05:33Z
Jochen Burghardt
predicate argument type "struct S" accepted by Frama-C, but not by Frama-clang
ID0002358:
**This issue was created automatically from Mantis Issue 2358. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002358:
**This issue was created automatically from Mantis Issue 2358. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002358 | Frama-C | Plug-in > clang | public | 2018-02-08 | 2018-02-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **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 stack_init_cpp.cpp" in the attached file results in an error message "keyword 'keyword -> struct' encountered when parsing a type" for line 6 (C++/C subroutine), but not for line 4 (Acsl predicate). When the file is renamed to "frama-c stack_init_cpp.c" , the error message disappears.
## Attachments
- [stack_init_cpp.cpp](/uploads/655f490009c017323d0b16f5261f5c9f/stack_init_cpp.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/276
insufficient contracts for generated constructors and assignment operator(s)
2021-03-30T08:22:30Z
Jens Gerlach
insufficient contracts for generated constructors and assignment operator(s)
ID0002356:
**This issue was created automatically from Mantis Issue 2356. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002356:
**This issue was created automatically from Mantis Issue 2356. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002356 | Frama-C | Plug-in > clang | public | 2018-02-07 | 2018-02-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached file contains a very simple class (struct).
It is used in simple copy initialization and assignment operations.
When called with with
frama-c-gui -wp -wp-rte generated_member_functions.cpp
then the two assertions are not verified by Fram-Clang/WP.
From what I see about the contracts of the generated constructors and assignment operator(s), this is not surprising because their postconditions do not refer to the member 'n'.
EVA seems to work just fine.
## Attachments
- [generated_member_functions.cpp](/uploads/c7dc2a564d7435a34294e0aa839d9178/generated_member_functions.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/275
Frama-clang complains when reserved keywords are used as property labels, whi...
2021-02-22T12:58:04Z
Jochen Burghardt
Frama-clang complains when reserved keywords are used as property labels, while Frama-C doesn't
ID0002359:
**This issue was created automatically from Mantis Issue 2359. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002359:
**This issue was created automatically from Mantis Issue 2359. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002359 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **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 st.cpp" on the attached program produces a (stderr) message "st.cpp:2:14: keyword 'keyword -> invariant' encountered when parsing term or predicate". When 'invariant' is changed e.g. to 'assert', a similar message is printed.
When the file is renamed to "st.c", the message disappears. Likewise, our use of a reserved keyword as procedure or parameter name didn't cause such a message.
## Attachments
- [st.cpp](/uploads/41260701caea5f2a98b989b4454b1fc1/st.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/274
"Here" as predicate label in statement contract causes Segmentation fault
2021-02-22T12:58:03Z
Jochen Burghardt
"Here" as predicate label in statement contract causes Segmentation fault
ID0002360:
**This issue was created automatically from Mantis Issue 2360. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002360:
**This issue was created automatically from Mantis Issue 2360. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002360 | 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** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp rotate_cpp.cpp" on the attached program outputs an error message "rotate_cpp.cpp:5:23: expecting a label argument", and then crashes due to a Segmentation fault. The problem disappears when the statement contract in line 5 is changed into an assertion.
## Attachments
- [rotate_cpp.cpp](/uploads/56cddcc4aad61f74882ab6f0a55106cf/rotate_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
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/272
"let" in predicate body unrecognized
2021-02-22T12:58:02Z
Jochen Burghardt
"let" in predicate body unrecognized
ID0002362:
**This issue was created automatically from Mantis Issue 2362. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002362:
**This issue was created automatically from Mantis Issue 2362. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002362 | 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 replace_copy_cpp.cpp" on the attached program issues two messages, the 2nd probably being a follow-up problem of the 1st:
replace_copy_cpp.cpp:2:47: unexpected token 'operator -> =' when starting to parse a term
replace_copy_cpp.cpp:4:21: unknown identifier 'Replace'
When the body of predicate definition of "Replace" is changed to "( \at(a[0],K) > 3 )", both message disappear.
## Attachments
- [replace_copy_cpp.cpp](/uploads/dfacff4304f7f33dc22b5bb80602202c/replace_copy_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/271
variable declared in "for" init-part unrecognized in loop body assigns clause...
2021-02-22T12:58:01Z
Jochen Burghardt
variable declared in "for" init-part unrecognized in loop body assigns clause; 100% verification degree reported nevertheless
ID0002363:
**This issue was created automatically from Mantis Issue 2363. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002363:
**This issue was created automatically from Mantis Issue 2363. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002363 | 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 remove_copy_cpp.cpp" on the attached program prints an error message "remove_copy_cpp.cpp:4:17: unknown identifier 'i'". When "i" is declared outside the loop, the message disappears.
As a second, more severe issue, Frama-C subsequently ignores the assertion. It prints "[wp] Proved goals: 0 / 0", and terminates successfully with exit code 0. In a larger program, an error message like the above one is likely to be overlooked, and from a reported verification degree of 100%, the user will infer that his program has been fully verified.
## Attachments
- [remove_copy_cpp.cpp](/uploads/6f2ad5f898b23f26b2560dceafaa9ba7/remove_copy_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/270
Frama-clang reports overloading ambiguity where Frama-C doesn't
2021-03-30T08:17:49Z
Jochen Burghardt
Frama-clang reports overloading ambiguity where Frama-C doesn't
ID0002364:
**This issue was created automatically from Mantis Issue 2364. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002364:
**This issue was created automatically from Mantis Issue 2364. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002364 | Frama-C | Plug-in > clang | public | 2018-02-12 | 2018-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
(Not sure this is a bug. The reported behavior may be unavoidable due to C++'s more complicated overloading rules?)
Running "frama-c -wp reverse_cpp.cpp" reports "reverse_cpp.cpp:9:33: Ambiguity when choosing overloaded function Rev". When the file is renamed to "reverse_cpp.c", this message disappears, and the version in line 5 is chosen (as the verification rate 0/1 indicates).
## Attachments
- [reverse_cpp.cpp](/uploads/446586da0c38f6161bae6da4fc04495a/reverse_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/269
user-defined type not accepted after builtin type in quantifier chain
2021-02-22T12:58:00Z
Jochen Burghardt
user-defined type not accepted after builtin type in quantifier chain
ID0002365:
**This issue was created automatically from Mantis Issue 2365. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002365:
**This issue was created automatically from Mantis Issue 2365. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002365 | 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 partial_sort_cpp.cpp" on the attached program reports "partial_sort_cpp.cpp:4:43: unexpected token 'identifier -> v' after a binders construct". The message disappears when "v" is declared as "int" instead of "value_type", or when "int n" is removed.
## Attachments
- [partial_sort_cpp.cpp](/uploads/27af4a5cad254a4d4837fb9aae5e0732/partial_sort_cpp.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/268
loop assigns clause ginored under strange circumstances
2021-03-30T08:17:49Z
Jochen Burghardt
loop assigns clause ginored under strange circumstances
ID0002366:
**This issue was created automatically from Mantis Issue 2366. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002366:
**This issue was created automatically from Mantis Issue 2366. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002366 | 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 reverse_cpp.cpp" on the attached program reports
reverse_cpp.cpp:13:37: Ambiguity when choosing overloaded function Rev.
reverse_cpp.cpp:16:[wp] warning: Missing assigns clause (assigns 'everything' instead)
For the 1st message, cf. #2364, using a similar program.
The 2nd message disappears if
(1) the file is renamed to "reverse_cpp.c",
(2) the "assert" clause in line 10 is removed,
(3) the "loop invariant" clause in line 13 is removed, or
(4) the (possibly imaginary, cf. #2364) "Rev" ambiguity is resolved by removing one of the overloaded predicate definitions in lines 3 and 5.
## Attachments
- [reverse_cpp.cpp](/uploads/8c82fdfbc3ec2d18a714a489c7d8a4df/reverse_cpp.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/266
e-acsl-gcc failes on macOS
2021-02-22T12:57:55Z
Jens Gerlach
e-acsl-gcc failes on macOS
ID0002369:
**This issue was created automatically from Mantis Issue 2369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002369:
**This issue was created automatically from Mantis Issue 2369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002369 | Frama-C | Plug-in > E-ACSL | public | 2018-02-23 | 2018-02-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to process the example 'true.i' from http://frama-c.com/eacsl.html
the `e-acsl-gcc.sh` script fails and reports
e-acsl-gcc: fatal error: unexpected output of system getopt
### Additional Information :
This problem does not occur on my Linux installation.
Julien Signoles
Julien Signoles