Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001081Frama-CKernelpublic2012-02-05 18:482012-09-19 17:16
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001081: foo ? (void)x : (signed char)y (csmithreduction)
DescriptionThe program below should probably be rejected as ill-typed: main(){ int foo, x, y; foo ? (void)x : (signed char)y; return 0; } but: $ ppc/bin/toplevel.opt -val t.c [kernel] preprocessing with "gcc -C -E -I. t.c" ... [value] Values at end of function main: __retres ? {0} Incidentally, for this example, the access to uninitialized variable foo should also cause the program to be analyzed as non-terminating. Not sure whether that secondary bug is in the front-end or in the value analysis.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
pascal (reporter)
2012-02-05 19:16

Additional info by Chucky Ellison: (n1570) 6.5.15:3 doesn't allow this as one of the allowed cases: One of the following shall hold for the second and third operands: — both operands have arithmetic type; — both operands have the same structure or union type; — both operands have void type; — both operands are pointers to qualified or unqualified versions of compatible types; — one operand is a pointer and the other is a null pointer constant; or — one operand is a pointer to an object type and the other is a pointer to a qualified or unqualified version of void. Moreover, paragraphs 5 and 6 do not give semantics for how to convert the types to a common type.
yakobowski (manager)
2012-02-06 08:41

I think I can shed some light on whether the second part of the bug comes from the front-end or the value analysis ~$ frama-c bug2.c -print [...] /* Generated by Frama-C */ int main(void) { int __retres; __retres = 0; return (__retres); }

- Issue History
Date Modified Username Field Change
2012-02-05 18:48 pascal New Issue
2012-02-05 19:16 pascal Note Added: 0002663
2012-02-06 08:41 yakobowski Note Added: 0002664
2012-02-06 08:48 pascal Summary foo ? (void)x : (signed char)y (csmith reduction) => foo ? (void)x : (signed char)y (csmithreduction)
2012-02-22 18:06 svn Checkin
2012-02-22 18:06 svn Status new => resolved
2012-02-22 18:06 svn Resolution open => fixed
2012-02-22 19:13 signoles Status resolved => assigned
2012-02-22 19:13 signoles Assigned To => virgile
2012-02-22 19:13 signoles Status assigned => resolved
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker