Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001503Frama-CKernelpublic2013-10-18 15:352015-05-10 22:55
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001503: failure: invalid implicit conversion from void to int
DescriptionThe program below appears to conform to the C99 standard:

$ cat r.c
void f()
{
  0 ? 0 * 0 ? 0 : 0 : 0;
}
$ gcc -c -std=c99 -pedantic r.c

But the Frama-C front-end refuses to parse it:

$ frama-c r.c
[kernel] preprocessing with "gcc -C -E -I. r.c"
r.c:3:[kernel] failure: invalid implicit conversion from void to int
[kernel] user error: skipping file "r.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
Additional InformationThis may be the first of a non-singleton series of programs misdiagnosed with the "invalid conversion from void to int" diagnostic. The original error is in the Linux kernel. It seems better to submit only reduced programs even if the real problem is still there after the first fix, than to submit the entire code.

The entire file causing the problem is attached to this issue, but I can do reduction again after the 0 ? 0 * 0 ? 0 : 0 : 0; problem is fixed.
TagsNo tags attached.
Attached Files

- Relationships
related to 0002117closedyakobowski frama-c gets confused by comma operator inside ternary operator: cannot cast from void to char 

-  Notes
(0004553)

2014-02-12 16:57

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2013-10-18 15:35 pascal New Issue
2013-10-18 15:36 pascal Assigned To => virgile
2013-10-18 15:36 pascal Status new => assigned
2013-10-18 15:39 pascal File Added: adreno_a2xx.c.i
2013-10-18 15:41 pascal Additional Information Updated
2013-10-18 15:43 pascal Description Updated
2013-10-29 15:13 svn Checkin
2013-10-29 15:13 svn Status assigned => resolved
2013-10-29 15:13 svn Resolution open => fixed
2013-11-08 17:52 pascal File Deleted: adreno_a2xx.c.i
2014-02-12 16:57 Note Added: 0004553
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
2015-05-10 22:55 yakobowski Relationship added related to 0002117


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker