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 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 - 2019 MantisBT Team
Powered by Mantis Bugtracker