goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
40 stars 16 forks source link

Wrong type for some comparisons #29

Closed michael-schwarz closed 3 years ago

michael-schwarz commented 3 years ago

For the following input

int main (int argc, char* argv[])
{
    signed char f2 = 7;
    signed char l_1857 = ((0xFFBD4A17L && f2) | f2);
}

CIL produces

int main(int argc , char **argv ) 
{ 
  signed char f2 ;
  signed char l_1857 ;
  {
#line 5
  f2 = (signed char)7;
#line 6
  l_1857 = (signed char )((f2 != (signed char)0) | (int )f2);
#line 7
  return (0);
}
}

The subexpression f2 != (signed char)0 in this has typ signed char, but the type should be int as for all comparisons in C.


This causes an error inside in Goblint where we assume comparisons have the correct type as mandated by the standard. References https://github.com/goblint/analyzer/pull/175

jerhard commented 3 years ago

Fixed in #36