Frama-C Bug Tracking System - Frama-C
View Issue Details
0002435Frama-CKernelpublic2019-05-07 16:452019-05-08 11:00
rmalak 
virgile 
normalmajoralways
assignedopen 
x86_64 Linux 4.19OCaml 4.07.1 Opam 2.0.3Debian Sid
Frama-C 18-Argon 
 
0002435: kernel generates UnspecifiedSequence when 2 following ternary operators
Consider ternary_operator.c :

/////////////////
int main() {
  return (2>1) ? 1 : (1>0) ? 1 : 0;
}
/////////////////

then frama-c generates :

/////////////////
int main(void)
{
  int tmp_0;
  if (2 > 1) tmp_0 = 1;
  else {
    int tmp;
    if (1 > 0) tmp = 1; else tmp = 0;
    tmp_0 = tmp;
  }
  return tmp_0;
}
//////////////

and considers :

if (1 > 0) tmp = 1; else tmp = 0;
tmp_0 = tmp;

as an UnspecifiedSequence statement

if (1 > 0) tmp = 1; else tmp = 0;

as a "If" statement

and

tmp_0 = tmp;

as a "Instr" statement

Is the construction of the AST with a intermediate UnspecifiedSequence the normal behaviour ?

No tags attached.
c ternary_operators.c (52) 2019-05-07 16:45
https://bts.frama-c.com/file_download.php?file_id=1310&type=bug
Issue History
2019-05-07 16:45rmalakNew Issue
2019-05-07 16:45rmalakFile Added: ternary_operators.c
2019-05-08 11:00virgileAssigned To => virgile
2019-05-08 11:00virgileStatusnew => assigned

There are no notes attached to this issue.