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
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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
(0002663)
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.
(0002664)
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 - 2018 MantisBT Team
Powered by Mantis Bugtracker