Frama-C Bug Tracking System - Frama-C
View Issue Details
0000829Frama-CPlug-in > jessiepublic2011-05-18 17:452011-05-24 06:45
Jochen 
cmarche 
normalminoralways
assignedopen 
Frama-C Carbon-20110201 
 
0000829: alias between int* and uint* handled incorrectly
The manual "jessie-tutorial-Carbon-beta.pdf" allows casts between pointer types (p.22). However, in the attached program, the property "*x == \old(*x)" of the function ftest() can be verified under SeparationPolicy(none), although ftest() modifies *x via its (possible) alias *y. A reason for this behavior is that x and y point to different types, viz. int and uint (if y is made an int, too, the bug vanishes). As a consequence, "p == \old(p)" can be proven for main(), although running the program reveals that p changes from 0 to 123. A side remark: type incompatibility uint* vs. int* seems to be unchecked in the initialization in line 14; no cast was needed there.
No tags attached.
c ftest.c (414) 2011-05-18 17:45
https://bts.frama-c.com/file_download.php?file_id=220&type=bug
Issue History
2011-05-18 17:45JochenNew Issue
2011-05-18 17:45JochenStatusnew => assigned
2011-05-18 17:45JochenAssigned To => cmarche
2011-05-18 17:45JochenFile Added: ftest.c
2011-05-18 21:18pascalNote Added: 0001910
2011-05-23 11:21JochenNote Added: 0001919
2011-05-24 06:45cmarcheNote Added: 0001921

Notes
(0001910)
pascal   
2011-05-18 21:18   
Regarding the side remark: the kind of warning that would be emitted at line 14 belongs in a compiler. Frama-C does not try to duplicate warnings that belong in a good compiler. We believe our limited resources are better spent elsewhere. gcc -c -Wall ftest.c ... ftest.c:14: warning: pointer targets in initialization differ in signedness
(0001919)
Jochen   
2011-05-23 11:21   
What my side remark really meant is: both semantical equivalent code versions ftest(&p,&p); and unsigned int *q; q = &p; ftest(&p,q); result in an error message "Jessie support for unions and pointer casts is disabled". I just wondered whether the version used in file ftest.c, viz. unsigned int * const q = &p; ftest(&p,q); should raise that error, too.
(0001921)
cmarche   
2011-05-24 06:45   
Just a note to say that, yes, I've seen this bug report. The problem is in the handling of the "main" function: global initializations are not taken into account. - Claude