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