Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #1296
Closed
Open
Issue created Mar 30, 2011 by Pascal Cuoq@pascal

r12436, unnecessary warning for side-effects (csmith)

ID0000771: This issue was created automatically from Mantis Issue 771. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000771 Frama-C Kernel public 2011-03-30 2014-02-12
Reporter pascal Assigned To virgile Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C GIT, precise the release id Target Version - Fixed in Version Frama-C Nitrogen-20111001

Description :

The 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));

Attachments

  • se.i
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking