Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002435Frama-CKernelpublic2019-05-07 16:452019-05-08 11:00
Reporterrmalak 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
Platformx86_64 Linux 4.19OSOCaml 4.07.1 Opam 2.0.3OS VersionDebian Sid
Product VersionFrama-C 18-Argon 
Target VersionFixed in Version 
Summary0002435: kernel generates UnspecifiedSequence when 2 following ternary operators
DescriptionConsider 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 ?

TagsNo tags attached.
Attached Filesc file icon ternary_operators.c [^] (52 bytes) 2019-05-07 16:45 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2019-05-07 16:45 rmalak New Issue
2019-05-07 16:45 rmalak File Added: ternary_operators.c
2019-05-08 11:00 virgile Assigned To => virgile
2019-05-08 11:00 virgile Status new => assigned


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker