Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000771Frama-CKernelpublic2011-03-30 15:442014-02-12 16:59
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000771: r12436, unnecessary warning for side-effects (csmith)
DescriptionThe command below leads the value analysis to check whether *g_19 can be in alias with g_20. They can be, so the value analysis emits an alarm, but I fail to see why this should be checked. The functions called have no side-effects. In fact, there are no side-effects in the whole assignment, except the side-effect of the assignment.

This is likely to be related to 676: the display below is very strange, with some statements displayed as empty lines (and still having inputs !!).
__

bin/toplevel.opt -unspecified-access se.i
____

assert.30103607.7.c:632:[kernel] warning: Unspecified sequence with side effect:
                  /* <- */
                  tmp = safe_add_func_uint16_t_u_u(p_69.f2,(unsigned short )l_80);
                  /* <-
                  */
                  tmp_0 = safe_lshift_func_uint8_t_u_u((unsigned char )p_70.f0,
                                                       (unsigned int )l_85);
                  /* <- p_70.f3 */
                  
                  /* <-
                  */
                  tmp_1 = safe_sub_func_uint32_t_u_u((unsigned int )l_90[0][0][1],
                                                     (unsigned int )*g_19);
                  /* <- */
                  tmp_2 = safe_sub_func_uint32_t_u_u(tmp_1,(unsigned int )p_70.f3);
                  /* <- l_80 g_14 */
                  
                  /* <- */
                  tmp_3 = safe_rshift_func_int8_t_s_s((signed char )p_70.f3,g_20);
                  /* <- g_20 */
                  
                  /* <-
                  */
                  tmp_4 = safe_add_func_int8_t_s_s((signed char )((int )tmp_3 >= g_20),
                                                   (signed char )((long )(l_80 < (int32_t )g_14) <= 0xC7L));
                  /* <-
                  */
                  tmp_5 = safe_add_func_int8_t_s_s(tmp_4,
                                                   (signed char )((uint32_t )((int )tmp != (int )tmp_0) <= tmp_2));
                  /* <- g_14 */
                  
                  /* *g_19 <-
                  */
                  *g_19 = (int32_t )safe_mul_func_int8_t_s_s((signed char )g_14,
                                                             (signed char )(1U != (unsigned int )tmp_5));
______
TagsNo tags attached.
Attached Files? file icon se.i [^] (158,471 bytes) 2011-03-30 15:44 [Show Content]

- Relationships
related to 0000676assignedvirgile Strange AST produced with unspecified side-effects involve function calls in expressions 
related to 0000832closedvirgile r13586 Spurious "assert \separated(...)" (csmith) 

-  Notes
(0004784)

2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-03-30 15:44 pascal New Issue
2011-03-30 15:44 pascal File Added: se.i
2011-03-30 15:44 pascal Status new => assigned
2011-03-30 15:44 pascal Assigned To => virgile
2011-03-30 15:46 pascal Relationship added related to 0000676
2011-05-17 19:36 svn Checkin
2011-05-17 19:36 svn Status assigned => resolved
2011-05-17 19:36 svn Resolution open => fixed
2011-05-24 08:27 pascal Relationship added related to 0000832
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 Note Added: 0004784
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker