Frama-C Bug Tracking System - Frama-C
View Issue Details
0002419Frama-CPlug-in > RTEpublic2018-12-17 13:572018-12-17 13:58
signoles 
signoles 
normalminoralways
confirmedopen 
Frama-C 18-Argon 
 
0002419: Missing cast in code generated by RTE
==========
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
No tags attached.
related to 0002412confirmed signoles E-ACSL crash with RTE generated assertion with booleans 
Issue History
2018-12-17 13:57signolesNew Issue
2018-12-17 13:57signolesStatusnew => assigned
2018-12-17 13:57signolesAssigned To => signoles
2018-12-17 13:58signolesStatusassigned => confirmed
2018-12-17 13:58signolesRelationship addedrelated to 0002412

There are no notes attached to this issue.