2021-03-01 05:16 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001081Frama-CKernelpublic2012-09-19 17:16
Assigned Tovirgile 
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:

  int foo, x, y;
  foo ? (void)x : (signed char)y;
  return 0;


$ 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




pascal (reporter)

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)

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
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
+Issue History