Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001330Frama-CKernelpublic2012-12-14 11:562014-03-13 15:57
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001330: inconsistent redefinition of type undetected
DescriptionThe attached program defines a type "ftest_t" as "int*" in line 2, but as "double" in line 3. This inconsistently defined type is used as parameter type in line 5. Nevertheless, the command "frama-c ftest.c" does not report any error (under Nitrogen; I can't yet test it here under Oxygen).
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (73 bytes) 2012-12-14 11:56 [Show Content]

- Relationships

-  Notes
(0003625)
yakobowski (manager)
2012-12-14 15:13

The problem is still present in Oxygen.

Notice that the AST produced is correct, as the second occurrence of ftest_t is properly renamed to avoid ambiguity. We do not claim that Frama-C will replace your compiler in terms of C parsing/linking errors so I'm not sure this will be corrected.
(0003626)
Jochen (reporter)
2012-12-14 15:34

I wouldn't need this to be corrected; I just wanted to report it.

- Issue History
Date Modified Username Field Change
2012-12-14 11:56 Jochen New Issue
2012-12-14 11:56 Jochen File Added: ftest.c
2012-12-14 12:14 signoles Status new => assigned
2012-12-14 12:14 signoles Assigned To => virgile
2012-12-14 15:13 yakobowski Note Added: 0003625
2012-12-14 15:34 Jochen Note Added: 0003626
2013-09-26 15:35 svn Checkin
2013-09-26 15:35 svn Status assigned => resolved
2013-09-26 15:35 svn Resolution open => fixed
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker