2021-01-27 11:37 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001330Frama-CKernelpublic2014-03-13 15:57
Assigned Tovirgile 
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 Files
  • c file icon ftest.c (73 bytes) 2012-12-14 11:56 -
    typedef int *ftest_t;
    typedef double ftest_t;
    void main(ftest_t i) {}
    c file icon ftest.c (73 bytes) 2012-12-14 11:56 +




yakobowski (manager)

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.


Jochen (reporter)

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