Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000933Frama-CKernelpublic2011-08-23 16:292014-02-12 16:59
Reporterpascal 
Assigned Topascal 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000933: Wrong AST (csmith)
DescriptionMini:~/d $ cat r.c
int g_18;

typedef unsigned int uint32_t;
typedef int int32_t;
typedef short int16_t;
typedef long long int64_t;

struct S0 {
   uint32_t f0;
   int16_t f1;
  signed f2 : 26;
   int64_t f3;
};

union U3 {
  signed f0 : 7;
   int32_t f1;
   int32_t f2;
   struct S0 f3;
};

static union U3 g_7[1] = {{0x00868BB4L}};

int g_5;
int g_2;

void Frama_C_show_each(unsigned);

main(){
  unsigned short l_8 = 1UL;
  unsigned int l_16 = 0xBD4AA41AL;

  g_2 |= (g_7[g_5].f3.f2 = l_16);
  Frama_C_show_each(g_2);
}

Mini:~/d $ ~/ppc/bin/toplevel.opt -val -slevel 99 r.c | grep each
[value] Called Frama_C_show_each({3175785498})

Mini:~/d $ clang -m32 r.c show_each.c && ./a.out
r.c:29:1: warning: type specifier missing, defaults to 'int' [-Wimplicit-int]
main(){
^
1 warning generated.
[value] Called Frama_C_show_each({21668890})

Mini:~/d $ ~/ppc/bin/toplevel.opt -print r.c
[kernel] preprocessing with "gcc -C -E -I. r.c"
r.c:34:[kernel] warning: Body of function main falls-through. Adding a return statement
/* Generated by Frama-C */
typedef unsigned int uint32_t;
typedef int int32_t;
typedef short int16_t;
typedef long long int64_t;
struct S0 {
   uint32_t f0 ;
   int16_t f1 ;
   int f2 : 26 ;
   int64_t f3 ;
};
union U3 {
   int f0 : 7 ;
   int32_t f1 ;
   int32_t f2 ;
   struct S0 f3 ;
};
int g_18;
static union U3 g_7[1] = {{(int)0x00868BB4L}};
int g_5;
int g_2;
extern void Frama_C_show_each(unsigned int);
int main(void)
{
  int __retres;
  unsigned short l_8;
  unsigned int l_16;
  int __attribute__((__FRAMA_C_BITFIELD_SIZE__(26))) tmp;
  l_8 = (unsigned short)1UL;
  l_16 = (unsigned int)0xBD4AA41AL;
  { /*undefined sequence*/
    tmp = (int)l_16;
    g_7[g_5].f3.f2 = tmp;
    g_2 |= tmp;
  }
  Frama_C_show_each((unsigned int)g_2);
  __retres = 0;
  return (__retres);
}


The program displayed with -print is not equivalent to the original because __attribute__((__FRAMA_C_BITFIELD_SIZE__(26))) in the declaration of tmp does not have any semantics.
TagsNo tags attached.
Attached Files

- Relationships
related to 0000969closedpascal Sliced program computes differently from original (csmith) 

-  Notes
(0002164)
pascal (reporter)
2011-08-23 16:56
edited on: 2011-12-13 18:13

The file show_each.c for executing contains:


#include <stdio.h>

void Frama_C_show_each(unsigned int crc)
{
  printf ("[value] Called Frama_C_show_each({%u})\n", crc);
}

(0002553)
pascal (reporter)
2011-12-13 10:58

Note:
            
Michael Mehlich from SemanticDesigns proposed the best solution, which is to store the address of g_7[g_5].f3 in a temporary variable.
(0004735)
pascal (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-08-23 16:29 pascal New Issue
2011-08-23 16:29 pascal Status new => assigned
2011-08-23 16:29 pascal Assigned To => monate
2011-08-23 16:32 pascal Description Updated
2011-08-23 16:56 pascal Note Added: 0002164
2011-08-23 16:56 pascal Note Edited: 0002164
2011-09-20 08:45 pascal Relationship added related to 0000969
2011-09-20 09:30 pascal Assigned To monate => pascal
2011-09-20 09:31 svn Checkin
2011-09-20 09:31 svn Status assigned => resolved
2011-09-20 09:31 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2011-12-13 10:58 pascal Note Added: 0002553
2011-12-13 10:58 pascal Status closed => feedback
2011-12-13 10:58 pascal Resolution fixed => reopened
2011-12-13 10:58 pascal Status feedback => closed
2011-12-13 10:58 pascal Resolution reopened => fixed
2011-12-13 18:10 pascal Status closed => feedback
2011-12-13 18:10 pascal Resolution fixed => reopened
2011-12-13 18:12 pascal Description Updated
2011-12-13 18:13 pascal Note Edited: 0002164
2011-12-13 18:13 pascal Status feedback => closed
2011-12-13 18:13 pascal Resolution reopened => fixed
2011-12-14 13:24 pascal Status closed => feedback
2011-12-14 13:24 pascal Resolution fixed => reopened
2011-12-14 13:25 pascal View Status private => public
2011-12-14 13:25 pascal Status feedback => closed
2011-12-14 13:25 pascal Resolution reopened => fixed
2014-02-12 16:59 pascal Note Added: 0004735
2014-02-12 16:59 pascal Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker