Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000676Frama-CKernelpublic2011-01-18 16:242011-01-18 16:25
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in Version 
Summary0000676: Strange AST produced with unspecified side-effects involve function calls in expressions
DescriptionOriginal code:

    if(((fast_read(o, 3) ^ fetch) & 0xffffff) == 0 && o < src - MINOFFSET)

Transformed as:

         ui32 tmp_1 ;
          { /*undefined sequence*/
            tmp_1 = fast_read((void const *)o,(unsigned int )3);
            ;
          }
          if (((tmp_1 ^ fetch) & (unsigned int )0xffffff) == (unsigned int )0) {
            if (o < src - 2) {


Contact Pascal for whole function.
TagsNo tags attached.
Attached Files

- Relationships
related to 0000771closedvirgile r12436, unnecessary warning for side-effects (csmith) 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-01-18 16:24 pascal New Issue
2011-01-18 16:25 pascal Status new => assigned
2011-01-18 16:25 pascal Assigned To => virgile
2011-03-30 15:46 pascal Relationship added related to 0000771


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker