Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002419Frama-CPlug-in > RTEpublic2018-12-17 13:572018-12-17 13:58
Reportersignoles 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 18-Argon 
Target VersionFixed in Version 
Summary0002419: Missing cast in code generated by RTE
Description========== int main(void) { int i = 2; unsigned int j = i < 2; return 0; } $ frama-c -check -rte -warn-unsigned-downcast -print -ocode res.c [kernel] Parsing a.c (with preprocessing) [rte] annotating function main /* Generated by Frama-C */ int main(void) { int __retres; int i = 2; /*@ assert rte: unsigned_downcast: (i < 2) ≤ 4294967295; */ /*@ assert rte: unsigned_downcast: 0 ≤ (i < 2); */ unsigned int j = (unsigned int)(i < 2); __retres = 0; return __retres; } $ frama-c res.c [kernel] Parsing res.c (with preprocessing) [kernel:annot-error] res.c:6: Warning: comparison of incompatible types: 𝔹 and ℤ. Ignoring code annotation [kernel] User Error: warning annot-error treated as fatal error. ========== The terms (i < 2) should be casted to int in the generated predicates
TagsNo tags attached.
Attached Files

- Relationships
related to 0002412confirmedsignoles E-ACSL crash with RTE generated assertion with booleans 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2018-12-17 13:57 signoles New Issue
2018-12-17 13:57 signoles Status new => assigned
2018-12-17 13:57 signoles Assigned To => signoles
2018-12-17 13:58 signoles Status assigned => confirmed
2018-12-17 13:58 signoles Relationship added related to 0002412


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker