Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000829Frama-CPlug-in > jessiepublic2011-05-18 17:452011-05-24 06:45
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in Version 
Summary0000829: alias between int* and uint* handled incorrectly
DescriptionThe 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.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (414 bytes) 2011-05-18 17:45 [Show Content]

- Relationships

-  Notes
(0001910)
pascal (reporter)
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 (reporter)
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 (developer)
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

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker