Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002355Frama-CPlug-in > clangpublic2018-02-05 16:432018-02-05 17:28
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002355: Alt-Ergo reports about " bool and int cannot be unified"
DescriptionIf the attached simple C++ file is processed with the command line

    frama-c -wp -wp-rte -warn-unsigned-downcast -wp-out equal.wp++ equal.cpp

then the following error message occurs:

[wp] [Alt-Ergo] Goal typed__Z5equali_assert_rte_unsigned_downcast : Failed
    characters 4-22:typing error: bool and int cannot be unified

Could it be that Frama-Clang (or WP?) treats the return value of operator == as int instead of bool?
Additional InformationThe error message disappears when the option "-warn-unsigned-downcast" is omitted.
TagsNo tags attached.
Attached Filescpp file icon equal.cpp [^] (42 bytes) 2018-02-05 16:43

- Relationships
related to 0001484assignedcorrenson ill-typed alt-ergo proof obligation 

-  Notes
(0006521)
virgile (developer)
2018-02-05 17:28

Symptoms are not unlike issue 1484

- Issue History
Date Modified Username Field Change
2018-02-05 16:43 jens New Issue
2018-02-05 16:43 jens Status new => assigned
2018-02-05 16:43 jens Assigned To => virgile
2018-02-05 16:43 jens File Added: equal.cpp
2018-02-05 17:27 virgile Relationship added related to 0001484
2018-02-05 17:28 virgile Note Added: 0006521


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker