|Anonymous | Login | Signup for a new account||2019-07-18 05:49 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000829||Frama-C||Plug-in > jessie||public||2011-05-18 17:45||2011-05-24 06:45|
|Product Version||Frama-C Carbon-20110201|
|Target Version||Fixed in Version|
|Summary||0000829: alias between int* and uint* handled incorrectly|
|Description||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.
|Tags||No tags attached.|
|Attached Files||ftest.c [^] (414 bytes) 2011-05-18 17:45 [Show Content]|
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
What my side remark really meant is: both semantical equivalent code versions
unsigned int *q;
q = &p;
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;
should raise that error, too.
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.
|2011-05-18 17:45||Jochen||New Issue|
|2011-05-18 17:45||Jochen||Status||new => assigned|
|2011-05-18 17:45||Jochen||Assigned To||=> cmarche|
|2011-05-18 17:45||Jochen||File Added: ftest.c|
|2011-05-18 21:18||pascal||Note Added: 0001910|
|2011-05-23 11:21||Jochen||Note Added: 0001919|
|2011-05-24 06:45||cmarche||Note Added: 0001921|
|Copyright © 2000 - 2019 MantisBT Team|