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