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>
3. struct my_struct {
4. void * my_field;
5. };
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.