frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-03-26T16:58:43Zhttps://git.frama-c.com/pub/frama-c/-/issues/301Substraction results in unknown values2021-03-26T16:58:43Zmantis-gitlab-migrationSubstraction results in unknown valuesID0002166:
**This issue was created automatically from Mantis Issue 2166. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002166:
**This issue was created automatically from Mantis Issue 2166. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002166 | Frama-C | Plug-in > Eva | public | 2015-09-17 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | buhler | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
This line of code has:
if (len + n >= 64) len -= n;
For callstack [SHA256_Update :: frama-test.c:19 <- main]
Before this statement / after this statement:
n ∈ [1..63]
and:
For callstack [SHA256_Update :: frama-test.c:19 <- main]
Before this statement:
len ∈ [1..1024]
After this statement:
len ∈ [--..--]
I was expecting len after this to be:
len ∈ [0..1023]
It might be non-obvious to get that completely correct from the first time, and could understand that it would be turned in:
len ∈ [-62..1023]
KurtDavid BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/298"pointer comparison" warning emitted for "p==NULL"2021-02-22T12:58:36ZJochen Burghardt"pointer comparison" warning emitted for "p==NULL"ID0002256:
**This issue was created automatically from Mantis Issue 2256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002256:
**This issue was created automatically from Mantis Issue 2256. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002256 | Frama-C | Plug-in > Eva | public | 2016-11-11 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | - |
### Description :
Running "frama-c -val -val-warn-undefined-pointer-comparison=pointer ptrcmp3.c" on the attached file results in a warning:
ptrcmp3.c:10:[kernel] warning: pointer comparison. assert \pointer_comparable((void *)p, (void *)0);
The warning disappears if
1. the type of parameter "name" is changed from "char*" to "char" both in "foo" and in "main", or
2. the "assigns" clause for "foo" is deleted.
The warning seems strange by itself, as every pointer should be comparable to NULL. The changes that make the warning disappear (in particular 1.) support the hypothesis that this is a bug.
## Attachments
- [ptrcmp3.c](/uploads/3c9e9c4fc07c25680f1e5c42b0b24b71/ptrcmp3.c)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/297suggest to provide and document a unique warning string to grep for in value-...2021-02-22T13:36:36ZJochen Burghardtsuggest to provide and document a unique warning string to grep for in value-analysis output filesID0002259:
**This issue was created automatically from Mantis Issue 2259. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002259:
**This issue was created automatically from Mantis Issue 2259. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002259 | Frama-C | Plug-in > Eva | public | 2016-11-28 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | Frama-C 15-Phosphorus | **Fixed in Version** | - |
### Description :
When running Frama-C value analysis with parameters that cause a huge output file, it is not possible to read thourgh it line by line. (My current output file, "results.txt.gz", has the size 700 MB in gzipped format) In this case, it is only possible to use tools like "zgrep -10 -n -i 'warning:' results.txt.gz >resultsExcerpt.txt" to find relevant messages.
The value analysis manual suggests (on p.41) to grep for "assert" to get all messages that relate to a proof obligation. However, warnings about non-terminating functions are not found this way, so at least another grep for "terminat" seems necessary. More important, I can't be not sure that "assert" and "terminat" will cover all relevant messages.
Therefore I suggest to provide a single search string that will appear at every relevant message. It shouldn't fit into C's variable name syntax (so 'warning:' is ok, but 'warning' is not). It should be mentioned in the manual at a prominent place when discussing the batch (i.e. non-gui) version of value analysis; it is an essential part of the methodology then.
If there are several such strings (e.g. for different degrees of severity, like 'error:' or 'hint:'), they should all be documented in that same place. A user who has read this documentation part should be confident about how to catch all relevant messages.https://git.frama-c.com/pub/frama-c/-/issues/296Option "-lib-entry" results misses possible values of function pointers2021-02-22T12:58:33ZJochen BurghardtOption "-lib-entry" results misses possible values of function pointersID0002254:
**This issue was created automatically from Mantis Issue 2254. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002254:
**This issue was created automatically from Mantis Issue 2254. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002254 | Frama-C | Plug-in > Eva | public | 2016-11-07 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
(I posed this question also on frama-c-discuss on 3 Nov 2016, 16:20, and received a reply from David Mentré on 5 Nov 2016, 15:52. The advice to use an invariant and increase the slevel originates from Julien Signoles.)
Running "frama-c -val -main foo -lib-entry -slevel 10 fctptr.c" on the attached program results in an output of:
a ∈ [--..--]
fct ∈ {0}
While option "-lib-entry" behaves on the int variable "a" as described in the value analysis manual (sect.5.2.3, p.58), it seems to have no effect on the function pointer variable "fct". Moreover, the latter is analyzed to contain a null pointer, while it actually never does, due to its initialization at the declaration. Instead, since "fct" is declared "static", I'd expect the analysis to report:
a ∈ [--..--]
fct ∈ {{ &f1, &f2 }}
When "-lib-entry" is omitted, Frama-C's analysis coincides with mine:
a ∈ {1}
fct ∈ {{ &f1 }}
Both with and without option "-lib-entry", Frama-C's results don't change when the invariant is removed. To sum up, it seems that the use of option "-lib-entry" inhibits information from call analysis, but also from explicit invariants.
## Attachments
- [fctptr.c](/uploads/35907f38d48ab7e62a81d969080d542a/fctptr.c)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/295Should warn for overlapping lv=lv; assignments2021-03-29T08:03:16ZPascal CuoqShould warn for overlapping lv=lv; assignmentsID0000945:
**This issue was created automatically from Mantis Issue 945. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000945:
**This issue was created automatically from Mantis Issue 945. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000945 | Frama-C | Plug-in > Eva | public | 2011-09-01 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | low | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C should warn for this program:
struct S { int x; int y; };
struct T { int z; struct S s; };
union U { struct S f ; struct T g; } u;
main(){
u.f = u.g.s;
return 0;
}
6.5.16.1 3:
If the value being stored in an object is read from another object that overlaps in any way the storage of the first object, then the overlap shall be exact and the two objects shall have qualified or unqualified versions of a compatible type; otherwise, the behavior is undefined.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/294opam upgrade/update failed to update frama-c2021-02-22T12:58:31Zmantis-gitlab-migrationopam upgrade/update failed to update frama-cID0002335:
**This issue was created automatically from Mantis Issue 2335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002335:
**This issue was created automatically from Mantis Issue 2335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002335 | Frama-C | Kernel | public | 2017-12-07 | 2017-12-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | cdelord | **Assigned To** | maroneze | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux x86_64 | **OS** | Fedora | **OS Version** | 26 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
opam refuses to upgrade from Frama-C Phosphorus to Sulfur because of dependency issues with the legacy frama-c-base package.
### Additional Information :
Workaround: opam remove frama-c-base
### Steps To Reproduce :
(previous version of frama-c installed with opam)
opam update
opam upgradehttps://git.frama-c.com/pub/frama-c/-/issues/293Incorrect overflow and cast assertions for bitfields2021-02-22T13:36:38ZKostyantyn VorobyovIncorrect overflow and cast assertions for bitfieldsID0002314:
**This issue was created automatically from Mantis Issue 2314. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002314:
**This issue was created automatically from Mantis Issue 2314. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002314 | Frama-C | Plug-in > RTE | public | 2017-06-26 | 2017-12-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following snippet:
struct STR { int num : 7; };
void foo(int a, long b) {
struct STR s = { .num = 0 };
s.num = b;
s.num += a;
}
generates the following assertions
/*@ assert rte: signed_downcast: b ≤ 2147483647; */
/*@ assert rte: signed_downcast: -2147483648 ≤ b; */
s.num = (int)b;
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)s.num + a; */
/*@ assert rte: signed_overflow: (int)s.num + a ≤ 2147483647; */
s.num = (int)((int)s.num + a);
The limits for s.num are incorrect, since s.num is a bitfield of 7 bits its limits should be [-64, 63]
### Steps To Reproduce :
frama-c -machdep x86_64 file.c -rte -warn-signed-overflow -warn-signed-downcast -print
## Attachments
- [b.c](/uploads/40289826f17e8973d35c95cb375e1d60/b.c)
- [patch-downcast-rte](/uploads/f5123ced359a007c0de00ba52c7fc3cd/patch-downcast-rte)https://git.frama-c.com/pub/frama-c/-/issues/291Incorrect dependency assignment using arraay inside for loop2021-02-22T13:12:37Zmantis-gitlab-migrationIncorrect dependency assignment using arraay inside for loopID0002341:
**This issue was created automatically from Mantis Issue 2341. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002341:
**This issue was created automatically from Mantis Issue 2341. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002341 | Frama-C | Plug-in > from | public | 2018-01-11 | 2018-01-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jaimeabe | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | urgent | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 16.04.3 LTS (GN |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached file, the dependencies Analysis result should be GlobalVector[3] FROM Schalter dependent. However, the reality is that it assigns the dependenciy of Schalter to the whole vector (GlobalVector[0..4]).
### Steps To Reproduce :
Call the -deps Option in frama-c from command line using the attached file.
## Attachments
- [arrayInLoop.c](/uploads/54a6bd7ff7988631cf94538bcc12e52e/arrayInLoop.c)https://git.frama-c.com/pub/frama-c/-/issues/290How to use the "Callers ..." context menu item2021-02-22T12:58:22Zmantis-gitlab-migrationHow to use the "Callers ..." context menu itemID0001431:
**This issue was created automatically from Mantis Issue 1431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001431:
**This issue was created automatically from Mantis Issue 1431. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001431 | Frama-C | Graphical User Interface | public | 2013-05-27 | 2018-01-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dhekir | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Pardon the ignorance, but I couldn't find this on the manual...
I have a program where, after parsing, some warnings of this form are emitted:
"Calling undeclared function __builtin_swap32. Old style K&R code?"
I know there is a missing source file somewhere in my project, but I'd like to know who is calling these functions (since they are never directly called in my code). So I right-click on the function prototype on the GUI, and the last button in the context menu is "Callers ...". If I click on it, the "Launching analysis" window is displayed, with no indication of which analysis to choose.
I suppose the analysis I'd like is "Syntactic callgraph". So I choose it, without customizing any options, click Execute, but nothing changes. The "Callers ..." button is always visible when right-clicking the function declaration.
I noticed that if I choose the "Users" analysis, when right-clicking afterwards there is no more "Callers ..." button on the context menu, but I fail to see how any of the new options (e.g. Dependencies) could help me identify the function callers.
Is there a simpler way, other than by manually parsing the DOT file (the produced graph is too large for me to visually inspect it), to obtain information about function callers?Andre MaronezeAndre Maronezehttps://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 Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/286direct initialisation of bool by nullptr2021-02-22T13:36:06ZJens Gerlachdirect initialisation of bool by nullptrID0002347:
**This issue was created automatically from Mantis Issue 2347. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002347:
**This issue was created automatically from Mantis Issue 2347. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002347 | Frama-C | Plug-in > clang | public | 2018-01-22 | 2018-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached program "nullptr_crash.cpp" compiles without warnings with g++-7.2 in C++11 mode.
Clang-5.0 issues a warning (and if I understood the standard correctly, it shouldn't, because the example uses "direct initialisation").
Frama-Clang crashes on the example.
The second example "nullptr_bool.cpp" which uses "copy initialisation" only warns about implicit conversion...
## Attachments
- [nullptr_crash.cpp](/uploads/7975ccda4df20b073580f91557d4e559/nullptr_crash.cpp)
- [nullptr_bool.cpp](/uploads/cecfd360ef834b1bcbf7a7a9606df04f/nullptr_bool.cpp)
- [nullptr_no_crash.cpp](/uploads/7bfd118ea401a367676355d8352849c2/nullptr_no_crash.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/285unknown variable in contract is not treated as an error2021-02-22T12:58:15ZJens Gerlachunknown variable in contract is not treated as an errorID0002348:
**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 PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/284BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version"2021-02-22T12:58:14ZJens GerlachBTS 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/283warning from kernel about exceptions2021-02-22T12:58:13ZJens Gerlachwarning from kernel about exceptionsID0002349:
**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 PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/282no diagnostics on wrong keyword2021-03-30T07:48:10ZJens Gerlachno diagnostics on wrong keywordID0002351:
**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 PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/281Frama-Clang crashes on error in contract2021-02-22T13:36:01ZJens GerlachFrama-Clang crashes on error in contractID0002352:
**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 PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/280Alt-Ergo reports about " bool and int cannot be unified"2021-02-22T14:01:05ZJens GerlachAlt-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 PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/279kernel warns about invalid implicit conversion2021-03-30T08:04:31ZJens Gerlachkernel warns about invalid implicit conversionID0002350:
**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 PrevostoVirgile Prevosto