From owner-lclint-interest@virginia.edu Fri May 25 20:18 EDT 2001
X-Mailer: exmh version 2.2 06/23/2000 with version: MH 6.8.3 #8[UCI]
To: lclint-interest@cs.virginia.edu
Subject: lack of control flow analysis
Mime-Version: 1.0
Date: Fri, 25 May 2001 17:12:18 -0700
From: Mathew Yeates <mathew@fugue.jpl.nasa.gov>
Precedence: bulk
Content-Type: text/plain; charset=us-ascii
Content-Length: 1277


I did some more work on the problem I sent yesterday. Here is a slightly 
modified version.
Even though line 14 is never executed, it causes s->i to go dead because 
"free" takes an
"only" param. And, even if line 13 were executed,  line 18 would not be 
executed
because of the "return" statement. It appears that lclint cannot tell when a 
particular branch
is impossible in a particular context.

The error I get from the following program is
t.c:18:7: Dead storage s->i passed as out parameter: s->i



1  #include <stdlib.h>
     2  int foo(   /*@out@*/char  *  b  );
     3
     4  struct s {
     5      /*@reldef@ *//*@relnull@ */ char *i;
     6  };
     7
     8  static int redir(struct s *s)
     9  {
    10      s->i = malloc(1 * sizeof(int));
    11      if (!(s->i))
    12          return 1;
    13      if (0) {
    14          free(s->i);
    15          return 1;
    16      }
    17      if (foo(s->i) == 1) {
    18          free(s->i);
    19          /*@-usereleased@ */
    20          return 1;
    21          /*@=usereleased@ */
    22      }
    23  /*@-usereleased@ */
    24      return 0;
    25  /*@=usereleased@ */
    26  }
    27
    28  void goo(void)
    29  {
    30      struct s s;
    31      if (redir(&s) == 1) exit(0);
    32  }