wrongly synthesized assert
ID0000195:
**This issue was created automatically from Mantis Issue 195. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000195 | Frama-C | Plug-in > Eva | public | 2009-07-16 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | derepas | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
Let's consider the following program:
1. #include <stdlib.h>
2.
3. struct my_struct {
4. void * my_field;
5. };
6.
7. void main(struct my_struct * l) {
8. if (l!=NULL) {
9. if (l->my_field!=NULL) {
10. l->my_field=NULL;
11. }
12. }
13. }
Then I launch frama-c-gui and value analysis on entry point 'main'.
The following assert is synthesized between line 8 and 9:
//@ assert \valid(&l->my_field);
Even though l->my_field could be NULL and the program be ok.
issue