frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T12:58:36Zhttps://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/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/54An option to return error code if there are any problems with the analysis, s...2021-03-29T11:49:28ZvarosiAn option to return error code if there are any problems with the analysis, so that frama-c is easier to be used in CI/CD workflowsFeature Request
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*...Feature Request
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: Docker: framac/frama-c:22.0
- Frama-C version: 22.0
- Plug-in used: WP and EVA
- OS name: macOS
- OS version: 11.1
# Steps to reproduce the issue
I put frama-c in a BitBucket CI pipeline. With calling directly frama-c executable. CI pipelines fail when error code returned from executables is different than 0. That way it stops you from pushing erroneous code.
# Expected behaviour
It would be great if there is an option so that frama-c executable return non-zero error code if in EVA found any error in my code, or in WP not all conditions are met.
# Actual behaviour
frama-c return 0 even if EVA show errors from the analysed code. It returns 0 if WP have found non correct behaviour also.