Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002350Frama-CPlug-in > clangpublic2018-01-31 17:562018-02-08 16:57
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002350: kernel warns about invalid implicit conversion
DescriptionWhen processing the attached (C-)code with Fram-Clang the kernels sends a diagnostic as follows

frama-c -wp -wp-rte implicit_conversion.cpp
[kernel] Parsing implicit_conversion.cpp (external front-end)
implicit_conversion.cpp:16:44: invalid implicit conversion
Now output intermediate result

When processed as a ACSL/C file by WP no warning occurs.
 
TagsNo tags attached.
Attached Filescpp file icon implicit_conversion.cpp [^] (516 bytes) 2018-01-31 17:56
cpp file icon imcCnv2.cpp [^] (192 bytes) 2018-02-08 16:54

- Relationships

-  Notes
(0006523)
Jochen (reporter)
2018-02-08 15:47

Using the command "frama-c -wp -wp-rte implicit_conversion.cpp | cat -n" reveals that the "implicit conversion" message is written (probably) to stderr, while all other output is writen to stdout.
(0006526)
Jochen (reporter)
2018-02-08 16:57

I just found and boiled down another example of the same behavior; see file "imcCnv2.cpp". The error message disappears if
(1) line 5 is removed,
(2) line 7 is removed, or
(3) each occurrence of "integer" in the file is changed to "int".

- Issue History
Date Modified Username Field Change
2018-01-31 17:56 jens New Issue
2018-01-31 17:56 jens Status new => assigned
2018-01-31 17:56 jens Assigned To => virgile
2018-01-31 17:56 jens File Added: implicit_conversion.cpp
2018-01-31 18:09 virgile Status assigned => acknowledged
2018-02-08 15:47 Jochen Note Added: 0006523
2018-02-08 16:54 Jochen File Added: imcCnv2.cpp
2018-02-08 16:57 Jochen Note Added: 0006526


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker